OR-Tools cung cấp hai công cụ chính để giải các bài toán lập trình số nguyên:
- MPSolver, được mô tả trong phần trước.
- Chúng tôi sẽ mô tả về trình giải CP-SAT trong phần tiếp theo.
Ví dụ giải quyết bài toán lập trình số nguyên bằng cả CP-SAT trình giải mã và trình bao bọc MPSolver, hãy xem Giải quyết bài tập.
Lưu ý: Để tăng tốc độ tính toán, trình giải CP-SAT hoạt động trên các số nguyên. Điều này có nghĩa là bạn phải xác định vấn đề tối ưu hoá bằng số nguyên. Nếu bắt đầu với một bài toán có ràng buộc với các số hạng không phải là số nguyên, bạn trước tiên, cần nhân các điều kiện ràng buộc đó với một số nguyên đủ lớn để tất cả các số hạng đều là số nguyên. Xem Ví dụ như Giải quyết một vấn đề tối ưu hoá.
Các phần sau đây trình bày ví dụ về cách sử dụng trình giải quyết CP-SAT.
Ví dụ: tìm một giải pháp khả thi
Hãy bắt đầu với một bài toán mẫu đơn giản trong đó có:
- Ba biến, x, y, z, mỗi biến có thể nhận các giá trị: 0, 1, hoặc 2.
- Một quy tắc ràng buộc: x != y
Chúng tôi sẽ bắt đầu bằng việc trình bày cách sử dụng trình giải quyết CP-SAT để tìm ra một giải pháp khả thi bằng tất cả các ngôn ngữ được hỗ trợ. Mặc dù việc tìm kiếm một giải pháp khả thi là không đáng kể trong trường hợp này, nhưng trong các bài toán lập trình ràng buộc phức tạp hơn, có thể rất khó để xác định liệu có giải pháp khả thi nào không.
Để xem ví dụ về cách tìm ra giải pháp tối ưu cho vấn đề về CP, vui lòng xem Giải quyết vấn đề tối ưu hoá.
Nhập thư viện
Mã sau đây nhập thư viện bắt buộc.
Khai báo mô hình
Mã sau đây khai báo mô hình CP-SAT.
Tạo biến
Mã sau đây sẽ tạo các biến cho bài toán này.
Trình giải này tạo ra 3 biến x, y và z, mỗi biến có thể nhận các giá trị 0, 1 hoặc 2.
Tạo quy tắc ràng buộc
Đoạn mã sau đây sẽ tạo quy tắc ràng buộc x != y.
Gọi trình giải
Mã sau đây gọi trình giải.
Giá trị trả về của CP-SAT
Trình giải CP-SAT sẽ trả về một trong các giá trị trạng thái như trong bảng dưới đây. Trong trong ví dụ này, giá trị được trả về là OPTIMAL.
Trạng thái Mô tả OPTIMAL Đã tìm thấy một giải pháp khả thi tối ưu. FEASIBLE Đã tìm thấy một giải pháp khả thi nhưng chúng tôi không biết giải pháp đó có tối ưu hay không. INFEASIBLE Vấn đề này đã được chứng minh là không khả thi. MODEL_INVALID CpModelProto đã cho không vượt qua bước xác thực. Bạn có thể nhận được lỗi cụ thể bằng cách gọi ValidateCpModel(model_proto). UNKNOWN Trạng thái của mô hình này không xác định do không tìm thấy nghiệm (hoặc vấn đề chưa được chứng minh là KHÔNG THỂ CHIA SẺ được) trước khi có điều gì đó khiến người giải điểm dừng, chẳng hạn như giới hạn thời gian, giới hạn bộ nhớ hoặc giới hạn tuỳ chỉnh do người dùng đặt.
Các giá trị này được xác định trong cp_model.proto.
Hiển thị giải pháp đầu tiên
Đoạn mã sau đây cho thấy giải pháp khả thi đầu tiên mà trình giải toán tìm ra. Xin lưu ý rằng mã này kiểm tra xem giá trị của status là FEASIBLE hay OPTIMAL.
Chạy chương trình
Bạn có thể xem các chương trình hoàn chỉnh ở phần tiếp theo. Khi chạy một chương trình, bạn sẽ trả về đáp án đầu tiên mà trình giải tìm thấy:
x = 1 y = 0 z = 0
Hoàn tất chương trình
Dưới đây là các chương trình hoàn chỉnh.
Tìm tất cả giải pháp
Tiếp theo, chúng ta sẽ trình bày cách sửa đổi chương trình ở trên để tìm tất cả các giải pháp khả thi.
Phần bổ sung chính cho chương trình là một máy in giải pháp. Lệnh gọi lại mà bạn chuyển đến trình giải, nơi hiển thị từng lời giải khi tìm được.
Thêm máy in giải pháp
Đoạn mã sau đây sẽ tạo máy in giải pháp.
Gọi trình giải
Đoạn mã sau đây gọi trình giải và chuyển máy in giải pháp cho trình giải quyết đó.
Chạy chương trình
Chương trình hoàn chỉnh được trình bày trong phần tiếp theo. Khi chạy chương trình, bạn sẽ thấy tất cả 18 giải pháp khả thi:
x=1 y=0 z=0 x=2 y=0 z=0 x=2 y=1 z=0 x=2 y=1 z=1 x=2 y=1 z=2 x=2 y=0 z=2 x=2 y=0 z=1 x=1 y=0 z=1 x=0 y=1 z=1 x=0 y=1 z=2 x=0 y=2 z=2 x=1 y=2 z=2 x=1 y=2 z=1 x=1 y=2 z=0 x=0 y=2 z=0 x=0 y=1 z=0 x=0 y=2 z=1 x=1 y=0 z=2 Status = FEASIBLE
Hoàn tất chương trình
Dưới đây là các chương trình hoàn chỉnh.