Nhập môn thực tiễn về lập trình ràng buộc với CP-SAT và Python

Giới thiệu thực tiễn về lập trình ràng buộc: CP-SAT và Python

Mô hình khai báo

• Lập trình ràng buộc (CP) là một mô hình khai báo để giải các bài toán tối ưu hóa rời rạc
• Không giống lập trình mệnh lệnh, bạn mô tả kết quả mong muốn và chương trình tự suy ra kết quả
• Ví dụ, bài viết giải thích sự khác biệt giữa cách tiếp cận mệnh lệnh và cách tiếp cận khai báo khi trích xuất danh sách người trưởng thành

Những điều cơ bản của lập trình ràng buộc (CP)

• Mô hình: mô tả kết quả mong muốn của bài toán
• Biến: các giá trị cần tìm, mỗi biến có một miền giá trị (tập các giá trị được phép)
• Ràng buộc: mô tả mối quan hệ giữa các biến
• Lời giải: gán giá trị cho các biến sao cho thỏa mãn các ràng buộc

Ví dụ thực tiễn với Python và CP-SAT

• Bài toán: tạo lịch làm việc hằng tuần cho nhân viên
• Tạo mô hình: dùng CP-SAT để tạo một mô hình rỗng
• Dữ liệu: định nghĩa danh sách nhân viên và vai trò, ngày làm việc, ca làm việc
• Định nghĩa biến: tạo các biến Boolean biểu thị việc mỗi nhân viên có làm việc hay không
• Thêm ràng buộc: thêm các ràng buộc vào biến theo mô tả của bài toán

Giải mô hình

• Giải: giải mô hình và đưa ra kết quả
• Ràng buộc bổ sung: thêm các ràng buộc như tránh làm thêm giờ, giới hạn thời gian làm việc của một số nhân viên cụ thể, ngăn một số nhân viên có thời gian làm việc chồng lấn nhau

Phần giữa: trạng thái giải

• Trạng thái giải: trả về các trạng thái như tối ưu, khả thi, không khả thi, không rõ
• Ví dụ: giải thích từng trạng thái bằng một ví dụ đơn giản

"Xin lỗi, Emma"

• Trạng thái không khả thi: Emma không thể nghỉ 5 ngày trong tuần
• Đề xuất thay thế: đề xuất để Emma chỉ nghỉ 3 ngày trong tuần

Mục tiêu: phân bổ đều thời gian làm việc

• Thêm mục tiêu: thêm mục tiêu để phân bổ thời gian làm việc đồng đều
• Kết quả: thời gian làm việc của mỗi nhân viên được phân bổ đồng đều

Kết luận

• Giới thiệu các khái niệm cơ bản: giới thiệu những khái niệm nền tảng của lập trình ràng buộc và giải thích bằng ví dụ thực tiễn
• Báo trước bài viết tiếp theo: bài viết tiếp theo sẽ đề cập cách dùng lập trình ràng buộc để chọn chỉ mục trong Postgres

Ý kiến của GN⁺

• Tính hữu ích của lập trình ràng buộc: rất hữu ích để giải các bài toán tối ưu hóa phức tạp
• Điểm mạnh của CP-SAT: CP-SAT, được phát triển như một phần của dự án OR-Tools của Google, có hiệu năng rất mạnh
• Trường hợp áp dụng thực tế: có thể áp dụng vào các vấn đề thực tế như tạo lịch làm việc cho nhân viên
• Những điểm cần cân nhắc khi áp dụng công nghệ: khi áp dụng công nghệ mới, cần cân nhắc đường cong học tập và vấn đề tích hợp với hệ thống hiện có
• Đề xuất các dự án tương tự: các solver thương mại như CPLEX của IBM và Gurobi cũng cung cấp các khả năng tương tự

[GN⁺]

Ý kiến Hacker News

• Từng có kinh nghiệm sử dụng các bộ giải ràng buộc trước đây, và những công cụ này cho hiệu năng rất đáng kinh ngạc

  • Vấn đề là hầu như không có tài liệu dành cho người mới bắt đầu
  • Phần lớn tài liệu là về cách giải Sudoku hoặc các tài liệu nghiên cứu mang tính kỹ thuật cao
  • Mong rằng các công cụ có thể giải được nhiều bài toán hơn sẽ trở nên dễ tiếp cận hơn
  • Dễ tiếp cận ở đây vẫn có nghĩa là cần lập trình viên

• Đang viết lại một chương ngắn trong cuốn sách cũ của tôi về việc dùng MiniZinc và Python

  • MiniZinc là một hệ thống lập trình ràng buộc
  • Có một khóa học hay trên Coursera sử dụng MiniZinc

• Nhiều chương trình cố gắng có một cách biểu diễn dữ liệu duy nhất, nhưng trong đa số trường hợp điều đó là không hợp lý

  • Cần rất nhiều sự bóp méo để làm cho thuật toán hoạt động trên một biểu diễn mới
  • Lúc nào tôi cũng thấy tiếc vì người ta không chuyển đổi biểu diễn thường xuyên hơn
  • Khi chuyển đổi biểu diễn, có thể có được cách biểu diễn rất ngắn gọn, từ đó cho phép chạy nhanh hơn

• Có một khách hàng vận hành trại thể thao

  • Bọn trẻ có thể yêu cầu môn thể thao và bạn bè mà chúng muốn
  • Điều này tạo ra một bài toán xếp lịch khó đối với con người
  • Đã xây dựng một hệ thống đơn giản bằng công cụ tối ưu hóa dựa trên OR-Tools
  • Giờ đây chỉ với vài cú nhấp chuột là có thể hoàn tất lịch

• Có kinh nghiệm dùng nhiều bộ giải vào đầu những năm 2000

  • Hiện tại đang làm phần mềm dùng Python (web)
  • Rất vui khi thấy có một bài đào sâu về chủ đề này
  • Việc chuyển các ràng buộc thành mô hình chiếm 90% công việc và là phần khó nhất

• Tò mò không biết có CAD tham số nào chủ yếu hoạt động như một bộ giải ràng buộc hay không

  • Ban đầu thường thấy bất tiện vì phải ước lượng các giá trị tham số mà mình không quan tâm
  • Thay vào đó muốn ràng buộc các tham số mình quan tâm và tối ưu hóa phần còn lại

• Tò mò không biết so với mixed integer programming thì sẽ như thế nào