Mô hình ổn định trong ASP từ phép rút gọn

1. Khi một tập nguyên tử thỏa luật vẫn chưa là nghiệm

Trong ASP, ta mô tả dữ kiện và quy tắc rồi hỏi chương trình chấp nhận những tập nguyên tử nào. Xét a :- a.. Nếu chỉ đọc luật như một mệnh đề kéo theo, tập {a} thỏa luật. Tuy nhiên, luật này chỉ lặp lại giả định rằng a đã đúng. Theo ngữ nghĩa mô hình ổn định, chương trình có mô hình ổn định là tập rỗng.

Điểm khó xuất hiện khi thân luật có not. Trong các chương trình normal đang xét, not b kiểm tra việc b vắng mặt trong một tập ứng viên. Tập ứng viên lại là thứ ta đang tìm. Phép rút gọn Gelfond–Lifschitz cho phép cố định một ứng viên rồi kiểm tra xem chương trình có tái tạo được chính ứng viên đó hay không.

2. Ba bước của phép rút gọn

1. Chọn một tập nguyên tử ứng viên M. Với mỗi luật có not x trong thân và x thuộc M, loại cả luật.
2. Trong các luật còn lại, bỏ các literal phủ định mặc định. Chương trình dương thu được gọi là phép rút gọn theo M.
3. Tính mô hình nhỏ nhất của chương trình dương bằng cách bắt đầu từ tập rỗng, thêm các kết luận có thân đã thỏa và lặp tới khi không có nguyên tử mới. Nếu kết quả bằng M, ứng viên là mô hình ổn định.

Xét hai luật đối xứng dưới đây. Chọn M = {a}. Luật kết luận b bị loại vì có not a. Luật kết luận a còn lại và trở thành sự kiện a. Phép rút gọn sinh đúng {a}, nên tập này ổn định. Thử tương tự cho {b}.

a :- not b.
b :- not a.

3. Tự cài một bộ kiểm tra trên ví dụ nhỏ

Mã Python dưới đây biểu diễn mỗi luật bằng đầu luật, tập điều kiện dương và tập nguyên tử dưới not. Chương trình duyệt mọi tập ứng viên để người học thấy rõ từng bước. Cách vét cạn này phù hợp với ví dụ ít nguyên tử. Khi mô hình lớn hơn, hãy dùng một bộ giải ASP.

"""Tính mô hình ổn định của chương trình ground normal nhỏ.

Mỗi luật là (đầu, thân dương, thân phủ định mặc định).
Ví dụ a :- b, not c. được viết ("a", {"b"}, {"c"}).
"""
from itertools import combinations


def reduct(program, candidate):
    return [(head, positive) for head, positive, negative in program
            if negative.isdisjoint(candidate)]


def least_model(positive_program):
    model = set()
    while True:
        consequences = {head for head, body in positive_program if body <= model}
        if consequences <= model:
            return model
        model.update(consequences)


def stable_models(program):
    atoms = sorted(set().union(*(positive | negative | {head}
                                for head, positive, negative in program)))
    models = []
    for size in range(len(atoms) + 1):
        for atoms_subset in combinations(atoms, size):
            candidate = set(atoms_subset)
            if least_model(reduct(program, candidate)) == candidate:
                models.append(candidate)
    return models


if __name__ == "__main__":
    examples = [
        ("Phủ định đối xứng", [("a", set(), {"b"}), ("b", set(), {"a"})]),
        ("Tự hỗ trợ", [("a", {"a"}, set())]),
        ("Phủ định chính nó", [("a", set(), {"a"})]),
        ("Có sự kiện làm căn cứ", [("a", set(), set()), ("b", {"a"}, set())]),
    ]
    for label, program in examples:
        models = stable_models(program)
        readable = ["{" + ", ".join(sorted(model)) + "}" for model in models]
        print(f"{label}: " + (" | ".join(readable) if readable else "không có nghiệm"))

    assert stable_models(examples[0][1]) == [{"a"}, {"b"}]
    assert stable_models(examples[1][1]) == [set()]
    assert stable_models(examples[2][1]) == []
    assert stable_models(examples[3][1]) == [{"a", "b"}]

Chạy python mo_hinh_on_dinh.py. Ví dụ phủ định đối xứng có hai mô hình. Luật tự hỗ trợ có đúng một mô hình là tập rỗng. Luật a :- not a. không có mô hình ổn định. Hai kết quả cuối khác nhau. Một trường hợp có một nghiệm nhưng nghiệm không chứa nguyên tử nào, trường hợp kia không có nghiệm.

4. Đọc kết quả ASP trong bài toán xếp lịch

Khi biểu diễn xep(Lop,Ca), cần có luật sinh phương án hoặc dữ kiện tạo ra phép gán. Một chuỗi luật chỉ lặp lại các giả định về phép gán sẽ không tự sinh lịch. Sau bước sinh, dùng ràng buộc toàn vẹn để loại các phương án trùng tài nguyên. Với dữ liệu lớn, tách rõ tầng sinh ứng viên, tầng kiểm tra và tầng chấm điểm giúp xác định lỗi ở tầng nào khi kết quả trái dự đoán.

Bài tập. Thêm sự kiện a. vào chương trình đối xứng và dự đoán số mô hình. Sau đó xét a :- b. cùng b :- a. khi không có sự kiện. Vì sao hai luật hỗ trợ lẫn nhau vẫn cho tập rỗng?

Đọc thêm về công trình Gelfond và Lifschitz (1988) và Potassco Guide.