from itertools import product


Literal = tuple  # ("P", True) or ("P", False)
Clause = frozenset  # frozenset of Literal


def negate(literal):
    name, positive = literal
    return (name, not positive)


def resolve(ci, cj):
    resolvents = set()
    for li in ci:
        for lj in cj:
            if li == negate(lj):
                new_clause = (ci - {li}) | (cj - {lj})
                resolvents.add(frozenset(new_clause))
    return resolvents


def pl_resolution(clauses):
    """Refutation-complete resolution over a set of CNF clauses.

    Returns True if the clause set is unsatisfiable (derives the
    empty clause), False if resolution saturates without doing so.
    """
    clauses = set(clauses)
    new = set()
    while True:
        pairs = [
            (ci, cj) for ci in clauses for cj in clauses if ci != cj
        ]
        for ci, cj in pairs:
            resolvents = resolve(ci, cj)
            if frozenset() in resolvents:
                return True  # empty clause: contradiction found
            new |= resolvents
        if new.issubset(clauses):
            return False  # saturated: no new information, satisfiable
        clauses |= new


def entails(premise_clauses, query_literal):
    """Test premise |= query via refutation: premise ∧ ¬query unsat?"""
    negated_query = frozenset({negate(query_literal)})
    return pl_resolution(set(premise_clauses) | {negated_query})


if __name__ == "__main__":
    # Knowledge base: (P ∨ Q), (¬P ∨ R), (¬Q ∨ R)  =>  R must hold
    kb = {
        frozenset({("P", True), ("Q", True)}),
        frozenset({("P", False), ("R", True)}),
        frozenset({("Q", False), ("R", True)}),
    }
    print("KB entails R:", entails(kb, ("R", True)))     # True
    print("KB entails ¬R:", entails(kb, ("R", False)))   # False
