"""Dùng giả định trong Clingo để giải thích một xung đột."""
from clingo import Control, Function

PROGRAM = """
lop(a;b). ca(1..3).
1 { xep(L,C) : ca(C) } 1 :- lop(L).
{ bat(a_co_dinh); bat(b_co_dinh); bat(chung_phong); bat(a_tranh_ca3) }.
:- bat(a_co_dinh), not xep(a,1).
:- bat(b_co_dinh), not xep(b,1).
:- bat(chung_phong), xep(a,C), xep(b,C).
:- bat(a_tranh_ca3), xep(a,3).
#show xep/2.
"""


def build():
    ctl = Control()
    ctl.add("base", [], PROGRAM)
    ctl.ground([("base", [])])
    return ctl


def solve(ctl, enabled, on_core=None):
    return ctl.solve(assumptions=[(key, True) for key in enabled], on_core=on_core)


if __name__ == "__main__":
    ctl = build()
    labels = {atom.literal: atom.symbol
              for atom in ctl.symbolic_atoms.by_signature("bat", 1)}
    keys = list(labels.values())
    cores = []
    assert solve(ctl, keys, on_core=cores.append).unsatisfiable
    core = [labels[lit] for lit in cores[-1]]
    for key in core[:]:
        trial = [other for other in core if other != key]
        if solve(ctl, trial).unsatisfiable:
            core = trial
    names = sorted(key.arguments[0].name for key in core)
    print("Nhóm xung đột tối tiểu:", names)
    assert names == ["a_co_dinh", "b_co_dinh", "chung_phong"]
    assert all(solve(ctl, [other for other in core if other != key]).satisfiable
               for key in core)