"""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.")