"""Sửa lịch theo ba cấp ưu tiên và đối chiếu bằng oracle vét cạn."""
from itertools import product
import clingo

PROGRAM = r"""
course(a;b;c). slot(1..2). room(r1;r2).
teacher(a,g1). teacher(b,g1). teacher(c,g2).
old(a,1,r1). old(b,2,r1). old(c,1,r2).
1 { at(L,S,R) : slot(S), room(R) } 1 :- course(L).
:- at(L,S,R), at(M,S,R), L < M.
:- at(L,S,R), at(M,S,Q), teacher(L,G), teacher(M,G), L < M.
:- closed(S,R), at(L,S,R).
:- fixed(L), old(L,S,R), not at(L,S,R).
time_changed(L) :- at(L,S,R), old(L,T,Q), S != T.
room_changed(L) :- at(L,S,R), old(L,T,Q), R != Q.
changed(L) :- time_changed(L).
changed(L) :- room_changed(L).
#minimize { 1@3,L : changed(L); 1@2,L : time_changed(L); 1@1,L : room_changed(L) }.
#show at/3.
"""
OLD = ((1, "r1"), (2, "r1"), (1, "r2"))

def score(schedule):
    times = sum(x[0] != y[0] for x, y in zip(schedule, OLD))
    rooms = sum(x[1] != y[1] for x, y in zip(schedule, OLD))
    return (sum(x != y for x, y in zip(schedule, OLD)), times, rooms)

def solve(extra):
    ctl = clingo.Control(["0", "--opt-mode=optN", "--warn=none"])
    ctl.add("base", [], PROGRAM + extra)
    ctl.ground([("base", [])])
    found = set()
    def collect(model):
        if not model.optimality_proven:
            return
        rows = {str(a.arguments[0]): (a.arguments[1].number, str(a.arguments[2]))
                for a in model.symbols(shown=True)}
        schedule = tuple(rows[l] for l in ("a", "b", "c"))
        assert tuple(model.cost) == score(schedule)
        found.add(schedule)
    result = ctl.solve(on_model=collect)
    assert result.exhausted and not result.interrupted
    return found

def oracle(frozen):
    feasible = []
    positions = list(product((1, 2), ("r1", "r2")))
    for s in product(positions, repeat=3):
        if any(p == (1, "r1") for p in s):
            continue
        if len(set(s)) < 3 or s[0][0] == s[1][0]:
            continue
        if any(s[i] != OLD[i] for i in frozen):
            continue
        feasible.append(s)
    best = min(map(score, feasible), default=None)
    return {s for s in feasible if score(s) == best}

repair = solve("closed(1,r1). fixed(b).")
assert repair == oracle({1}) == {((1, "r2"), (2, "r1"), (2, "r2"))}
assert score(next(iter(repair))) == (2, 1, 1)
assert solve("closed(1,r1). fixed(b). fixed(c).") == oracle({1, 2}) == set()
print("Lịch sửa tối ưu:", sorted(repair))
print("Vector (lớp đổi, lớp đổi ca, lớp đổi phòng): (2, 1, 1)")
print("Đóng băng cả B và C: vô nghiệm; cần xét lại phạm vi được sửa.")