Điều có thể đúng và điều tất yếu đúng trong tập lịch ASP

1. Hai câu hỏi cần hai phép suy luận

Khi một lớp có thể học ca 1 hoặc ca 2, câu hỏi “lớp có thể học ca 1 không?” khác với “mọi lịch đều xếp lớp vào ca 1 phải không?”. Câu hỏi đầu cần tìm ít nhất một nghiệm chứa phép gán. Câu hỏi sau cần xác nhận không có nghiệm nào bỏ phép gán ấy. Trả lời từ nghiệm đầu tiên có thể làm người dùng hiểu một lựa chọn thành một điều kiện bắt buộc.

2. Từ hợp và giao tới ý nghĩa nghiệp vụ

Trên tập nghiệm hữu hạn đã liệt kê đầy đủ, hợp chứa các nguyên tử xuất hiện ở ít nhất một nghiệm, còn giao chứa các nguyên tử xuất hiện ở mọi nghiệm. Ví dụ có lớp a trong cả hai lịch, nhưng hai nguyên tử xep(a,1) và xep(a,2) xuất hiện ở hai lịch khác nhau. Vì vậy lop(a) nằm trong giao, còn mỗi phép gán chỉ nằm trong hợp.

3. Chạy ví dụ và kiểm tra trường hợp rỗng

Mã liệt kê tất cả nghiệm rồi tính hợp và giao. Nếu bài toán vô nghiệm, chương trình báo riêng, tránh đưa ra một danh sách “tất yếu” từ phép tính trên tập rỗng. Cài gói clingo trước khi chạy. Với bài toán lớn, nên dùng chế độ suy luận hoặc kiểm tra phản ví dụ của bộ giải thay cho lưu toàn bộ nghiệm vào bộ nhớ.

Cài thư viện bằng python -m pip install clingo nếu môi trường chưa có Clingo.

Chạy ví dụ bằng python asp_suy_luan_tat_yeu.py.

import clingo

def liet_ke(chuong_trinh):
    bo_giai = clingo.Control(["0"])
    bo_giai.add("base", [], chuong_trinh)
    bo_giai.ground([("base", [])])
    nghiem = []
    ket_qua = bo_giai.solve(on_model=lambda m: nghiem.append(set(map(str, m.symbols(shown=True)))))
    if not ket_qua.satisfiable:
        raise ValueError("Bài toán vô nghiệm")
    return nghiem

nghiem = liet_ke("""
ca(1..2). lop(a).
1 { xep(L,C) : ca(C) } 1 :- lop(L).
#show lop/1.
#show xep/2.
""")
co_the = set.union(*nghiem)
tat_yeu = set.intersection(*nghiem)
assert len(nghiem) == 2
assert co_the == {"lop(a)", "xep(a,1)", "xep(a,2)"}
assert tat_yeu == {"lop(a)"}
print("Có thể", sorted(co_the), "| Tất yếu", sorted(tat_yeu))

4. Xác định rõ tập lịch đang xét

Cần phân biệt mọi lịch khả thi với mọi lịch tối ưu. Một nguyên tử có thể không bắt buộc trên toàn tập khả thi nhưng xuất hiện trong tất cả lịch có chi phí nhỏ nhất. Trước khi công bố kết luận, ghi rõ mục tiêu, ngưỡng chi phí và việc quá trình suy luận đã hoàn tất hay bị ngắt. Nếu mới duyệt một phần, hợp mới chỉ chứa các khả năng đã tìm thấy và giao chưa bảo đảm là kết luận cuối.

Đọc thêm Tài liệu và bộ giải Clingo.