Kiểm chứng hai mã hóa ASP bằng đối chiếu nghiệm

1. Cùng điểm tối ưu chưa đủ để tin hai mã hóa tương đương

Khi thay ràng buộc cặp bằng một biểu thức đếm, ta có thể kỳ vọng mô hình nhỏ hơn hoặc dễ bảo trì hơn. Một lỗi đổi ngưỡng có thể cho phép thêm nhiều lịch sai nhưng vẫn giữ nguyên điểm tối ưu trên vài ví dụ. Vì vậy trước khi so hiệu năng, cần kiểm tra hai cách viết mô tả cùng tập phương án trong phạm vi bài toán đã định.

Chọn bài toán tô màu đồ thị nhỏ. Mỗi lớp phải chọn đúng một ca. Hai lớp nối cạnh không được có cùng ca. Một mã hóa cấm trực tiếp hai nguyên tử xep cùng đúng. Mã hóa còn lại đếm hai nguyên tử ứng với cùng ca và cấm khi số đếm đạt ít nhất hai.

2. Chiếu nghiệm lên biến quyết định nghiệp vụ

Các mã hóa có thể dùng những nguyên tử phụ khác nhau. Nếu so toàn bộ answer set, sự khác biệt ở phần phụ có thể làm hai mô hình trông khác dù lịch gán hoàn toàn giống nhau. Hãy chiếu lên xep/2, sắp theo mã lớp và đưa kết quả về một biểu diễn chuẩn. Sau đó so tập lịch, đồng thời kiểm tra mọi lớp có đúng một ca.

Trường hợp không cạnh cho phép mọi phép gán. Tam giác với hai ca không có nghiệm. Đồ thị hai đỉnh và một cạnh có đúng hai lịch với hai ca. Các trường hợp này làm mốc trước khi thêm mẫu ngẫu nhiên. Dùng thêm một oracle vét cạn độc lập để giảm nguy cơ hai mã hóa cùng mắc một lỗi.

3. Tìm phản ví dụ tự động trên dữ liệu vi mô

"""So sánh tập lịch đã chiếu của hai mã hóa với oracle vét cạn."""
from itertools import combinations, product
from random import Random
import clingo

PAIR = ":- canh(A,B), xep(A,C), xep(B,C)."
COUNT = ":- canh(A,B), ca(C), 2 { xep(A,C); xep(B,C) }."


def solve(n, colors, edges, encoding):
    data = f"lop(1..{n}). ca(1..{colors})." + "".join(
        f"canh({a},{b})." for a, b in edges
    )
    ctl = clingo.Control(["0", "--warn=none"])
    ctl.add("base", [], data + """
        1 { xep(L,C) : ca(C) } 1 :- lop(L).
        #show xep/2.
    """ + encoding)
    ctl.ground([("base", [])])
    result = set()
    with ctl.solve(yield_=True) as handle:
        for model in handle:
            positions = sorted((s.arguments[0].number, s.arguments[1].number)
                               for s in model.symbols(shown=True))
            result.add(tuple(c for _, c in positions))
        handle.get()
    return result


def oracle(n, colors, edges):
    return {row for row in product(range(1, colors + 1), repeat=n)
            if all(row[a - 1] != row[b - 1] for a, b in edges)}


if __name__ == "__main__":
    rng = Random(2026)
    cases = [(3, 2, [(1, 2), (1, 3), (2, 3)]), (3, 3, [])]
    for n in range(2, 6):
        for colors in (2, 3):
            edges = [pair for pair in combinations(range(1, n + 1), 2)
                     if rng.random() < 0.5]
            cases.append((n, colors, edges))
    for n, colors, edges in cases:
        expected = oracle(n, colors, edges)
        assert solve(n, colors, edges, PAIR) == expected
        assert solve(n, colors, edges, COUNT) == expected
    mutant = COUNT.replace("2 {", "3 {")
    assert solve(2, 2, [(1, 2)], mutant) - oracle(2, 2, [(1, 2)]) == {(1, 1), (2, 2)}
    print("Đối chiếu", len(cases), "bộ dữ liệu. Đột biến ngưỡng 3 bị phát hiện.")

Chạy python asp_kiem_chung_hai_ma_hoa.py sau khi cài gói clingo. Mã đối chiếu mười bộ dữ liệu và tạo một đột biến đổi ngưỡng đếm từ 2 thành 3. Vì biểu thức chỉ có hai nguyên tử, ngưỡng 3 không đạt được. Hai lịch trùng ca của đồ thị hai đỉnh trở thành phản ví dụ.

Khi có khác biệt, lưu instance, tập phương án chỉ xuất hiện ở một bên và lịch kiểm chứng. Thu nhỏ số lớp hoặc cạnh nhưng giữ khác biệt để tìm quy tắc gây lỗi. Bảng số đếm có thể hữu ích để theo dõi, song cần ít nhất một lịch cụ thể để người viết mô hình tái hiện.

4. Chuyển từ kiểm chứng vi mô sang so sánh hiệu năng

Kiểm tra trên miền nhỏ giúp tìm phản ví dụ, còn lập luận tương đương phải dựa vào ngữ nghĩa của hai điều kiện. Với bài này, do có đúng hai nguyên tử trong thân biểu thức đếm, điều kiện “đạt 2” đúng đúng lúc cả hai cùng đúng. Nếu sau này bổ sung thêm nguyên tử vào tập đếm, lập luận đó cần được xem lại.

Khi có tối ưu, so riêng tập khả thi, giá trị hàm mục tiêu cho cùng lịch và tập nghiệm tối ưu nếu kích thước cho phép. Chỉ sau bước kiểm chứng mới so thời gian, bộ nhớ hoặc khả năng chứng minh tối ưu. Xem ngữ nghĩa biểu thức đếm tại tài liệu ngôn ngữ Clingo.