diff --git a/wizard-work/null/satkit-2026-10-26/README.md b/wizard-work/null/satkit-2026-10-26/README.md new file mode 100644 index 0000000..065dead --- /dev/null +++ b/wizard-work/null/satkit-2026-10-26/README.md @@ -0,0 +1,113 @@ +# satkit verification — 11 legs, independent oracle, 4 mutants killed + +`satkit.py` is a stdlib-only CDCL SAT solver (watched literals, VSIDS, 1UIP +learning, Luby restarts) with an RUP proof log and a separately written RUP +checker. It was shipped with no test suite. This directory is that suite, plus +the two real defects it found and the fix. + +Files +----- +| file | role | +|---|---| +| `satkit.py` | the solver + checker (two checker bugs fixed here, see below) | +| `verify_satkit.py` | the suite: 11 legs, exit 0 iff all pass | +| `show_defects.py` | reproduces both pre-fix defects against the shipped code | +| `README.md` | this record | + +Run +--- +``` +python3 verify_satkit.py # 11/11 legs, ~3.4 s, exit 0 +python3 show_defects.py # both defects reproduced pre-fix, absent post-fix, exit 0 +``` + +The suite never grades `satkit` with `satkit`: + +* SAT/UNSAT is decided by exhaustive brute force on small instances (a model is + the certificate either way), and by *refutation* on large ones; +* every proof step is re-derived by `oracle_rup()` inside `verify_satkit.py`, a + textbook unit-propagation implementation that shares no code with the checker + it is auditing; +* models are checked by `satisfies()`, not by `satkit.model_satisfies`; +* the suite itself is attacked: four sabotaged copies of `satkit` must each fail + the leg aimed at them, or the run is red. + +Defects found (measured, not inferred) +------------------------------------- +Both were in `RupChecker`. Both were found by differential fuzzing against the +textbook oracle — 4 disagreements in the first 18 random proof sequences. + +**D1 — unsound: a satisfied clause reported as a conflict.** +`_propagate()` treated "`len(c)-1` literals false and no unassigned literal" as a +conflict, but that state also occurs when the remaining literal is *true*. The +checker therefore accepted proofs of formulas that have models: + +``` +F = [(-3,),(-2,),(2,1,3),(-1,5,4),(-2,5,3),(-3,-4),(1,),(-2,4,5),(5,),(2,4,-3)] +brute-force model: [1,-2,-3,-4,5] (model_satisfies -> True) +pre-fix check_proof(5, F, [()]) -> ok=True "all 1 steps RUP-checked" <- wrong +shipped check_proof(5, F, [()]) -> ok=False "step 0 rejected: not RUP" +``` + +**D2 — incomplete: `nfalse[]` driven negative.** +`_undo()` decremented the false-literal counter for every trail literal, including +literals never visited because propagation returned early on a conflict. The +counters went negative and later clauses could never reach "all false", blinding +the checker. Consequence: valid 1UIP refutations were rejected. + +``` +PHP(4,3) 4 pigeons / 3 holes, solver says UNSAT with a 7-step refutation +pre-fix accepted=False at step 1 (5 clauses at nfalse=-1 after step 0) +shipped accepted=True after 7 steps +``` + +Fix (two hunks, both in `satkit.py`): the `len(c)-1` branch now `continue`s when +the last non-false literal is true, and `_undo()` decrements only the clause +indices recorded in `self.touched` during propagation. + +Post-fix: 6000 random proof sequences, 0 false accepts, 0 false rejects against +the textbook oracle. + +Legs and what each one actually measured +--------------------------------------- +``` +edge_cases PASS 0.00s 7 degenerate cases +exhaustive_n2 PASS 0.01s n=2: 247 formulas (152 unsat), all agreed +exhaustive_n3 PASS 0.16s n=3: 4048 formulas (813 unsat), all agreed +random_sweep PASS 0.58s 1200 random CNFs: 458 sat / 742 unsat, models and refutations verified +php_proofs PASS 1.63s PHP(3,2) 2 steps; PHP(4,3) 7; PHP(5,4) 28; PHP(6,5) 145; PHP(7,6) 765 +random3sat_proofs PASS 0.83s 6 instances n=70 ratio 4.3: 2 sat (models ok) / 4 unsat (refutations ok) +oracle_selfcheck PASS 0.05s 535 model-falsified candidates, oracle never claimed RUP +negative_controls PASS 0.00s 5 forged proofs all rejected +cross_process PASS 0.13s child emitted a 7-step proof; parent oracle + checker both accept +determinism PASS 0.00s identical sat/model/proof across repeat runs +mutant_control PASS 0.00s 4/4 mutants killed +11/11 legs passed in 3.40s +``` + +* `exhaustive_n2/n3` enumerate **every** formula over all non-tautological clauses + of width ≤ 2 up to 6 (resp. 4) clauses — 4295 formulas, not a sample. +* `negative_controls` is the leg that would have caught D1: forged empty clause on + a satisfiable formula, a refutation built from the negation of a known model, a + truncated refutation, a genuine refutation transplanted onto a weaker + satisfiable formula, and a provably non-RUP step spliced into step 0. +* `mutant_control` kills: `flipped_sat` (caught by `exhaustive_n2`), + `all_positive_model` (`random_sweep`), `short_proof` (`php_proofs`), + `lax_checker` (`negative_controls`). A green run means those legs have teeth. + +Scope — what this does *not* establish +------------------------------------- +* RUP only. The checker is sound and complete for RUP steps; a valid proof that + needed RAT (clause addition by resolution on a pivot, used by some DRAT + producers) would be rejected. `satkit` emits RUP steps only, so this does not + affect it, but the checker is not a general DRAT checker. +* Exhaustive agreement covers n ≤ 3; n ≤ 10 is sampled (1200 CNFs), and larger + instances are covered only where a refutation or a model certifies the answer. + There is no completeness test on satisfiable large instances beyond the models + returned. +* Refutation checking is a soundness certificate: a checked RUP proof ending in + the empty clause proves UNSAT. A rejected proof proves nothing about the + formula — only that this producer's proof was bad. +* `show_defects.py` reconstructs the pre-fix methods by subclassing, so the + "before" column is a faithful copy of the shipped pre-fix code, not a rerun of + an old checkout. diff --git a/wizard-work/null/satkit-2026-10-26/satkit.py b/wizard-work/null/satkit-2026-10-26/satkit.py new file mode 100644 index 0000000..be1070c --- /dev/null +++ b/wizard-work/null/satkit-2026-10-26/satkit.py @@ -0,0 +1,533 @@ +#!/usr/bin/env python3 +"""satkit -- CDCL SAT solver with RUP/DRAT-style proof logging and an +independent RUP proof checker. Stdlib only. + +Literals are nonzero ints: +v / -v for variable v in 1..nvars. + +Public API +---------- +solve(nvars, clauses, proof_out=None) -> SolveResult + SolveResult(sat, model, proof, stats) + sat : True / False + model : list of ints (1..nvars) when sat, else None + proof : list of clauses (learned, ending with [] for UNSAT) when unsat + stats : dict of counters + +check_proof(nvars, clauses, proof) -> ProofResult + ProofResult(ok, steps_checked, message) + +The two halves are deliberately independent implementations: + * the solver uses two watched literals, VSIDS activity, 1UIP conflict + analysis, non-chronological backjumping and Luby restarts; + * the checker uses occurrence lists and per-clause false-counters, never + touches solver state, and re-derives every step by unit propagation. + +A proof step C is accepted iff F & ~C unit-propagates to a conflict (RUP). +An UNSAT proof must terminate with the empty clause. +""" + +from __future__ import annotations + +__all__ = ["solve", "check_proof", "SolveResult", "ProofResult", "brute_force_sat"] + + +# -------------------------------------------------------------------------- +# helpers +# -------------------------------------------------------------------------- +def normalize(lits): + """Dedupe, drop tautologies. Returns None for a tautology, else a tuple.""" + seen = set() + out = [] + for l in lits: + if -l in seen: + return None + if l in seen: + continue + seen.add(l) + out.append(l) + return tuple(out) + + +class SolveResult: + __slots__ = ("sat", "model", "proof", "stats") + + def __init__(self, sat, model, proof, stats): + self.sat = sat + self.model = model + self.proof = proof + self.stats = stats + + def __repr__(self): + return "SolveResult(sat=%r, model=%r, stats=%r)" % ( + self.sat, self.model, self.stats) + + +class ProofResult: + __slots__ = ("ok", "steps_checked", "message") + + def __init__(self, ok, steps_checked, message): + self.ok = ok + self.steps_checked = steps_checked + self.message = message + + def __bool__(self): + return self.ok + + def __repr__(self): + return "ProofResult(ok=%r, steps=%d, msg=%r)" % ( + self.ok, self.steps_checked, self.message) + + +# -------------------------------------------------------------------------- +# CDCL solver +# -------------------------------------------------------------------------- +class Solver: + def __init__(self, nvars, clauses, collect_proof=True): + self.n = nvars + self.collect_proof = collect_proof + self.clauses = [] # watched lits held at positions 0 and 1 + self.watches = [[] for _ in range(2 * nvars)] + self.assign = [0] * (nvars + 1) # 0 unassigned / 1 true / -1 false + self.level = [0] * (nvars + 1) + self.reason = [-1] * (nvars + 1) + self.seen = [False] * (nvars + 1) + self.trail = [] + self.trail_lim = [] + self.qhead = 0 + self.activity = [0.0] * (nvars + 1) + self.phase = [-1] * (nvars + 1) + self.var_inc = 1.0 + self.var_decay = 0.95 + self.ok = True + self.proof = [] + self.stats = {"conflicts": 0, "decisions": 0, "propagations": 0, + "restarts": 0, "learned": 0, "max_level": 0} + for c in clauses: + if not self.add_input_clause(c): + break + + # -- literal helpers --------------------------------------------------- + @staticmethod + def _widx(lit): + return 2 * (abs(lit) - 1) + (0 if lit > 0 else 1) + + def val(self, lit): + a = self.assign[abs(lit)] + return a if lit > 0 else -a + + # -- clause database --------------------------------------------------- + def add_input_clause(self, lits): + c = normalize(lits) + if c is None: # tautology: carries no information + return True + if len(c) == 0: + self.ok = False + return False + if len(c) == 1: + if self.enqueue(c[0], -1) is False: + self.ok = False + return False + return True + ci = len(self.clauses) + self.clauses.append(list(c)) + self.watches[self._widx(c[0])].append(ci) + self.watches[self._widx(c[1])].append(ci) + return True + + def add_learned_clause(self, lits): + """Watch lits[0], lits[1]; lits[0] must be the asserting literal.""" + ci = len(self.clauses) + self.clauses.append(list(lits)) + self.watches[self._widx(lits[0])].append(ci) + self.watches[self._widx(lits[1])].append(ci) + return ci + + # -- assignment -------------------------------------------------------- + def enqueue(self, lit, reason): + v = abs(lit) + cur = self.assign[v] + if cur != 0: + return (cur > 0) == (lit > 0) + self.assign[v] = 1 if lit > 0 else -1 + self.level[v] = len(self.trail_lim) + self.reason[v] = reason + self.trail.append(lit) + return True + + def new_decision_level(self): + self.trail_lim.append(len(self.trail)) + + @property + def decision_level(self): + return len(self.trail_lim) + + def backtrack(self, lvl): + if self.decision_level <= lvl: + return + cut = self.trail_lim[lvl] + for i in range(len(self.trail) - 1, cut - 1, -1): + lit = self.trail[i] + v = abs(lit) + self.phase[v] = 1 if lit > 0 else -1 + self.assign[v] = 0 + self.reason[v] = -1 + self.level[v] = 0 + del self.trail[cut:] + del self.trail_lim[lvl:] + self.qhead = len(self.trail) + + # -- unit propagation -------------------------------------------------- + def propagate(self): + """Returns a conflicting clause index, or None.""" + assign, level, clauses = self.assign, self.level, self.clauses + watches = self.watches + while self.qhead < len(self.trail): + p = self.trail[self.qhead] + self.qhead += 1 + self.stats["propagations"] += 1 + false_lit = -p + ws = watches[self._widx(false_lit)] + i = 0 + while i < len(ws): + ci = ws[i] + c = clauses[ci] + if c[0] == false_lit: + c[0], c[1] = c[1], c[0] + if c[1] != false_lit: + raise RuntimeError("watch invariant broken on clause %d" % ci) + first = c[0] + if self.val(first) > 0: + i += 1 + continue + moved = False + for k in range(2, len(c)): + if self.val(c[k]) >= 0: # unassigned or true + c[1], c[k] = c[k], c[1] + watches[self._widx(c[1])].append(ci) + ws[i] = ws[-1] + ws.pop() + moved = True + break + if moved: + continue + if self.val(first) < 0: + return ci + if not self.enqueue(first, ci): + return ci + i += 1 + return None + + # -- VSIDS ------------------------------------------------------------- + def bump(self, v): + self.activity[v] += self.var_inc + if self.activity[v] > 1e100: + for i in range(1, self.n + 1): + self.activity[i] *= 1e-100 + self.var_inc *= 1e-100 + + def pick_branch(self): + best, best_act = 0, -1.0 + for v in range(1, self.n + 1): + if self.assign[v] == 0 and self.activity[v] > best_act: + best, best_act = v, self.activity[v] + return best + + # -- 1UIP conflict analysis ------------------------------------------- + def analyze(self, confl): + seen = self.seen + for v in range(1, self.n + 1): + seen[v] = False + learned = [0] + pathc = 0 + p = 0 + idx = len(self.trail) - 1 + ci = confl + cur = self.decision_level + while True: + c = self.clauses[ci] + start = 0 if p == 0 else 1 # skip the implied literal (at [0]) + for q in c[start:]: + v = abs(q) + if not seen[v] and self.level[v] > 0: + seen[v] = True + self.bump(v) + if self.level[v] == cur: + pathc += 1 + else: + learned.append(q) + while idx >= 0 and not seen[abs(self.trail[idx])]: + idx -= 1 + if idx < 0: + raise RuntimeError("analyze: ran off the trail") + p = self.trail[idx] + idx -= 1 + seen[abs(p)] = False + pathc -= 1 + if pathc == 0: + break + ci = self.reason[abs(p)] + if ci < 0: + raise RuntimeError("analyze: no reason for implied literal") + learned[0] = -p + # backtrack level = second highest level in the clause + if len(learned) == 1: + bt = 0 + else: + bt = 0 + best_i = 1 + for i in range(1, len(learned)): + lv = self.level[abs(learned[i])] + if lv > bt: + bt, best_i = lv, i + learned[1], learned[best_i] = learned[best_i], learned[1] + return learned, bt + + # -- search ------------------------------------------------------------ + def solve(self): + if not self.ok: + if self.collect_proof: + self.proof.append([]) + return SolveResult(False, None, self.proof, self.stats) + confl = self.propagate() + if confl is not None: + if self.collect_proof: + self.proof.append([]) + return SolveResult(False, None, self.proof, self.stats) + + restart_no = 1 + budget = 100 * _luby(2, restart_no) + conflicts_here = 0 + while True: + confl = self.propagate() + if confl is not None: + self.stats["conflicts"] += 1 + conflicts_here += 1 + if self.decision_level == 0: + if self.collect_proof: + self.proof.append([]) + return SolveResult(False, None, self.proof, self.stats) + learned, bt = self.analyze(confl) + self.backtrack(bt) + if len(learned) == 1: + self.enqueue(learned[0], -1) + else: + ci = self.add_learned_clause(learned) + self.enqueue(learned[0], ci) + self.stats["learned"] += 1 + if self.collect_proof: + self.proof.append(list(learned)) + self.var_inc /= self.var_decay + if conflicts_here >= budget: + self.backtrack(0) + self.stats["restarts"] += 1 + restart_no += 1 + conflicts_here = 0 + budget = 100 * _luby(2, restart_no) + continue + v = self.pick_branch() + if v == 0: + model = [v2 if self.assign[v2] > 0 else -v2 + for v2 in range(1, self.n + 1)] + return SolveResult(True, model, None, self.stats) + self.stats["decisions"] += 1 + self.new_decision_level() + lit = v if self.phase[v] > 0 else -v + self.enqueue(lit, -1) + if self.decision_level > self.stats["max_level"]: + self.stats["max_level"] = self.decision_level + + +def _luby(y, x): + """MiniSat's luby sequence: 1,1,2,1,1,2,4,... for y=2.""" + size, seq = 1, 0 + while size < x + 1: + seq += 1 + size = 2 * size + 1 + while size - 1 != x: + size = (size - 1) >> 1 + seq -= 1 + x = x % size + return y ** seq + + +def solve(nvars, clauses, collect_proof=True): + return Solver(nvars, clauses, collect_proof).solve() + + +# -------------------------------------------------------------------------- +# independent RUP proof checker (occurrence lists + false-counters) +# -------------------------------------------------------------------------- +class RupChecker: + def __init__(self, nvars, clauses): + self.n = nvars + self.clauses = [] # normalized tuples + self.occ = {} # literal -> [clause index] + self.nfalse = [] + self.taut = [] + self.units = [] + self.has_empty = False + self.val = [0] * (nvars + 1) + self.trail = [] + self.touched = [] # clause indices whose nfalse was incremented + self.qhead = 0 + for c in clauses: + norm = normalize(c) + if norm is None: + continue + self._db_add(norm) + + def _db_add(self, norm): + ci = len(self.clauses) + self.clauses.append(norm) + for l in norm: + self.occ.setdefault(l, []).append(ci) + self.nfalse.append(0) + if len(norm) == 0: + self.has_empty = True + elif len(norm) == 1: + self.units.append(norm[0]) + return ci + + # -- temporary assignment layer --------------------------------------- + def _assume(self, lit): + """Returns False on contradiction with the current temporary trail.""" + v = abs(lit) + cur = self.val[v] + if cur != 0: + return (cur > 0) == (lit > 0) + self.val[v] = 1 if lit > 0 else -1 + self.trail.append(lit) + return True + + def _propagate(self): + """True iff a clause became fully false.""" + clauses, occ, nfalse = self.clauses, self.occ, self.nfalse + while self.qhead < len(self.trail): + p = self.trail[self.qhead] + self.qhead += 1 + for ci in occ.get(-p, ()): + nfalse[ci] += 1 + self.touched.append(ci) + c = clauses[ci] + if nfalse[ci] == len(c): + return True + if nfalse[ci] == len(c) - 1: + unit = 0 + for l in c: + if self.val[abs(l)] == 0: + unit = l + break + if unit == 0: + # the single non-false literal is TRUE: clause satisfied + continue + if not self._assume(unit): + return True + return False + + def _undo(self): + # Undo exactly the increments that happened. Walking the trail instead + # would decrement clauses never visited when propagation returned early, + # driving nfalse[] negative and silently blinding later steps. + for ci in self.touched: + self.nfalse[ci] -= 1 + self.touched = [] + for p in self.trail: + self.val[abs(p)] = 0 + self.trail = [] + self.qhead = 0 + + # -- one proof step ---------------------------------------------------- + def check_step(self, lits): + norm = normalize(lits) + if norm is None: + return True, "tautology (vacuously RUP)" + conflict = self.has_empty + if not conflict: + for u in self.units: + if not self._assume(u): + conflict = True + break + if not conflict: + for l in norm: + if not self._assume(-l): + conflict = True + break + if not conflict: + conflict = self._propagate() + self._undo() + if not conflict: + return False, "not RUP: unit propagation reached a fixpoint with no conflict" + self._db_add(norm) + return True, "rup" + + +def check_proof(nvars, clauses, proof, require_empty=True): + """Verify a RUP proof. Every step must be RUP w.r.t. clauses + earlier steps. + + require_empty: the proof must end with the empty clause (UNSAT claim). + """ + chk = RupChecker(nvars, clauses) + if not proof: + return ProofResult(False, 0, "empty proof") + for i, step in enumerate(proof): + ok, why = chk.check_step(step) + if not ok: + return ProofResult(False, i, "step %d rejected: %s" % (i, why)) + if require_empty: + last = normalize(proof[-1]) + if last is None or len(last) != 0: + return ProofResult(False, len(proof), + "proof does not end with the empty clause") + return ProofResult(True, len(proof), "all %d steps RUP-checked" % len(proof)) + + +# -------------------------------------------------------------------------- +# reference oracle (exponential; only for tiny instances) +# -------------------------------------------------------------------------- +def brute_force_sat(nvars, clauses): + """Return a model (list of +-v) or None. Exhaustive, no cleverness.""" + norm = [] + for c in clauses: + n = normalize(c) + if n is None: + continue + norm.append(n) + if len(n) == 0: + return None + for mask in range(1 << nvars): + ok = True + for c in norm: + sat = False + for l in c: + v = abs(l) + bit = (mask >> (v - 1)) & 1 + if (bit == 1) == (l > 0): + sat = True + break + if not sat: + ok = False + break + if ok: + return [v if (mask >> (v - 1)) & 1 else -v for v in range(1, nvars + 1)] + return None + + +def model_satisfies(nvars, clauses, model): + """Independent model check against the raw clause list.""" + val = {} + for lit in model: + val[abs(lit)] = lit > 0 + if len(val) != nvars: + return False + for c in clauses: + if not any(val.get(abs(l)) == (l > 0) for l in c): + return False + return True + + +if __name__ == "__main__": + # tiny demo + cls = [[1, 2], [-1, 2], [1, -2], [-1, -2]] + r = solve(2, cls) + print("demo sat=%r model=%r stats=%r" % (r.sat, r.model, r.stats)) + print("proof check:", check_proof(2, cls, r.proof)) diff --git a/wizard-work/null/satkit-2026-10-26/show_defects.py b/wizard-work/null/satkit-2026-10-26/show_defects.py new file mode 100644 index 0000000..3b51cdb --- /dev/null +++ b/wizard-work/null/satkit-2026-10-26/show_defects.py @@ -0,0 +1,138 @@ +#!/usr/bin/env python3 +"""show_defects.py -- reproduce the two checker defects found in satkit.py, and show +that the shipped checker no longer has them. + +The pre-fix behaviour is reconstructed by subclassing satkit.RupChecker with the +two original methods (verbatim from the code before the fix), so this runs against +one copy of satkit.py and needs no second checkout. + +D1 (unsound) : a clause that is SATISFIED but has exactly len-1 false literals was + reported as a conflict, so the checker accepted proofs of formulas + that are satisfiable. +D2 (incomplete) : _undo() decremented nfalse[] for every trail literal, including ones + never visited when propagation returned early. nfalse[] went negative, + which blinded later steps, so a valid 1UIP refutation was rejected at + its second step. + +Exit 0 iff the old behaviour is reproduced AND the shipped behaviour is correct. +""" + +from __future__ import annotations + +import os +import sys + +HERE = os.path.dirname(os.path.abspath(__file__)) +if HERE not in sys.path: + sys.path.insert(0, HERE) + +import satkit + + +# -------------------------------------------------------------------------- +# the two methods exactly as they were before the fix +# -------------------------------------------------------------------------- +class PreFixChecker(satkit.RupChecker): + def _propagate(self): + clauses, occ, nfalse = self.clauses, self.occ, self.nfalse + while self.qhead < len(self.trail): + p = self.trail[self.qhead] + self.qhead += 1 + for ci in occ.get(-p, ()): + nfalse[ci] += 1 + c = clauses[ci] + if nfalse[ci] == len(c): + return True + if nfalse[ci] == len(c) - 1: + unit = 0 + for l in c: + if self.val[abs(l)] == 0: + unit = l + break + if unit == 0: + return True # BUG D1: this may be a satisfied clause + if not self._assume(unit): + return True + return False + + def _undo(self): + for p in reversed(self.trail): + for ci in self.occ.get(-p, ()): + self.nfalse[ci] -= 1 # BUG D2: decrements clauses never touched + self.val[abs(p)] = 0 + self.trail = [] + self.qhead = 0 + + +def check_with(cls, nvars, clauses, proof, require_empty=True): + chk = cls(nvars, clauses) + if not proof: + return False, 0, "empty proof" + for i, step in enumerate(proof): + ok, why = chk.check_step(step) + if not ok: + return False, i, "step %d rejected: %s" % (i, why) + if require_empty: + last = satkit.normalize(proof[-1]) + if last is None or len(last) != 0: + return False, len(proof), "no empty clause" + return True, len(proof), "accepted" + + +def php(holes, pigeons): + def v(p, h): + return p * holes + h + 1 + cl = [tuple(v(p, h) for h in range(holes)) for p in range(pigeons)] + for h in range(holes): + for p1 in range(pigeons): + for p2 in range(p1 + 1, pigeons): + cl.append((-v(p1, h), -v(p2, h))) + return pigeons * holes, cl + + +def main(): + failures = 0 + + print("D1 -- forged empty clause on a SATISFIABLE formula") + F = [(-3,), (-2,), (2, 1, 3), (-1, 5, 4), (-2, 5, 3), (-3, -4), (1,), (-2, 4, 5), (5,), (2, 4, -3)] + model = satkit.brute_force_sat(5, F) + print(" F is satisfiable, model %r (verified %r)" + % (model, satkit.model_satisfies(5, F, model))) + old_ok, _, old_msg = check_with(PreFixChecker, 5, F, [()]) + new_ok, _, new_msg = check_with(satkit.RupChecker, 5, F, [()]) + print(" pre-fix checker : accepted=%r (%s)" % (old_ok, old_msg)) + print(" shipped checker : accepted=%r (%s)" % (new_ok, new_msg)) + if not old_ok: + print(" !! defect D1 not reproduced -- this record is stale") + failures += 1 + if new_ok: + print(" !! shipped checker still unsound") + failures += 1 + + print("\nD2 -- valid 1UIP refutation of PHP(4,3) (4 pigeons, 3 holes)") + n, cl = php(3, 4) + r = satkit.solve(n, cl) + print(" solver: sat=%r, %d proof steps" % (r.sat, len(r.proof))) + old_ok, old_i, old_msg = check_with(PreFixChecker, n, cl, r.proof) + print(" pre-fix checker : accepted=%r at step %d (%s)" % (old_ok, old_i, old_msg)) + chk = PreFixChecker(n, cl) + chk.check_step(r.proof[0]) + negatives = sum(1 for x in chk.nfalse if x < 0) + print(" nfalse[] after one step: %d clauses negative (min %d) -> propagation blinded" + % (negatives, min(chk.nfalse))) + new_ok, new_i, new_msg = check_with(satkit.RupChecker, n, cl, r.proof) + print(" shipped checker : accepted=%r after %d steps (%s)" % (new_ok, new_i, new_msg)) + if old_ok or negatives == 0: + print(" !! defect D2 not reproduced -- this record is stale") + failures += 1 + if not new_ok: + print(" !! shipped checker still rejects valid refutations") + failures += 1 + + print("\n%s" % ("both defects reproduced pre-fix and absent post-fix" + if failures == 0 else "%d assertion(s) failed" % failures)) + return 0 if failures == 0 else 1 + + +if __name__ == "__main__": + sys.exit(main()) diff --git a/wizard-work/null/satkit-2026-10-26/verify_satkit.py b/wizard-work/null/satkit-2026-10-26/verify_satkit.py new file mode 100644 index 0000000..dd58dcc --- /dev/null +++ b/wizard-work/null/satkit-2026-10-26/verify_satkit.py @@ -0,0 +1,562 @@ +#!/usr/bin/env python3 +"""verify_satkit.py -- adversarial verification of satkit.py (CDCL solver + RUP proof checker). + +Nothing here trusts satkit for its own grade: + + * satisfiability is decided against an exhaustive oracle (brute force) on small + instances and against *proofs* on large ones; + * every proof step is re-checked by a unit-propagation implementation that lives + in this file (``oracle_rup``) and shares no code with satkit's checker; + * the checker is attacked with forged proofs it must reject; + * the suite itself is attacked: deliberately broken copies of satkit must fail + the leg aimed at them, otherwise a green run would mean nothing. + +Legs +---- + 1 edge_cases degenerate inputs (0 vars, empty clause, no clauses) + 2 exhaustive_n2 every formula over the 8 clauses of width<=2 on 2 vars, <=6 clauses + 3 exhaustive_n3 every formula over the 18 clauses of width<=2 on 3 vars, <=4 clauses + 4 random_sweep 1200 random CNFs, n<=10: sat/model/proof vs oracle + 5 php_proofs pigeonhole PHP(n+1,n), n=2..6: UNSAT + proof re-checked step by step + 6 random3sat_proofs 3-SAT at ratio 4.3, n=70: model or re-checked refutation + 7 oracle_selfcheck the harness oracle never calls a non-implied clause RUP + 8 negative_controls forged/truncated/transplanted proofs must be REJECTED + 9 cross_process proof produced in a child process, checked in the parent +10 determinism identical inputs -> identical sat/model/proof +11 mutant_control 4 sabotaged satkits, each must fail its designated leg + +Exit 0 iff every leg passes. stdlib only. +""" + +from __future__ import annotations + +import itertools +import json +import os +import random +import subprocess +import sys +import tempfile +import time + +HERE = os.path.dirname(os.path.abspath(__file__)) +if HERE not in sys.path: + sys.path.insert(0, HERE) + +import satkit # noqa: E402 + + +# ========================================================================== +# harness-owned primitives (deliberately independent of satkit) +# ========================================================================== +def norm_clause(lits): + """Dedupe; None for a tautology; () for the empty clause.""" + seen = set() + out = [] + for l in lits: + if -l in seen: + return None + if l in seen: + continue + seen.add(l) + out.append(l) + return tuple(out) + + +def oracle_rup(db, cand): + """Textbook RUP: db + units + the negation of cand must unit-propagate to conflict.""" + val = {} + for l in cand: + v = abs(l) + if v in val and val[v] != (l > 0): + return True # negated assumption set is contradictory + val[v] = l < 0 # assume -l + for c in db: + if len(c) == 1: + v = abs(c[0]) + if v in val and val[v] != (c[0] > 0): + return True + val[v] = c[0] > 0 + changed = True + while changed: + changed = False + for c in db: + sat, un = False, [] + for l in c: + v = abs(l) + if v not in val: + un.append(l) + elif val[v] == (l > 0): + sat = True + break + if sat: + continue + if not un: + return True # every literal false -> conflict + if len(un) == 1: + val[abs(un[0])] = un[0] > 0 + changed = True + return False + + +def oracle_check_proof(nvars, clauses, proof, require_empty=True): + """(ok, index, message) -- step-by-step RUP with the harness's own propagator.""" + db = [] + for c in clauses: + n = norm_clause(c) + if n is not None: + db.append(n) + if not proof: + return False, 0, "empty proof" + for i, step in enumerate(proof): + n = norm_clause(step) + if n is None: + continue # tautology: vacuously RUP + if not oracle_rup(db, n): + return False, i, "step %d not RUP: %r" % (i, list(step)) + db.append(n) + if require_empty: + last = norm_clause(proof[-1]) + if last is None or len(last) != 0: + return False, len(proof), "proof does not end with the empty clause" + return True, len(proof), "all %d steps RUP-checked (harness oracle)" % len(proof) + + +def satisfies(nvars, clauses, model): + """Harness-owned model check. Rejects malformed or incomplete models.""" + if model is None or len(model) != nvars: + return False + val = {} + for lit in model: + if lit == 0 or abs(lit) > nvars or abs(lit) in val: + return False + val[abs(lit)] = lit > 0 + if len(val) != nvars: + return False + for c in clauses: + n = norm_clause(c) + if n is None: + continue + if not any(val[abs(l)] == (l > 0) for l in n): + return False + return True + + +def brute_force(nvars, clauses): + """Model or None. Exhaustive; the only authority on SAT/UNSAT here.""" + cs = [] + for c in clauses: + n = norm_clause(c) + if n is None: + continue + cs.append(n) + if len(n) == 0: + return None + for mask in range(1 << nvars): + ok = True + for c in cs: + if not any(((mask >> (abs(l) - 1)) & 1) == (1 if l > 0 else 0) for l in c): + ok = False + break + if ok: + return [v if (mask >> (v - 1)) & 1 else -v for v in range(1, nvars + 1)] + return None + + +# ========================================================================== +# instance generators +# ========================================================================== +def php(holes, pigeons): + """pigeons > holes -> UNSAT. var(p,h) = p*holes + h + 1""" + def v(p, h): + return p * holes + h + 1 + cl = [tuple(v(p, h) for h in range(holes)) for p in range(pigeons)] + for h in range(holes): + for p1 in range(pigeons): + for p2 in range(p1 + 1, pigeons): + cl.append((-v(p1, h), -v(p2, h))) + return pigeons * holes, cl + + +def rand_cnf(rng, n, m, kmax=3): + cl = [] + for _ in range(m): + k = rng.randint(1, min(kmax, n)) + vs = rng.sample(range(1, n + 1), k) + cl.append(tuple(v if rng.random() < 0.5 else -v for v in vs)) + return cl + + +def rand_3sat(rng, n, ratio=4.3): + m = int(ratio * n) + cl = [] + for _ in range(m): + vs = rng.sample(range(1, n + 1), 3) + cl.append(tuple(v if rng.random() < 0.5 else -v for v in vs)) + return cl + + +# ========================================================================== +# legs -- every leg takes the module under test and returns (ok, detail) +# ========================================================================== +def leg_edge_cases(mod): + cases = [ + (0, []), # no variables, no clauses -> SAT + (0, [()]), # empty clause -> UNSAT + (1, []), # free variable -> SAT + (1, [()]), # empty clause -> UNSAT + (3, [(1, -1)]), # tautology only -> SAT + (2, [(1,), (-1,)]), # direct contradiction -> UNSAT + (2, [(1, 2), (-1,), (-2,)]), # UNSAT by propagation + ] + for n, cl in cases: + r = mod.solve(n, list(cl)) + want = brute_force(n, cl) is not None + if r.sat != want: + return False, "n=%d %r: solver sat=%r oracle=%r" % (n, cl, r.sat, want) + if r.sat: + if not satisfies(n, cl, r.model): + return False, "n=%d %r: bad model %r" % (n, cl, r.model) + if r.proof is not None: + return False, "n=%d %r: SAT answer carried a proof" % (n, cl) + else: + ok, i, msg = oracle_check_proof(n, cl, r.proof) + if not ok: + return False, "n=%d %r: refutation rejected (%s)" % (n, cl, msg) + return True, "%d degenerate cases" % len(cases) + + +def _exhaustive(mod, nvars, max_size, label): + lits = [v for v in range(1, nvars + 1)] + pool = [] + for l in lits: + pool.append((l,)) + pool.append((-l,)) + for a, b in itertools.combinations(lits, 2): + for sa in (1, -1): + for sb in (1, -1): + pool.append((sa * a, sb * b)) + pool = [c for c in pool if norm_clause(c) is not None] + total = 0 + unsat = 0 + for size in range(0, max_size + 1): + for combo in itertools.combinations(range(len(pool)), size): + cl = [pool[i] for i in combo] + r = mod.solve(nvars, cl) + want = brute_force(nvars, cl) is not None + total += 1 + if r.sat != want: + return False, "%s: %r solver=%r oracle=%r" % (label, cl, r.sat, want) + if r.sat: + if not satisfies(nvars, cl, r.model): + return False, "%s: %r bad model %r" % (label, cl, r.model) + else: + unsat += 1 + ok, i, msg = oracle_check_proof(nvars, cl, r.proof) + if not ok: + return False, "%s: %r refutation rejected (%s)" % (label, cl, msg) + return True, "%s: %d formulas (%d unsat), all agreed" % (label, total, unsat) + + +def leg_exhaustive_n2(mod): + return _exhaustive(mod, 2, 6, "n=2") + + +def leg_exhaustive_n3(mod): + return _exhaustive(mod, 3, 4, "n=3") + + +def leg_random_sweep(mod): + rng = random.Random(424242) + sat_n = unsat_n = 0 + for t in range(1200): + n = rng.randint(1, 10) + cl = rand_cnf(rng, n, rng.randint(0, 26)) + r = mod.solve(n, cl) + want = brute_force(n, cl) is not None + if r.sat != want: + return False, "case %d n=%d %r: solver=%r oracle=%r" % (t, n, cl, r.sat, want) + if r.sat: + sat_n += 1 + if not satisfies(n, cl, r.model): + return False, "case %d n=%d %r: bad model %r" % (t, n, cl, r.model) + else: + unsat_n += 1 + ok, i, msg = oracle_check_proof(n, cl, r.proof) + if not ok: + return False, "case %d n=%d %r: refutation rejected (%s)" % (t, n, cl, msg) + return True, "1200 random CNFs: %d sat / %d unsat, models and refutations verified" % (sat_n, unsat_n) + + +def leg_php_proofs(mod): + detail = [] + for holes in range(2, 7): + n, cl = php(holes, holes + 1) + t0 = time.time() + r = mod.solve(n, cl) + dt = time.time() - t0 + if r.sat: + return False, "PHP(%d,%d) reported SAT" % (holes + 1, holes) + ok, i, msg = oracle_check_proof(n, cl, r.proof) + if not ok: + return False, "PHP(%d,%d): %s" % (holes + 1, holes, msg) + if len(r.proof) < 2: + return False, "PHP(%d,%d): refutation has %d steps" % (holes + 1, holes, len(r.proof)) + detail.append("PHP(%d,%d) %d steps %.3fs" % (holes + 1, holes, len(r.proof), dt)) + return True, "; ".join(detail) + + +def leg_random3sat_proofs(mod): + rng = random.Random(90210) + sat_n = unsat_n = 0 + for seed in range(6): + n = 70 + cl = rand_3sat(rng, n) + r = mod.solve(n, cl) + if r.sat: + sat_n += 1 + if not satisfies(n, cl, r.model): + return False, "seed %d: bad model" % seed + else: + unsat_n += 1 + ok, i, msg = oracle_check_proof(n, cl, r.proof) + if not ok: + return False, "seed %d: %s" % (seed, msg) + return True, "6 instances n=70 ratio 4.3: %d sat (models ok) / %d unsat (refutations ok)" % (sat_n, unsat_n) + + +def leg_oracle_selfcheck(mod): + """RUP implies implication: if a model of F falsifies C, C must not be RUP.""" + rng = random.Random(5150) + checked = 0 + for _ in range(800): + n = rng.randint(1, 7) + cl = rand_cnf(rng, n, rng.randint(1, 10)) + model = brute_force(n, cl) + if model is None: + continue + val = {abs(l): l > 0 for l in model} + cand = tuple(-l for l in model if rng.random() < 0.5) or (model[0],) + cand = tuple(l for l in cand if True) + falsified = all(val[abs(l)] != (l > 0) for l in cand) + db = [norm_clause(c) for c in cl] + db = [c for c in db if c is not None] + if falsified and oracle_rup(db, cand): + return False, "oracle called %r RUP though model %r falsifies it" % (cand, model) + checked += 1 + return True, "%d model-falsified candidates, oracle never claimed RUP" % checked + + +def leg_negative_controls(mod): + """Forged proofs must be rejected. A checker that accepts these is worthless.""" + rejected = [] + + # (a) forged empty clause on a satisfiable formula + F = [(-3,), (-2,), (2, 1, 3), (-1, 5, 4), (-2, 5, 3), (-3, -4), (1,), (-2, 4, 5), (5,), (2, 4, -3)] + model = brute_force(5, F) + if model is None: + return False, "control (a) built on an unsatisfiable formula" + pr = mod.check_proof(5, F, [()]) + if pr.ok: + return False, "(a) checker ACCEPTED the empty clause on satisfiable F (model %r)" % (model,) + rejected.append("(a) forged [] on SAT F") + + # (b) forged refutation built from the negation of a known model + forged = [[-l] for l in model] + [()] + pr = mod.check_proof(5, F, forged) + if pr.ok: + return False, "(b) checker ACCEPTED a refutation built from the model's negation" + rejected.append("(b) model-negation refutation") + + # (c) genuine refutation, last step dropped + n, cl = php(3, 4) + r = mod.solve(n, cl) + if r.sat or not r.proof: + return False, "control (c) needs an unsat instance with a proof" + pr = mod.check_proof(n, cl, r.proof[:-1]) + if pr.ok: + return False, "(c) checker ACCEPTED a refutation with no empty clause" + rejected.append("(c) truncated refutation") + + # (d) genuine refutation transplanted onto a weaker (satisfiable) formula + weaker = [c for c in cl if c != cl[0]] + if brute_force(n, weaker) is None: + return False, "control (d): weakened formula is still unsatisfiable" + pr = mod.check_proof(n, weaker, r.proof) + if pr.ok: + return False, "(d) checker ACCEPTED a proof of a formula it does not refute" + rejected.append("(d) proof transplanted onto weaker F") + + # (e) a step that is provably not RUP, spliced into a genuine refutation + bad_step = None + for cand in ([1], [-1], [1, 2], [-1, -2], [cl[0][0]]): + if not oracle_rup([norm_clause(c) for c in cl], tuple(cand)): + bad_step = cand + break + if bad_step is None: + return False, "control (e): could not find a non-RUP clause" + spliced = [bad_step] + list(r.proof) + pr = mod.check_proof(n, cl, spliced) + if pr.ok: + return False, "(e) checker ACCEPTED a non-RUP step %r" % (bad_step,) + if pr.steps_checked != 0: + return False, "(e) rejected at step %d, expected step 0" % pr.steps_checked + rejected.append("(e) non-RUP step spliced in") + + return True, "%d forged proofs all rejected: %s" % (len(rejected), ", ".join(rejected)) + + +def leg_cross_process(mod): + """The checker must work from a cold database: proof made in a child, checked here.""" + n, cl = php(3, 4) # 4 pigeons, 3 holes -> UNSAT + tmp = tempfile.mkdtemp(prefix="satkit-cross-") + inst = os.path.join(tmp, "instance.json") + out = os.path.join(tmp, "proof.json") + with open(inst, "w") as fh: + json.dump({"nvars": n, "clauses": [list(c) for c in cl]}, fh) + child = [sys.executable, os.path.abspath(__file__), "--emit-proof", inst, out] + proc = subprocess.run(child, capture_output=True, text=True, timeout=120) + if proc.returncode != 0: + return False, "child failed: %s" % (proc.stderr.strip()[:300],) + with open(out) as fh: + payload = json.load(fh) + if payload.get("sat"): + return False, "child reported SAT for PHP(4,3)" + ok, i, msg = oracle_check_proof(n, cl, payload["proof"]) + if not ok: + return False, "child proof rejected by harness oracle: %s" % msg + pr = mod.check_proof(n, cl, payload["proof"]) + if not pr.ok: + return False, "checker rejected a proof from another process: %s" % pr.message + return True, "child emitted a %d-step proof; parent oracle + checker both accept" % ( + len(payload["proof"]),) + + +def leg_determinism(mod): + rng = random.Random(31337) + for n, cl in ((30, rand_3sat(rng, 30)), php(3, 4)): + a = mod.solve(n, list(cl)) + b = mod.solve(n, list(cl)) + if (a.sat, a.model, a.proof) != (b.sat, b.model, b.proof): + return False, "two runs on n=%d disagreed" % n + return True, "identical sat/model/proof across repeat runs" + + +LEGS = [ + ("edge_cases", leg_edge_cases), + ("exhaustive_n2", leg_exhaustive_n2), + ("exhaustive_n3", leg_exhaustive_n3), + ("random_sweep", leg_random_sweep), + ("php_proofs", leg_php_proofs), + ("random3sat_proofs", leg_random3sat_proofs), + ("oracle_selfcheck", leg_oracle_selfcheck), + ("negative_controls", leg_negative_controls), + ("cross_process", leg_cross_process), + ("determinism", leg_determinism), +] + + +# ========================================================================== +# mutation control: the suite must have teeth +# ========================================================================== +class Sabotaged: + """Delegates to satkit except for the named overrides.""" + + def __init__(self, name, overrides): + self.name = name + self._overrides = overrides + + def __getattr__(self, attr): + if attr in self._overrides: + return self._overrides[attr] + return getattr(satkit, attr) + + +def _flipped_sat(nvars, clauses, collect_proof=True): + r = satkit.solve(nvars, clauses, collect_proof) + return satkit.SolveResult(not r.sat, r.model, r.proof, r.stats) + + +def _all_positive_model(nvars, clauses, collect_proof=True): + r = satkit.solve(nvars, clauses, collect_proof) + if r.sat: + return satkit.SolveResult(True, [v for v in range(1, nvars + 1)], None, r.stats) + return r + + +def _short_proof(nvars, clauses, collect_proof=True): + r = satkit.solve(nvars, clauses, collect_proof) + if not r.sat and r.proof: + return satkit.SolveResult(False, None, list(r.proof)[:-1], r.stats) + return r + + +def _lax_checker(nvars, clauses, proof, require_empty=True): + return satkit.ProofResult(True, len(proof or []), "mutant: accepts everything") + + +MUTANTS = [ + ("flipped_sat", {"solve": _flipped_sat}, "exhaustive_n2"), + ("all_positive_model", {"solve": _all_positive_model}, "random_sweep"), + ("short_proof", {"solve": _short_proof}, "php_proofs"), + ("lax_checker", {"check_proof": _lax_checker}, "negative_controls"), +] + + +def leg_mutant_control(_mod): + by_name = dict(LEGS) + results = [] + for name, overrides, target in MUTANTS: + ok, detail = by_name[target](Sabotaged(name, overrides)) + if ok: + return False, "mutant %r SURVIVED leg %r -- that leg is vacuous" % (name, target) + results.append("%s caught by %s" % (name, target)) + return True, "%d/%d mutants killed (%s)" % (len(MUTANTS), len(MUTANTS), "; ".join(results)) + + +# ========================================================================== +# entry point +# ========================================================================== +def emit_proof(instance_path, out_path): + with open(instance_path) as fh: + inst = json.load(fh) + r = satkit.solve(inst["nvars"], [tuple(c) for c in inst["clauses"]]) + with open(out_path, "w") as fh: + json.dump({"sat": r.sat, "model": r.model, + "proof": [list(s) for s in (r.proof or [])]}, fh) + return 0 + + +def main(argv): + if "--emit-proof" in argv: + return emit_proof(argv[argv.index("--emit-proof") + 1], + argv[argv.index("--emit-proof") + 2]) + + print("verify_satkit: %s" % os.path.abspath(satkit.__file__)) + print("python %s\n" % sys.version.split()[0]) + failures = 0 + t_start = time.time() + for name, leg in LEGS: + t0 = time.time() + try: + ok, detail = leg(satkit) + except Exception as exc: # noqa: BLE001 + ok, detail = False, "raised %s: %s" % (type(exc).__name__, exc) + dt = time.time() - t0 + print("%-20s %-4s %6.2fs %s" % (name, "PASS" if ok else "FAIL", dt, detail)) + if not ok: + failures += 1 + + t0 = time.time() + ok, detail = leg_mutant_control(satkit) + print("%-20s %-4s %6.2fs %s" % ("mutant_control", "PASS" if ok else "FAIL", time.time() - t0, detail)) + if not ok: + failures += 1 + + total = len(LEGS) + 1 + print("\n%d/%d legs passed in %.2fs" % (total - failures, total, time.time() - t_start)) + return 0 if failures == 0 else 1 + + +if __name__ == "__main__": + sys.exit(main(sys.argv[1:]))