resolution_refutation.py

import argparse


Literal = tuple[str, bool]
Clause = frozenset[Literal]


def parse_literal(token: str) -> Literal:
    token = token.strip()
    if not token:
        raise ValueError("Empty literal found in clause")

    if token.startswith("!"):
        return token[1:].strip(), True

    return token, False


def negate_literal(literal: Literal) -> Literal:
    symbol, is_negated = literal
    return symbol, not is_negated


def parse_clause(expression: str) -> Clause:
    expression = expression.strip().replace(" ", "")
    if not expression:
        raise ValueError("Empty clause found in input")

    literals = [parse_literal(token) for token in expression.split("|")]
    return frozenset(literals)


def read_problem(path: str) -> tuple[list[Clause], Clause]:
    with open(path, "r", encoding="utf-8") as file:
        lines = [line.strip() for line in file if line.strip()]

    if len(lines) < 2:
        raise ValueError("Input must contain a clause count, knowledge base, and query")

    clause_count = int(lines[0])
    expected_line_count = clause_count + 2

    if len(lines) != expected_line_count:
        raise ValueError(
            f"Expected {expected_line_count} non-empty lines, found {len(lines)}"
        )

    knowledge_base = [parse_clause(line) for line in lines[1 : clause_count + 1]]
    query = parse_clause(lines[clause_count + 1])

    return knowledge_base, query


def negate_query(query: Clause) -> list[Clause]:
    return [frozenset([negate_literal(literal)]) for literal in sorted(query)]


def is_tautology(clause: Clause) -> bool:
    return any(negate_literal(literal) in clause for literal in clause)


def resolve_pair(left: Clause, right: Clause) -> list[Clause]:
    resolvents = []

    for literal in left:
        complement = negate_literal(literal)
        if complement not in right:
            continue

        resolvent = (left - {literal}) | (right - {complement})
        if not is_tautology(resolvent):
            resolvents.append(frozenset(resolvent))

    return resolvents


def format_literal(literal: Literal) -> str:
    symbol, is_negated = literal
    return f"!{symbol}" if is_negated else symbol


def format_clause(clause: Clause) -> str:
    if not clause:
        return "{}"

    return " | ".join(format_literal(literal) for literal in sorted(clause))


def resolution_refutation(clauses: list[Clause], show_steps: bool = True) -> bool:
    known_clauses = list(dict.fromkeys(clauses))
    step = 1

    while True:
        new_clauses = []

        for left_index, left_clause in enumerate(known_clauses):
            for right_clause in known_clauses[left_index + 1 :]:
                for resolvent in resolve_pair(left_clause, right_clause):
                    if resolvent in known_clauses or resolvent in new_clauses:
                        continue

                    if show_steps:
                        print(
                            f"{step}: RESOLVE ({format_clause(left_clause)}) "
                            f"and ({format_clause(right_clause)}) "
                            f"=> {format_clause(resolvent)}"
                        )
                    step += 1

                    if not resolvent:
                        return True

                    new_clauses.append(resolvent)

        if not new_clauses:
            return False

        known_clauses.extend(new_clauses)


def prove(path: str, show_steps: bool = True) -> bool:
    knowledge_base, query = read_problem(path)
    clauses = knowledge_base + negate_query(query)
    return resolution_refutation(clauses, show_steps=show_steps)


def main() -> None:
    parser = argparse.ArgumentParser(
        description="Prove propositional entailment using resolution refutation."
    )
    parser.add_argument(
        "input_file",
        nargs="?",
        default="input.txt",
        help="Path to the input file. Defaults to input.txt.",
    )
    parser.add_argument(
        "--quiet",
        action="store_true",
        help="Only print the final entailment result.",
    )
    args = parser.parse_args()

    result = prove(args.input_file, show_steps=not args.quiet)
    print(1 if result else 0)


if __name__ == "__main__":
    main()