T
Jun 7, 2026The Expensive Half of a SAT Proof
A from-first-principles tour of double-lex symmetry breaking for SAT: why the UNSAT side is expensive, how canonical-representative constraints fix it, a worked Zarankiewicz example that settled three new OEIS values, and an honest map of where the technique stops scaling.
Jun 7, 20268 min read0 reactions0 comments
