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

 (pganalyze.com)
1 điểm bởi GN⁺ 2024-07-05 | 1 bình luận | Chia sẻ qua WhatsApp
  • Lập trình ràng buộc (CP) là một cách tiếp cận khai báo để mô hình hóa các bài toán tối ưu hóa rời rạc bằng biến, miền giá trị và ràng buộc thay vì mã thủ tục, để solver tìm ra nghiệm thỏa mãn các điều kiện
  • Cốt lõi của mô hình là biến cần tìm, miền giá trị là phạm vi các giá trị có thể có, và các ràng buộc giới hạn quan hệ giữa các biến; khi cần, có thể dùng hàm mục tiêu để chọn nghiệm tốt hơn
  • Ví dụ chia tiền mua kẹo của Alice, Bob và Carol cho thấy luồng cải thiện từ một nghiệm hợp lệ sang nghiệm cân bằng hơn thông qua alldifferent, maximum, minimize
  • Ví dụ thực tế sử dụng solver mã nguồn mở CP-SAT của Google OR-Tools và Python để lập lịch làm việc theo tuần cho 4 nhân viên với 7 ngày, 3 ca và 2 vai trò
  • Trên cùng một mô hình, có thể từng bước thêm các điều kiện như giới hạn 40 giờ mỗi tuần, lịch học, các cặp không được làm cùng nhau, phân bổ ca cuối tuần đồng đều, yêu cầu nghỉ phép và tối thiểu hóa chênh lệch số ca làm

Tư duy cơ bản của lập trình ràng buộc

  • 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
  • Lập trình mệnh lệnh viết tuần tự quy trình để đi đến kết quả, còn cách tiếp cận khai báo mô tả các điều kiện của kết quả mong muốn và để hệ thống thực thi tìm ra kết quả đó
  • Trong ví dụ lấy danh sách người trưởng thành, mã mệnh lệnh sẽ duyệt danh sách người và kiểm tra Age >= 18, còn SQL khai báo biểu diễn trực tiếp điều kiện như SELECT person_name FROM people WHERE age >= 18;
  • CP cũng mô tả kết quả mong muốn dưới dạng mô hình, với các thành phần cốt lõi là biến, miền giá trị và ràng buộc
    • Biến biểu thị điều cần tìm
    • Miền giá trị là tập các giá trị mà biến có thể nhận
    • Ràng buộc giới hạn quan hệ giữa các biến

Biến, miền giá trị, ràng buộc và hàm mục tiêu

  • Một nghiệm là một phép gán trong đó mỗi biến nhận một giá trị trong miền giá trị của nó và đồng thời thỏa mãn mọi ràng buộc
  • Ví dụ tiền mua kẹo là bài toán Alice, Bob và Carol mỗi người có tối đa 20 đô la và cùng góp tiền để mua hộp kẹo giá 50 đô la
    • Các biến a, b, c là số tiền mỗi người đóng góp
    • Miền giá trị của ba biến là {0, ..., 20}
    • a + b + c == 50 để khớp tổng tiền
    • a >= b để Alice trả ít nhất bằng Bob
    • c % 5 == 0 để giới hạn số tiền của Carol là bội số của 5
    • Có thể đặt a != b, a != c, b != c để ba người không trả cùng một số tiền
  • Những điều kiện liên quan đến nhiều biến có thể được biểu diễn bằng ràng buộc toàn cục (global constraints), ví dụ alldifferent(a, b, c) buộc cả ba biến đều nhận giá trị khác nhau
  • Solver nhận mô hình làm đầu vào và trả về một nghiệm hợp lệ
    • Nghiệm ví dụ a = 19, b = 11, c = 20 thỏa mãn mọi ràng buộc
    • Tuy vậy Carol trả gần gấp đôi Bob, nên có thể tồn tại một nghiệm cân bằng hơn
  • Hàm mục tiêu cho phép tối thiểu hóa hoặc tối đa hóa một biểu thức nào đó trong số các nghiệm thỏa mãn ràng buộc
    • Đặt biến mới x là khoản đóng góp lớn nhất và dùng maximum(x, [a, b, c])
    • Khi áp dụng minimize: x, kết quả trả về là a = 18, b = 17, c = 15, x = 18
    • Chênh lệch giữa khoản đóng góp lớn nhất và nhỏ nhất giảm từ 9 đô la xuống còn 3 đô la

Xây dựng mô hình lịch làm việc với CP-SAT và Python

  • Ví dụ thực tế là bài toán tạo lịch làm việc theo tuần cho một cửa hàng nhỏ
    • Cửa hàng mở cửa mỗi ngày từ 8 giờ sáng đến 8 giờ tối
    • Mỗi ngày có ba ca Morning, Afternoon, Evening và mỗi ca kéo dài 4 giờ
    • Có hai vai trò là Cashier và Restocker
    • Nhân viên gồm bốn người: Phil, Emma, David, Rebecca
  • CP-SAT là solver CP mã nguồn mở nằm trong bộ OR-Tools của Google
  • Mô hình rỗng được tạo bằng cp_model.CpModel() trong ortools.sat.python
  • Các vai trò mà từng nhân viên có thể đảm nhiệm như sau
    • Phil: Restocker
    • Emma: Cashier, Restocker
    • David: Cashier, Restocker
    • Rebecca: Cashier
  • Lịch làm việc được biểu diễn bằng biến Boolean theo tổ hợp nhân viên, vai trò, ngày và ca
    • schedule["Emma"]["Restocker"]["Monday"]["Evening"] sẽ là 1 nếu Emma làm Restocker vào ca tối thứ Hai, nếu không thì là 0
    • model.new_bool_var() tạo một biến có miền giá trị {0, 1}

Các ràng buộc làm việc cơ bản

  • Vì cần đúng một thu ngân ở mọi thời điểm, nên với mỗi cặp ngày và ca, tổng các biến của vai trò Cashier phải bằng 1
  • Nhân viên phụ trách sắp xếp hàng chỉ cần một ca mỗi ngày, nên tổng toàn bộ vai trò Restocker trong mỗi ngày được đặt bằng 1
  • Để tránh nối liền ca Evening làm kho của ngày trước với ca Morning làm kho của ngày sau, tổng của hai phân công đó không được vượt quá 1
  • Một nhân viên không thể đồng thời đảm nhiệm hai vai trò trong cùng một ca, nên tổng theo vai trò của mỗi nhân viên, ngày và ca phải nhỏ hơn hoặc bằng 1
  • Để tránh phân công vào vai trò không đủ điều kiện, mọi biến tương ứng với vai trò mà nhân viên đó không thể làm đều được cố định bằng 0
  • Mỗi ngày làm tối đa 8 giờ, tức là 2 ca
    • Nếu cùng ngày được phân công cả Morning lẫn Evening thì sẽ phát sinh 4 giờ trống ở giữa trong khoảng Afternoon
    • Vì vậy, tổng phân công Morning và Evening theo từng nhân viên và ngày bị giới hạn ở mức không quá 1 để đồng thời ngăn vượt quá 2 ca/ngày và tránh khoảng trống giữa ca

Chạy solver và kết quả ban đầu

  • Khi giải mô hình, tạo cp_model.CpSolver() và gọi solver.solve(model)
  • Sau khi có nghiệm, dùng solver.value(...) để đọc giá trị của các biến schedule
  • Lịch làm việc ban đầu thỏa mãn mọi ràng buộc cơ bản, nhưng dẫn đến việc Rebecca nhận tới 14 ca trong một tuần
  • Để tránh làm thêm quá nhiều, thêm ràng buộc giới hạn mỗi nhân viên làm tối đa 40 giờ mỗi tuần, tức 10 ca
  • Phil là sinh viên học toàn thời gian nên chỉ làm đúng 4 ca mỗi tuần, và không thể làm Morning hoặc Afternoon vào ngày thường do lịch học
  • Để Phil và Emma không làm cùng một ca, với mỗi ngày và ca, tổng phân công của hai người bị giới hạn ở mức không quá 1
  • Các ca cuối tuần mà ai cũng không thích được ràng buộc để tổng 8 ca của thứ Bảy và Chủ nhật được chia mỗi người 2 ca cho bốn nhân viên

Trạng thái nghiệm: OPTIMAL, INFEASIBLE, FEASIBLE, UNKNOWN

  • Solver nhận mô hình đầu vào và trả về trạng thái cùng với nghiệm
  • OPTIMAL có nghĩa là đã tìm được nghiệm mà không tồn tại nghiệm nào tốt hơn
    • Ví dụ khi x + y >= 5 và mục tiêu là tối thiểu hóa x + y, thì (x, y) = (5, 0) là một nghiệm tối ưu
    • (x, y) = (3, 2) cũng có cùng giá trị mục tiêu nên cũng có thể là nghiệm tối ưu
  • INFEASIBLE có nghĩa là dù gán giá trị thế nào cho các biến cũng không thể thỏa mãn các ràng buộc
    • Ví dụ x ∈ {0, ..., 10} nhưng lại yêu cầu x >= 15 thì là bất khả thi
  • Khi dừng solver vì giới hạn thời gian do bài toán lớn hoặc hàm mục tiêu phức tạp, có thể nhận một trong hai trạng thái
    • FEASIBLE: đã tìm được một nghiệm thỏa mãn ràng buộc nhưng chưa biết có tối ưu hay không
    • UNKNOWN: chưa tìm được nghiệm, và cũng chưa biết có tồn tại nghiệm hay không

Yêu cầu nghỉ phép và phân bổ công bằng

  • Khi thêm ràng buộc Emma muốn nghỉ từ thứ Hai đến thứ Sáu, trạng thái của solver trở thành INFEASIBLE
    • Vì không thể lấp đầy lịch làm việc mà không vi phạm các ràng buộc khác
  • Nếu đổi thành Emma chỉ nghỉ từ thứ Hai đến thứ Tư thì có thể lập được lịch
    • Phil làm đúng 4 ca như mong muốn
    • Emma nhận 6 ca, David 10 ca, Rebecca 8 ca
  • Để phân bổ số ca đồng đều hơn giữa Emma, David và Rebecca, thêm một hàm mục tiêu
    • Tạo biến số nguyên total_shifts biểu thị tổng số ca của từng nhân viên
    • Dùng model.new_int_var(0, 10, ...) để tạo biến số nguyên có giá trị từ 0 đến 10
    • Vì Phil làm bán thời gian nên được loại ra, còn model.add_min_equality(...) và model.add_max_equality(...) được dùng để theo dõi số ca tối thiểu và tối đa
    • model.minimize(max_shifts - min_shifts) để tối thiểu hóa chênh lệch giữa số ca nhiều nhất và ít nhất
  • Kết quả cuối cùng là Phil 4 ca, Emma 6 ca, David 9 ca, Rebecca 9 ca
    • Emma có 3 ngày nghỉ nên làm 6 ca
    • David và Rebecca được phân bổ cùng mức 9 ca

Mã ví dụ và chủ đề tiếp theo

  • Mô hình này tạo ra lịch làm việc đáp ứng đồng thời yêu cầu của chủ cửa hàng và của nhân viên
  • Có thể tiếp tục thêm ràng buộc vào cùng một mô hình CP để kiểm tra yêu cầu có khả thi hay không, rồi dùng hàm mục tiêu để tìm cách phân bổ công bằng hơn trong số các nghiệm khả thi
  • Mã ví dụ được công khai trên pganalyze GitHub
  • Chủ đề của bài viết tiếp theo là cách dùng lập trình ràng buộc cho việc chọn chỉ mục trong Postgres

Bài viết liên quan

1 bình luận

 
GN⁺ 2024-07-05
Ý kiến trên Hacker News

  • Trước đây tôi từng dùng trình giải ràng buộc, và những gì nó làm được thật sự như phép thuật. Vấn đề là không có nhiều tài liệu phù hợp cho người mới bắt đầu
    Phần lớn hoặc là giải Sudoku (Hello World của lĩnh vực này), hoặc là các tài liệu nghiên cứu sơ cấp rất kỹ thuật chỉ dành cho chuyên gia miền
    Điều đáng tiếc là nếu những công cụ như thế này trở nên dễ tiếp cận hơn, có lẽ chúng có thể giải được vô số vấn đề. Ở đây “dễ tiếp cận” vẫn có nghĩa là cần lập trình viên, và việc nhào nặn bài toán thành một DSL ràng buộc không phải là lĩnh vực mà đa số mọi người có thể làm tốt

    • Tôi nghĩ lý do những công cụ này chưa đủ dễ tiếp cận chủ yếu là vì phần lớn trình giải dựa trên quy hoạch nguyên hỗn hợp (MIP), nên phải viết miền bài toán dưới dạng các phương trình toán học. Để làm vậy, người dùng phải hiểu cả miền lẫn toán học thì mới viết đúng các ràng buộc được
      Tuy nhiên MIP không phải là toàn bộ thế giới trình giải. Cũng có các trình giải ràng buộc dựa trên tìm kiếm cục bộ, và cách này không bị giới hạn ở việc phải mô hình hóa mọi ràng buộc thành quan hệ hay phương trình giữa các biến nguyên
      Trong trình giải tìm kiếm cục bộ, ràng buộc thường được xem như một hộp đen cho biết một nghiệm cụ thể tốt đến mức nào. Vì vậy khó đảm bảo nghiệm tối ưu nếu không thử mọi nghiệm có thể, nhưng thường tìm được nghiệm gần tối ưu trong thời gian hợp lý
      Timefold Solver là một trong các trình giải dựa trên tìm kiếm cục bộ như vậy. Người dùng gắn annotation cho miền để trình giải biết các biến và các giá trị khả dĩ. Nhờ đó ràng buộc xử lý Shift và Employee thay vì int, và cũng có thể truy cập các phương thức của chúng
      Công khai: tôi làm việc tại Timefold Solver
    • Chính xác là vậy. Cú pháp hay API thực tế của trình giải ràng buộc quá đơn giản nên có thể học rất nhanh. Phần thật sự tốn thời gian và chuyên môn là mô hình hóa bài toán theo cách này, nhưng gần như không có ví dụ nào ở quy mô và độ phức tạp thực tế để tham khảo
      Tôi có khoảng 5 năm kinh nghiệm giải các bài toán lập lịch bằng MiniZinc, nhưng tiếc là toàn bộ mã đó đều đóng, nên sẽ không được phát hành mã nguồn mở
      Tôi muốn tạo một ví dụ lập trình ràng buộc hoàn chỉnh bao gồm container hóa, trực quan hóa và mô hình hóa, nhưng rào cản là tìm được một bài toán thật sự đáng giải và có dữ liệu mã nguồn mở có thể dùng được
    • Tôi đồng ý rằng phép quy giảm (reduction) khó hơn bản thân lý thuyết rất nhiều. "SAT/SMT by Example" của Dennis Yurichev (https://smt.st/) là tài liệu hay về chủ đề này, nhưng khá đáng ngợp
    • Nhận xét “phần lớn tài liệu là giải Sudoku hoặc tài liệu nghiên cứu dành riêng cho chuyên gia miền” rất chính xác. Tôi từng thử dùng trình giải SAT cho một rule engine nhưng hoàn toàn không hình dung được phải dùng thế nào
      Sau kha khá suy luận, tôi đã làm được một proof of concept cơ bản, nhưng không mở rộng được tới mức thật sự cần. Khoảng cách giữa một triển khai đồ chơi và thứ có tính thực tiễn hơn là rất lớn
    • Tôi đã code lâu năm nhưng giờ hơi gỉ tay. Năm ngoái tôi tạo một bộ tối ưu hóa đội bóng đá bằng OR-Tools của Google, với các ràng buộc lựa chọn như cho phép chơi cùng bạn bè và các điều kiện như cân bằng trình độ giữa các đội
      LLM giúp đưa tôi đi khá nhanh theo hướng đại khái đúng. Hiện tại nó vẫn không làm đúng hoàn toàn, nhưng đã hỗ trợ đủ để sau đó tôi tự hoàn thiện phần còn lại

  • Cốt lõi của tất cả những điều này là học cách mô hình hóa một thứ gì đó thành dạng có thể gửi cho trình giải. Tiếp theo là cách biểu diễn nghiệm trả về sao cho con người hiểu được
    Điều đáng tiếc là hầu hết chương trình cố giữ dữ liệu trong một biểu diễn duy nhất, đi ngược lại lối tư duy này. Trong phần lớn trường hợp, làm vậy không hợp lý, và tạo ra nhiều sự rối rắm khi phải điều chỉnh thuật toán cho khớp với biểu diễn mới
    Bài viết này cũng đề cập đến điểm đó ở phần đầu khi nói ngắn về phong cách khai báo. Tôi luôn tiếc vì code của mình không chuyển đổi giữa các biểu diễn thường xuyên hơn. Làm vậy có thể có được biểu diễn rất súc tích, và nhờ súc tích hơn mà còn có lợi ích kép là nhanh hơn
    Tất nhiên tôi biết cuối cùng đây cũng là cách mô tả nhiều data pipeline: phần lớn thời gian được dùng để biến đổi dữ liệu và rẽ nhánh nó tới nhiều vị trí tính toán khác nhau

  • Trong một cuốn sách tôi viết trước đây và hiện đang viết lại, có một chương ngắn về việc dùng MiniZinc trong Python: https://leanpub.com/pythonai/read#constraint-programming-wit...
    MiniZinc là một hệ thống lập trình ràng buộc. Cũng có một khóa Coursera hay sử dụng MiniZinc

    • Không biết có link khóa Coursera không

  • Sau khi học kinh tế lượng, tôi đã dùng nhiều trình giải trong chương trình thạc sĩ nghiên cứu vận trù hồi đầu những năm 2000. Hiện tôi làm về phần mềm web dùng Python, nên rất vui khi thấy một bài viết sâu về chủ đề này
    Tôi thích chủ đề này, và đọc bài viết khiến nhiều ký ức ùa về. Tôi cũng lại nhận ra rằng việc chuyển các ràng buộc thành mô hình (biến, cấu trúc, v.v.) chiếm 90% công việc và là phần khó nhất

    • Hồi học thạc sĩ tôi dùng một chương trình tên là GAMS
      Cấu trúc cú pháp của nó hoàn toàn ở dạng tự do
      https://www.gams.com/latest/docs/UG_GAMSPrograms.html#UG_GAM...
    • LLM có thể khá hữu ích trong việc chuyển ràng buộc thành mô hình. Tôi từng muốn thử một adapter chuyển từ LLM sang mô hình ràng buộc
      Trông giống như một “trái chín dễ hái”, nhưng tôi cũng tò mò liệu người khác có được hưởng lợi không
    • Tôi nghĩ phần khó nhất là chạy việc tối thiểu hóa bài toán trong môi trường vận hành. Việc mở rộng và làm cho nó vững trước thay đổi dữ liệu mất rất nhiều thời gian

  • Có một khách hàng vận hành trại thể thao cho trẻ em. Các em có thể yêu cầu những môn thể thao mình muốn chơi và những bạn mình muốn học cùng lớp
    Vì vậy đã phát sinh một bài toán lập lịch khó giải thủ công, và trước đây mỗi năm phải tốn vài tuần nhân lực cho việc này. Tôi đã tạo một hệ thống đơn giản kết nối dữ liệu của khách hàng với bộ tối ưu hóa dựa trên OR-Tools, và giờ đây việc lập lịch hoàn tất chỉ sau vài cú nhấp chuột

    • Đúng vậy. Nếu đưa dữ liệu, các ràng buộc và hàm tiện ích vào hệ thống một cách đúng đắn, có thể tìm được rất nhiều nghiệm đủ tốt cực nhanh
      Tôi làm huấn luyện viên một giải bóng rổ, có 8 hiệp. Không cầu thủ nào được chơi nhiều hơn cầu thủ khác từ 2 hiệp trở lên. Số đội hình khả dĩ cho mỗi trận, trong khi vẫn thỏa ràng buộc về thời lượng thi đấu, là lớn đến mức thiên văn
      Tìm một tập các đội hình thỏa ràng buộc thì rất dễ, nhưng tìm tập đội hình tối ưu hoặc gần tối ưu thì rất khó. Mọi thứ còn thú vị hơn nếu phải phản ánh cả những cầu thủ đến muộn hoặc vắng mặt không báo trước
      *Không phải lúc nào cũng hoàn toàn khả thi
    • Một bài blog viết chi tiết về cách làm việc này chắc chắn sẽ cực kỳ được quan tâm

  • Tôi tự hỏi liệu có CAD tham số nào chủ yếu hoạt động như một bộ giải ràng buộc không
    Việc ban đầu cứ phải ước lượng đại khái giá trị cho các tham số mà mình không quan tâm xảy ra quá thường xuyên và khá khó chịu. Sẽ thật tốt nếu có thể đặt các tham số quan tâm làm ràng buộc rồi tối ưu hóa phần còn lại

  • Tôi tò mò cách này so với quy hoạch nguyên hỗn hợp thì thế nào. Với các bài toán vật lý thì sao

    • Nhiều bài toán có thể được thiết lập theo cả hai cách. MILP luôn có hàm mục tiêu, và các ràng buộc luôn là tổ hợp tuyến tính của các biến quyết định
      Vì Gurobi nhanh đến khó tin, nên có thể đáng để cố gắng bẻ bài toán thành dạng MILP nhằm lấy được nghiệm
    • CP-SAT chỉ dành cho số nguyên, nên có lẽ không phù hợp lắm với vật lý. Có thể scale số thực, nhưng không tốt bằng việc xử lý trực tiếp số dấu phẩy động
      Ưu điểm của CP-SAT là xử lý các biến và ràng buộc Boolean cũng như số nguyên hiệu quả hơn nhiều so với bộ giải MIP, đặc biệt nổi bật ở các ràng buộc cấp cao như all_different
    • Tôi đoán nhìn chung là tương tự nhau. https://www.amazon.com/gp/product/1107658799/ là cuốn sách gần nhất tôi đọc về chủ đề này, và nó đề cập nhiều ý tưởng giống vậy
      Đặc biệt, phần trong bài viết này nói về việc cố gắng tối thiểu hóa một giá trị nào đó theo tôi là đang trực tiếp viết về cùng nội dung đó