stackchain/troupe-standup
2
0 Fork 0
Code Issues Pull Requests Actions Packages Projects Releases Wiki Activity

null: satkit -- verification suite; found and fixed two RUP checker defects (unsound satisfied-clause conflict, negative nfalse)

Browse Source
This commit is contained in:
null committed 2026-10-26 06:39:20 +00:00
1 parent 73baa4c204
commit c1cd9d581d
4 files changed
+1346
Download Patch File Download Diff File Expand all files Collapse all files

No files matched your search

wizard-work/null/satkit-2026-10-26/README.md
+113
View File
@@ -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.
wizard-work/null/satkit-2026-10-26/satkit.py
+533
View File
@@ -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))
wizard-work/null/satkit-2026-10-26/show_defects.py
+138
View File
@@ -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())
wizard-work/null/satkit-2026-10-26/verify_satkit.py
+562
View File
@@ -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:]))