Phá đối xứng khi nhiều phòng tương đương

1. Nhận diện phép hoán vị hợp lệ

Hai phòng chỉ thay thế được cho nhau khi cùng tham gia vào mọi điều kiện liên quan. Cùng sức chứa vẫn chưa đủ nếu một phòng thuộc cơ sở khác, có ca bị khóa riêng hoặc chịu điểm phạt riêng. Trong ví dụ nhỏ, hai lớp diễn ra cùng ca và hai phòng có đặc tính giống hệt nhau, nên đổi tên hai phòng biến mọi lịch khả thi thành một lịch khả thi có cùng chi phí.

2. Giữ đúng một đại diện

Đánh số lớp và phòng. Với hai lớp cần hai phòng, yêu cầu phòng của lớp 1 có mã nhỏ hơn phòng của lớp 2. Trong mỗi cặp phương án hoán vị, đúng một phương án thỏa thứ tự tăng. Lập luận dựa vào việc cả hai phòng được dùng và tên phòng không có ý nghĩa nghiệp vụ. Với ba lớp có nhiều ca, cần phát biểu lại phép hoán vị áp dụng chung cho toàn lịch trước khi đặt thêm điều kiện.

3. Chạy hai cấu hình để đối chiếu

Chạy với -n 0 để liệt kê toàn bộ. Khi chưa bật phá đối xứng, có hai answer set. Thêm -c phadoixung=1 thì còn một. Khi so hai cấu hình, gom các lịch theo quan hệ đổi tên trước rồi kiểm tra mỗi nhóm vẫn còn ít nhất một nghiệm. So trực tiếp số answer set sẽ cho hai con số khác nhau như mong đợi.

Nếu chưa có Clingo, cài bằng python -m pip install clingo.

Chạy ví dụ bằng python -m clingo asp_pha_doi_xung_phong.lp -n 0.

#const phadoixung=0.
lop(1..2).
phong(1..2).
1 { xep(L,P) : phong(P) } 1 :- lop(L).
:- xep(1,P), xep(2,P).
:- phadoixung=1, xep(1,P), xep(2,Q), P>Q.
#show xep/2.

4. Tìm phản ví dụ cho một quy tắc quá mạnh

Hãy cho phòng 2 là phòng duy nhất có thiết bị của lớp 1. Lịch duy nhất lúc này đặt lớp 1 ở phòng 2 và lớp 2 ở phòng 1. Nếu vẫn bật quy tắc phá đối xứng, mô hình vô nghiệm. Khi đánh giá hiệu năng, nên ghi cả số phương án bị loại và thời gian giải, bởi giảm số nghiệm không tự động đồng nghĩa giảm thời gian chứng minh tối ưu.

Đọc thêm Tài liệu ngôn ngữ ASP của Potassco.