"""SAT verification and a SAT-to-independent-set reduction. Python 3.10+, stdlib."""
from __future__ import annotations
from itertools import product, combinations


def verify(clauses, assignment):
    """Pre: nonzero signed literals reference assignment indices 1..n. Post: CNF truth."""
    if any(lit == 0 or abs(lit) > len(assignment) for clause in clauses for lit in clause):
        raise ValueError("literal references an undefined variable")
    return all(any(assignment[abs(lit)-1] == (lit > 0) for lit in clause) for clause in clauses)


def solve(clauses, n):
    """Pre: n>=0 and valid literals. Post: a satisfying witness, or None."""
    if n < 0:
        raise ValueError("number of variables must be nonnegative")
    # Invariant: no earlier assignment satisfied all clauses. Bound: remaining 2**n assignments.
    for assignment in product((False, True), repeat=n):
        if verify(clauses, assignment):
            return assignment
    return None


def reduce_to_independent_set(clauses):
    """Pre: finite clauses. Post: one vertex/occurrence and conflict edges, target=len(clauses)."""
    vertices = [(clause_index, literal) for clause_index, clause in enumerate(clauses) for literal in clause]
    edges = set()
    # Invariant: every earlier vertex pair has its correct conflict status.
    # Bound: remaining unordered vertex pairs.
    for a, b in combinations(range(len(vertices)), 2):
        if vertices[a][0] == vertices[b][0] or vertices[a][1] == -vertices[b][1]:
            edges.add((a, b))
    return vertices, edges, len(clauses)


def independent_set(size, edges, target):
    """Pre: finite simple graph, target>=0. Post: target-sized independent witness or None."""
    # Invariant: previous vertex subsets fail; bound: remaining binomial(size,target) subsets.
    for subset in combinations(range(size), target):
        if all((a, b) not in edges for a, b in combinations(subset, 2)):
            return subset
    return None


def demo():
    clauses = [(1, -2, 3), (-1, 2, 3), (1, 2, -3)]
    witness = solve(clauses, 3)
    vertices, edges, target = reduce_to_independent_set(clauses)
    subset = independent_set(len(vertices), edges, target)
    print("SAT witness:", witness, "verified:", verify(clauses, witness))
    print("Reduction:", len(vertices), "vertices;", len(edges), "edges; target", target)
    print("Independent-set witness:", subset)
    print("Exhaustive small-instance solving does not settle P vs NP.")


def self_test():
    import random
    rng, count = random.Random(7), 0
    # Invariant: previous reductions preserve satisfiability in both directions.
    # Bound: remaining 40 finite formulas.
    for _ in range(40):
        clauses = [tuple(rng.choice((-1, 1))*rng.randrange(1, 4) for _ in range(3)) for _ in range(3)]
        witness = solve(clauses, 3)
        vertices, edges, target = reduce_to_independent_set(clauses)
        graph_yes = independent_set(len(vertices), edges, target) is not None
        check(graph_yes, witness is not None)
        if witness is not None:
            check(verify(clauses, witness), True)
        count += 1
    check(solve([()], 0), None)
    check(solve([], 0), ())
    return count + 2

def check(actual, expected):
    """Require an expected result; this check also runs under python -O."""
    if actual != expected:
        raise AssertionError(f"expected {expected!r}, got {actual!r}")


if __name__ == "__main__":
    import argparse
    parser = argparse.ArgumentParser(description=__doc__)
    parser.add_argument("--self-test", action="store_true")
    args = parser.parse_args()
    if args.self_test:
        print(f"{self_test()} checks passed")
    else:
        demo()