"""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"}]