Chọn tập sửa lỗi theo số thay đổi hay chi phí thay đổi

1. Tập sửa cần chạm vào mọi nhóm xung đột

Giả sử hai nhóm điều kiện gây xung đột là {a,b} và {b,c}. Muốn phá cả hai nhóm, một tập điều kiện được nới phải giao với mỗi nhóm. Tập {b} làm được điều đó bằng một thay đổi. Tập {a,c} cũng làm được, nhưng dùng hai thay đổi. Đây là bài toán tập chạm trên những nhóm xung đột đã biết.

2. Ba tiêu chí có thể chọn khác nhau

Một tập tối tiểu theo bao hàm không cho bỏ riêng phần tử nào mà vẫn sửa được mọi nhóm. Cả {b} và {a,c} đều thỏa tính chất này. Chọn ít phần tử nhất sẽ lấy {b}. Nếu chi phí nới b là 5, còn a và c mỗi điều kiện là 1, chọn tổng chi phí nhỏ nhất lại lấy {a,c}, với chi phí 2.

3. Dùng hai phép kiểm chứng độc lập

Mã Python vét cạn tập con để xác định các tập tối tiểu theo bao hàm. Phần Clingo tối thiểu hóa tổng chi phí và kiểm tra kết quả cuối. Khi đặt các trọng số trong biểu thức tối ưu, giữ mã điều kiện trong tuple để hai khoản bằng trọng số vẫn được cộng riêng. Giá trị chi phí ở đây là dữ liệu giả lập dùng giải thích cách chọn.

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_chon_tap_sua_loi.py.

from itertools import combinations
import clingo

nhan = {"a", "b", "c"}
xung_dot = [{"a", "b"}, {"b", "c"}]
tap_sua = [
    set(chon)
    for co in range(4)
    for chon in combinations(sorted(nhan), co)
    if all(set(chon) & nhom for nhom in xung_dot)
]
toi_tieu = [chon for chon in tap_sua if not any(khac < chon for khac in tap_sua)]
assert sorted(map(sorted, toi_tieu)) == [["a", "c"], ["b"]]

ctl = clingo.Control(["0"])
ctl.add("base", [], """
nhan(a;b;c).
gia(a,1). gia(b,5). gia(c,1).
{ bo(X) } :- nhan(X).
:- not bo(a), not bo(b).
:- not bo(b), not bo(c).
#minimize { W,X : bo(X), gia(X,W) }.
#show bo/1.
""")
ctl.ground([("base", [])])
nghiem = []
ctl.solve(on_model=lambda m: nghiem.append((set(map(str, m.symbols(shown=True))), list(m.cost))))
assert nghiem[-1] == ({"bo(a)", "bo(c)"}, [2])
print("Theo bao hàm", sorted(map(sorted, toi_tieu)), "| Theo chi phí", nghiem[-1])

4. Kiểm tra lại lịch sau khi nới

Chạm vào các nhóm đã biết là điều kiện cần để phá những nguyên nhân đó, nhưng có thể còn nhóm xung đột chưa được phát hiện. Sau khi áp dụng một tập sửa, phải giải lại mô hình gốc với các thay đổi đã chọn. Nếu vẫn vô nghiệm, thu thêm thông tin xung đột và lặp lại. Quyết định nới một quy định còn cần người có thẩm quyền nghiệp vụ duyệt.

Đọc thêm Tài liệu tối ưu trong ASP của Potassco.