sair-distillation/eq2-leaner/ce_backtrack - Storage Bucket

ce_backtrack — a lean constraint-propagation counterexample finder

Pure-Python (no deps, no Lean, no LLM) finite-magma counterexample search for Stage-2 FALSE problems: given E1 ⇒ E2?, find a magma (Fin n, ◇) where E1 holds for all assignments and E2 fails for some assignment. Every table returned is re-verified through the official Lean judge (finOpTable + decideFin!) before it is ever claimed.

Modules

• core.py — equation parser + codegen evaluator. Each equation compiles to a native Python function (exec) that loops over assignments with no dict lookups; holds() / violated() run fast. This is the hot path everything else sits on.
• search.py — the "cheap ladder": exhaustive Fin 2-3, ~40 structured table families Fin 2-7, direct-product tables, random sampling. Mirrors the opnorm reference solver's deterministic families so the benchmark is apples-to-apples.
• backtrack.py — the contribution: a DPLL-style constraint-propagation model finder.
  • Expands "E1 holds" into ground constraints, one per assignment.
  • Unit propagation: a constraint that resolves to (known value v) == (one unassigned cell c) forces T[c] = v.
  • Branches on a blocking cell an unresolved constraint is waiting on.
  • Optional least-number heuristic (lnh=True): caps a branch cell's values at max-used+1, a symmetry reduction over element relabelling. Heuristic — can miss a model (false negative) but never produces a wrong table.
  • Free cells (unconstrained by E1) are completed to violate E2 if possible.
  • find_targeted / search_targeted (the residual cracker): drive the search from the E2-violation side. By value symmetry, if any counterexample exists there is an isomorphic one where E2.lhs(a2)=0 ∧ E2.rhs(a2)=1 for some assignment a2 (relabel the two distinct values to 0,1). Pin those two equalities (they propagate hard, unlike a raw disequality) and iterate a2. This cracks Fin-6 counterexamples the plain finder's all-zero completion misses.
• certgen.py — emit the false Lean certificate and call judge.verify.
• bench.py, eval_misses.py, build_certs.py — measurement + packaging.

Results on the 1,669 public problems (850 FALSE)

Measured in pure Python (E1-holds/E2-fails is decidable without Lean):

stage	FALSE solved	notes
cheap ladder (exhaustive Fin2-3 + structured + product + random)	761 / 850	~11 ms/problem
+ backtrack (Fin 4-6, propagation)	822 / 850	+61 (all Fin 4-5)
+ find_targeted (Fin 6, pin E2 sides by value symmetry)	828 / 850	+6 residual (Fin 6)
+ satfind (SAT selector-per-a2, Fin 7-8, pysat)	833 / 850	+5 residual, no CE at Fin ≤6-7
+ find_sat_sym (symbolic-E2 SAT, Fin 7-9)	848 / 850	+15; only hard2_0027, hard2_0051 remain

satfind.py (the SAT finder) is an offline mining tool — it needs pysat and is not part of any submittable solver; the coverage pool accepts certs produced by any means, and every table is judge-verified before posting. It one-hot-encodes the Cayley table + interned ground-term value vars (lookup flattening) and asserts E1-holds ∧ E2-fails. Two E2 encodings:

• find_sat — a selector per E2 assignment. Simple, but for a 3-variable E2 the n³·n^k2 clauses blow up at n≥8 (generation, not solving, is the wall).
• find_sat_sym — encodes the violating assignment itself as one-hot SAT vars (symbolic E2), so E2 cost is O(#E2-op-nodes · n³), independent of n^k2. This cracked the 15 stubborn 3-variable-E2 residuals at Fin 7-9.

Solving is wall-clock bounded (_solve_bounded: pysat timer + interrupt) so a hard UNSAT can't hang. Certs need set_option maxRecDepth 100000 for Fin ≥6 (baked into certgen); a Fin-8 decideFin! cert verifies in ~6-8 s (< 120 s cap).

Honesty note. The opnorm reference solver's full deterministic pipeline already includes a Fin 4-5 backtracking stage (10 s budget). Comparing my 61 backtracking wins against opnorm-deterministic: opnorm also finds 60 of them; exactly 1 (hard1_0037) is novel vs opnorm-deterministic. See opnorm_comparison.txt. So this finder's value is (a) it packages 61 verified, posted certificates for hard problems into the coverage pool, (b) it is a lean, dependency-free, propagation-based finder (no 5000-sample random flailing), and (c) it's the base I'm extending with LNH + Fin 6-7 to attack the 28 residual that no deterministic search here cracks yet.

Residual (open frontier): 2 FALSE problems

Down from 28 → the symbolic-E2 SAT finder cleared all but hard2_0027 and hard2_0051. Both return UNSAT at Fin ≤9 within budget → they need Fin ≥10 (or a longer solve). Next: run find_sat_sym at n=10-12 with a larger time/clause budget, or a dedicated symmetry-broken model finder. Both are answer: false, so a counterexample exists at some finite order.

Everything else across all 850 public FALSE problems now has a verified, posted counterexample certificate (848 / 850).

Usage

python -m cebench.bench --sets normal,hard1,hard2,hard3 --out baseline.json
python -m cebench.eval_misses --baseline baseline.json --sizes 4,5,6 --out found.json
python -m cebench.build_certs --found found.json --out certs.json
python eq2_harness.py package --repo <repo> --agent-id <you> --certs certs.json