Giải thích lịch vô nghiệm bằng giả thiết trong Clingo

1. Biến thông báo vô nghiệm thành một câu hỏi nghiệp vụ

Khi bộ giải báo vô nghiệm, người điều phối cần biết nhóm quy định nào xung đột. Ví dụ hai lớp cùng cần một phòng, cả hai bị ghim vào ca 1 và một lớp còn bị cấm ca 3. Điều kiện cấm ca 3 có mặt trong dữ liệu nhưng không tạo ra xung đột chính. Ta muốn tìm nhóm gồm ghim A, ghim B và dùng chung phòng.

Một cách tổ chức mô hình là gắn nguyên tử bat(Ma) cho mỗi điều kiện cần giải thích. Mỗi nguyên tử được phép chọn hoặc bỏ. Ở lượt chẩn đoán, truyền các nguyên tử cần bật dưới dạng giả định. Điều kiện không có trong tập giả định có thể tắt, nên bộ giải được phép tìm lịch khi nới nó.

2. Đọc đúng ý nghĩa của lõi vô nghiệm

Lõi vô nghiệm là một tập con các giả định đủ để duy trì vô nghiệm trong mô hình nền. Lõi trả về ban đầu có thể chứa giả định thừa. Có thể thử bỏ từng phần tử. Nếu phần còn lại vẫn vô nghiệm, bỏ phần tử đó khỏi lõi. Kết quả cuối là tối tiểu theo bao hàm, nghĩa là bỏ bất kỳ phần tử nào cũng làm nhóm đó khả thi.

Tối tiểu theo bao hàm chưa bảo đảm số phần tử nhỏ nhất trong mọi lõi. Ví dụ một instance có hai nhóm xung đột độc lập, một nhóm gồm hai điều kiện và nhóm kia gồm ba. Thuật toán rút gọn có thể trả nhóm ba nếu lõi ban đầu không chứa nhóm hai. Khi công bố kết quả, ghi cách rút gọn và tính chất thực sự đã kiểm tra.

3. Lấy lõi bằng API giả định của Clingo

"""Dùng giả định trong Clingo để giải thích một xung đột."""
from clingo import Control, Function

PROGRAM = """
lop(a;b). ca(1..3).
1 { xep(L,C) : ca(C) } 1 :- lop(L).
{ bat(a_co_dinh); bat(b_co_dinh); bat(chung_phong); bat(a_tranh_ca3) }.
:- bat(a_co_dinh), not xep(a,1).
:- bat(b_co_dinh), not xep(b,1).
:- bat(chung_phong), xep(a,C), xep(b,C).
:- bat(a_tranh_ca3), xep(a,3).
#show xep/2.
"""


def build():
    ctl = Control()
    ctl.add("base", [], PROGRAM)
    ctl.ground([("base", [])])
    return ctl


def solve(ctl, enabled, on_core=None):
    return ctl.solve(assumptions=[(key, True) for key in enabled], on_core=on_core)


if __name__ == "__main__":
    ctl = build()
    labels = {atom.literal: atom.symbol
              for atom in ctl.symbolic_atoms.by_signature("bat", 1)}
    keys = list(labels.values())
    cores = []
    assert solve(ctl, keys, on_core=cores.append).unsatisfiable
    core = [labels[lit] for lit in cores[-1]]
    for key in core[:]:
        trial = [other for other in core if other != key]
        if solve(ctl, trial).unsatisfiable:
            core = trial
    names = sorted(key.arguments[0].name for key in core)
    print("Nhóm xung đột tối tiểu:", names)
    assert names == ["a_co_dinh", "b_co_dinh", "chung_phong"]
    assert all(solve(ctl, [other for other in core if other != key]).satisfiable
               for key in core)

Chạy python asp_unsat_assumptions.py với gói clingo. Hàm nhận lõi trả các literal của chương trình. Mã ánh xạ literal về nguyên tử bat/1, sau đó chuyển thành mã điều kiện nghiệp vụ. Sau khi rút gọn, chương trình chạy lại khi bỏ từng phần tử để xác nhận cả ba đều cần thiết trong nhóm.

Trong ví dụ, điều kiện được bảo vệ bằng luật chọn để có thể bật hoặc tắt. Nếu viết bat(a_co_dinh). thành fact cố định, bỏ nó khỏi danh sách giả định vẫn không tắt được điều kiện. Đây là lỗi thiết kế dễ gặp khi đưa lõi vào một chương trình đang có nhiều dữ kiện cứng.

4. Dùng giải thích mà vẫn bảo toàn quy trình kiểm chứng

Thử thêm một nhóm xung đột độc lập và chạy lại với thứ tự giả định khác nhau. Ghi số lõi, số lượt giải bổ sung và khả năng truy ngược tới dòng dữ liệu. Nếu lượt giải bị dừng mà không chứng minh khả thi hoặc vô nghiệm, cần lưu trạng thái chưa kết luận và tránh tuyên bố lõi đã tối tiểu.

Giải thích là căn cứ để đề xuất nới một điều kiện. Một phương án sửa phải được kiểm tra lại trên toàn bộ ràng buộc còn áp dụng. Nếu mô hình nền đã vô nghiệm trước khi bật bất cứ giả định nào, hãy kiểm tra dữ liệu và các điều kiện nền trước. Xem thêm Clingo Python API · assumptions và on_core.