Phủ định mặc định, phủ định mạnh và dữ liệu chưa biết

1. Không có dữ liệu đóng phòng chưa có nghĩa phòng đang mở

Một hệ thống xếp lịch nhận dữ liệu từ ba bộ phận: danh mục phòng, lịch bảo trì và xác nhận khả dụng. Phòng A được xác nhận mở. Phòng B được xác nhận đóng. Phòng C có trong danh mục nhưng chưa nhận được phản hồi. Nếu người lập trình chỉ kiểm tra “không tìm thấy thông báo đóng”, A và C đều trở thành ứng viên. Nếu quy định yêu cầu xác nhận mở trước khi xếp lớp, chỉ A được sử dụng. Hai kết quả đều có thể xuất phát từ một chương trình chạy đúng cú pháp; khác biệt nằm ở chính sách đối với dữ liệu chưa biết.

Bài này phân tích sự khác nhau giữa phủ định mặc định not p và phủ định mạnh -p trên Clingo 5.8.x. Mục đích là thiết kế hợp đồng dữ liệu, không gắn mặc định một chính sách cho mọi trường. Khi dữ liệu liên quan đến phòng chuyên dụng, thiết bị an toàn hoặc ca di chuyển giữa cơ sở, sự im lặng của nguồn dữ liệu cần được diễn giải rõ trước khi mô hình hóa.

2. Tách sự thật được ghi nhận khỏi cách suy luận

Dùng mo(a). để ghi nhận A mở và -mo(b). để ghi nhận B không mở. Không thêm thông tin nào về trạng thái của C. Trong một answer set cụ thể, not mo(c) được thỏa khi mo(c) không có trong tập đó. Điều này không tự sinh nguyên tử -mo(c). Muốn chuyển sự vắng mặt thành kết luận đóng, ta phải viết thêm quy tắc và chịu trách nhiệm về giả thiết đóng thế giới ấy.

Ba nhãn “mở”, “đóng” và “chưa biết” ở đây là cách ứng dụng tổ chức thông tin. Chúng không có nghĩa Clingo tự thay mọi phép đánh giá bằng một logic ba giá trị. Bên trong một answer set, mỗi nguyên tử được xét theo ngữ nghĩa của chương trình. Trạng thái chưa biết được ứng dụng nhận diện khi cả nguyên tử khẳng định và nguyên tử phủ định mạnh đều vắng mặt.

3. Hai chính sách tạo hai miền ứng viên khác nhau

duoc_mac_dinh(R) :- phong(R), not -mo(R).
duoc_xac_nhan(R) :- phong(R), mo(R).
chua_biet(R) :- phong(R), not mo(R), not -mo(R).

Quy tắc thứ nhất chấp nhận mọi phòng chưa có thông tin phủ định mạnh. Đây là chính sách nới: một phần bất định được giữ trong miền. Quy tắc thứ hai yêu cầu bằng chứng khẳng định. Đây là chính sách thận trọng hơn đối với nguồn thông tin đang xét. Quy tắc thứ ba phục vụ báo cáo, giúp người điều phối biết còn thiếu xác nhận ở đâu. Nhãn báo cáo không tự loại một phòng; việc loại hay giữ cần được thể hiện ở quan hệ ứng viên dùng trong luật chọn lịch.

Biến R được giới hạn bởi phong(R). Nếu viết một quy tắc chỉ có not -mo(R) mà không có miền dương thích hợp, ta chưa cho grounder một tập phòng để xét. Vấn đề an toàn biến khác với quyết định nghiệp vụ “phòng chưa biết có được dùng hay không”. Một mô hình có thể an toàn về biến nhưng vẫn dùng chính sách không phù hợp.

4. Theo dõi điều gì thay đổi khi bổ sung thông tin

Thêm mo(c). khiến C được xác nhận mở. Tập ứng viên mặc định vẫn gồm A và C, nhưng tập ứng viên có xác nhận mở tăng từ một lên hai. Nhãn chưa biết của C biến mất. Nếu thay bằng -mo(c)., C bị loại khỏi cả hai chính sách và cũng không còn là trường hợp chưa biết. Đây là hai thông tin mới khác nhau, không phải hai cách viết tương đương của việc “đã xử lý C”.

Một quy tắc hoàn thiện dữ liệu như -mo(R) :- phong(R), not mo(R). tuy ngắn nhưng mang quyết định đáng kể: mọi phòng thiếu xác nhận mở đều được suy ra là không mở. Trong ví dụ, C chuyển sang trạng thái đóng theo chính sách. Nếu nguồn xác nhận cập nhật chậm, quy tắc có thể làm mất nhiều ứng viên và dẫn tới vô nghiệm. Kết luận vô nghiệm khi đó gắn với cả dữ liệu lẫn chính sách hoàn thiện, không chỉ với số phòng vật lý.

5. Chạy ví dụ và đọc các khẳng định

Cài môi trường bằng python -m pip install "clingo==5.8.3", lưu mã nguồn bên dưới rồi chạy python asp_phu_dinh_va_chua_biet.py. Tệp Python chứa toàn bộ chương trình ASP, không cần tạo thêm tệp LP. Hàm thu nghiệm sao chép tên các nguyên tử ngay trong callback, sau đó mới so với tập kết quả mong đợi.

"""Python 3.10+, clingo 5.8.x. Chạy: python asp_phu_dinh_va_chua_biet.py"""
import clingo

PROGRAM = r"""
phong(a;b;c).
mo(a). -mo(b).
duoc_mac_dinh(R) :- phong(R), not -mo(R).
duoc_xac_nhan(R) :- phong(R), mo(R).
chua_biet(R) :- phong(R), not mo(R), not -mo(R).
:- mo(R), -mo(R).
#show duoc_mac_dinh/1.
#show duoc_xac_nhan/1.
#show chua_biet/1.
"""

def models(extra=""):
    ctl = clingo.Control(["0", "--warn=none"])
    ctl.add("base", [], PROGRAM + extra)
    ctl.ground([("base", [])])
    found = []
    result = ctl.solve(on_model=lambda m: found.append(
        {str(atom) for atom in m.symbols(shown=True)}))
    assert result.exhausted and not result.interrupted
    return found

initial = models()
assert initial == [{"duoc_mac_dinh(a)", "duoc_mac_dinh(c)",
                    "duoc_xac_nhan(a)", "chua_biet(c)"}]
confirmed = models("mo(c).")
assert "duoc_xac_nhan(c)" in confirmed[0]
assert "chua_biet(c)" not in confirmed[0]
closed_world = models("-mo(R) :- phong(R), not mo(R).")
assert closed_world == [{"duoc_mac_dinh(a)", "duoc_xac_nhan(a)"}]
assert models("-mo(a).") == []
print("Ban đầu:", sorted(initial[0]))
print("Bổ sung mo(c):", sorted(confirmed[0]))
print("Đóng thế giới:", sorted(closed_world[0]))
print("Dữ liệu mâu thuẫn mo(a), -mo(a): vô nghiệm.")

Bốn phép kiểm tra chính lần lượt xác nhận trạng thái ban đầu, bổ sung thông tin mở cho C, áp dụng quy tắc đóng thế giới và phát hiện dữ liệu mâu thuẫn. Ràng buộc :- mo(R), -mo(R). viết rõ yêu cầu nhất quán: một phòng không đồng thời được xem là mở và không mở trong cùng mô hình. Trường hợp mâu thuẫn không được sửa bằng cách âm thầm ưu tiên dữ kiện đến sau; thứ tự dòng dữ liệu không phải một cơ chế giải quyết xung đột.

6. Khi nhiều nguồn đưa thông tin khác nhau

Trong triển khai thực tế, nên lưu nguồn, khoảng hiệu lực và thời điểm cập nhật trước khi suy ra mo hoặc -mo. Hai thông báo “B đóng tuần 3” và “B mở tuần 4” không mâu thuẫn nếu chúng nói về các tuần khác nhau. Ngược lại, gộp tất cả vào một vị từ không có thời gian sẽ biến hai thông tin hợp lệ thành xung đột giả. Có thể mở rộng thành mo(Phong,Tuan,Ca) rồi dùng cùng phạm vi trong mọi quy tắc.

Khi có nguồn ưu tiên, cần đặc tả quy tắc hợp nhất riêng. Ví dụ, lịch bảo trì đã phê duyệt có thể thắng thông báo mở mặc định, nhưng không nên mặc nhiên thắng một xác nhận phục hồi được duyệt sau đó nếu nghiệp vụ không quy định như vậy. Một hướng nghiên cứu là đo mức thiếu dữ liệu và số lịch còn khả thi dưới nhiều chính sách hợp nhất, đồng thời giữ lại thông tin nào đã khiến từng ứng viên bị loại.

7. Bài tập và câu hỏi nghiên cứu

Thêm hai tuần học. Cho C mở tuần 1 và đóng tuần 2; A vẫn chưa có xác nhận tuần 2. Dự đoán tập ứng viên dưới hai chính sách rồi mới chạy. Tiếp theo, thêm một lớp chỉ dùng được C trong tuần 2. Hãy giải thích vì sao “không đủ phòng đã xác nhận” khác với “không tồn tại phòng phù hợp trong thực tế”. Báo cáo cần nói đúng miền tri thức mà mô hình đang sử dụng.

Để nghiên cứu chính sách dữ liệu thiếu, cố định một bộ lịch đầy đủ, chủ động che một phần xác nhận và so sánh tỷ lệ giữ được lịch, số yêu cầu cần người dùng xác minh và số phương án bị bác khi dữ liệu hoàn chỉnh trở lại. Các kết quả này cần được kiểm tra trên dữ liệu tách riêng; ví dụ ba phòng trong bài chỉ minh họa ngữ nghĩa, không phải bằng chứng một chính sách luôn tốt hơn.

Nguồn đối chiếu: Gelfond và Lifschitz, Classical Negation in Logic Programs and Disjunctive Databases; Potassco Guide cho dòng Clingo 5. Đọc tiếp Mô hình ổn định từ phép rút gọn.