Đệ quy trong ASP và chu trình thiếu điểm xuất phát

1. Vì sao chu trình chưa đủ tạo ra kết luận

Xét hai cặp đỉnh có cạnh đi qua lại, a–b và c–d. Chương trình chỉ cho a là điểm đã tới. Một người đọc luật như quan hệ kéo theo có thể thử gán cả c và d là đã tới, vì hai đỉnh hỗ trợ lẫn nhau trên hình. Với phần chương trình dương trong ví dụ, nghiệm ổn định lấy tập suy ra nhỏ nhất từ các fact, nên chu trình không nối với nguồn chưa tạo thêm đỉnh.

2. Theo dõi phép đóng từng bước

Bắt đầu với toi(a). Cạnh a → b suy ra toi(b). Cạnh b → a chỉ dẫn về nguyên tử đã có. Không có bước nào kích hoạt cạnh thuộc cụm c–d, vì cả hai thân luật liên quan đều thiếu điểm đã tới. Phép lặp dừng khi tập nguyên tử không đổi. Ta có thể dùng quá trình này làm oracle tay cho chương trình rất nhỏ.

3. Đối chiếu với Clingo

Mẫu Python chạy hai chương trình. Lượt đầu có đúng một nghiệm với a và b. Lượt thứ hai thêm toi(c), khiến d được suy ra và cả bốn đỉnh xuất hiện. Lấy bản sao tập nguyên tử ngay trong callback, vì đối tượng Model chỉ hợp lệ trong phạm vi mà API cho phép.

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

import clingo

chuong_trinh = """
canh(a,b). canh(b,a). canh(c,d). canh(d,c).
toi(a).
toi(Y) :- toi(X), canh(X,Y).
#show toi/1.
"""

def tap_toi(nguon_bo_sung=""):
    bo_giai = clingo.Control(["0"])
    bo_giai.add("base", [], chuong_trinh + nguon_bo_sung)
    bo_giai.ground([("base", [])])
    nghiem = []
    bo_giai.solve(on_model=lambda m: nghiem.append({str(a) for a in m.symbols(shown=True)}))
    assert len(nghiem) == 1
    return nghiem[0]

assert tap_toi() == {"toi(a)", "toi(b)"}
assert tap_toi("toi(c).") == {"toi(a)", "toi(b)", "toi(c)", "toi(d)"}
print("Chu trình c–d chỉ được tới sau khi bổ sung nguồn c.")

4. Chuyển sang bài toán thực

Trong lập lịch, đóng bắc cầu có thể biểu diễn quan hệ tiên quyết hoặc các nhóm liên quan qua nhiều bước. Hãy phân biệt quan hệ suy ra với quan hệ quyết định được phép chọn. Nếu thay luật suy ra bằng luật lựa chọn, tập phương án thay đổi. Bộ kiểm chứng nên có ca nguồn rỗng, nguồn nằm ngoài chu trình và nguồn nằm trong chu trình để phát hiện việc thêm kết luận thiếu căn cứ.

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