SAT/CP-SAT-based finite counterexample search and verification

Statement

Boolean satisfiability (SAT): given a propositional formula in conjunctive normal form (CNF) — a conjunction of clauses, each a disjunction of literals over Boolean variables — decide whether some assignment of the variables makes the formula true (SAT), and if so, exhibit one; otherwise report UNSAT. SAT was the first problem proved NP-complete (Cook–Levin theorem, Cook 1971 / Levin 1973, en.wikipedia.org/wiki/Cook%E2%80%93Levin_theorem): every problem in NP polynomial-time-reduces to it. In practice, modern CDCL (conflict-driven clause learning) solvers — MiniSat, Glucose, CaDiCaL, Kissat, etc. — decide SAT instances with millions of variables by search-with-clause-learning (non-chronological backjumping plus recording the "reason" for each conflict as a new learned clause), refining the 1961 DPLL backtracking algorithm (en.wikipedia.org/wiki/Conflict-driven_clause_learning, en.wikipedia.org/wiki/DPLL_algorithm).

CP-SAT (Google OR-Tools): a constraint-programming solver built on top of a SAT engine via Lazy Clause Generation (LCG) — native constraints (AllDifferent, linear-Boolean, table, interval/scheduling constraints) are propagated directly by dedicated algorithms, and every propagation step is lazily "explained" as a clause pushed into the underlying SAT clause database only when needed, so the CDCL learning/backjumping machinery still applies globally across the whole model (developers.google.com/optimization/cp; d-krupke.github.io/cpsat-primer). This lets a modeler state combinatorial constraints (e.g. "no triangle," "exactly $k$ vertices selected," "all-different colors") natively instead of hand-compiling everything to CNF, while keeping CDCL's search power.

The core epistemic move this concept-page is about, applied to a mathematical conjecture with a free parameter $n$ (graph order, sequence length, dimension, number of colors, point-set size): fix $n$ to a specific finite value, encode "a counterexample of this exact size/shape exists" as a SAT/CP-SAT instance, and run the solver.

- SAT (satisfiable) outcome $\Rightarrow$ the solver returns a satisfying assignment, which decodes back into an *explicit finite combinatorial object*. This object is a genuine counterexample/witness and is trivially verifiable: checking that it satisfies the original (un-encoded) mathematical property is a direct, small, from-scratch computation, independent of trusting the solver. - UNSAT (unsatisfiable) outcome $\Rightarrow$ the solver (optionally) emits a proof certificate (DRAT/LRAT format) that can be checked by an independent, much simpler verifier. A validated UNSAT certificate is a machine-checked, rigorous proof that no object of that exact finite size/shape exists — i.e. it *proves* a specific finite instance of the conjecture (an exact value in a sequence, a "ruled out up to $n$" bound, or a fully resolved small case), not merely "the solver didn't find one."

This is the sense in which SAT/CP-SAT search is a genuine proof technique, not just a heuristic search tool: both outcomes, when the certificate/witness is independently checked, produce results as rigorous as a hand proof for that fixed finite instance.

Facts

- Boolean Pythagorean triples problem (Heule, Kullmann, Marek, arXiv:1605.00723, 2016): is there a 2-coloring of $\{1,\dots,N\}$ with no monochromatic Pythagorean triple? Proved UNSAT for $N=7825$ (and SAT — an explicit valid coloring exists — for $N=7824$), settling a Ramsey-theory-style discrepancy question open since the 1980s. The UNSAT proof: ~1 trillion cases after symmetry-breaking/preprocessing, solved via cube-and-conquer on the TACC Stampede supercomputer in about 2 wall-clock days (~4 CPU-years total), producing a 200 terabyte proof certificate, compressed to 68 GB, independently checked (en.wikipedia.org/wiki/Boolean_Pythagorean_triples_problem; cs.utexas.edu/~marijn/ptn/). - Schur Number Five (Heule, arXiv:1711.08076, AAAI 2018): what is the largest $n$ with a 5-coloring of $\{1,\dots,n\}$ avoiding a monochromatic solution to $a+b=c$? Answer $n=160$ (i.e. $S(5)=160$), found via massively parallel cube-and-conquer with a custom cheap hardness predictor splitting the search into millions of subproblems; proof size 2 petabytes, checked with a formally verified proof checker. - Keller's conjecture, dimension 7 (Brakensiek, Heule, Mackey, Narváez, arXiv:1910.03740, IJCAR 2020 best paper): reduced to "does any of three specific graphs contain a clique of size $2^7=128$?" via a known graph-theoretic equivalence, encoded as SAT with symmetry-breaking, solved UNSAT with CaDiCaL (~200 GB proof, independently checked) in about 30 minutes on a compute cluster after four months of encoding/engineering work — resolving a 90-year-old geometry conjecture (do all unit-cube tilings of $\mathbb R^7$ contain two cubes sharing a full facet?) for the last open dimension. - Empty hexagon number (Heule & Scheucher, arXiv:2403.00737, 2024; formally verified by Subercaseaux, Nawrocki, Gallicchio, Codel, Carneiro, Heule, arXiv:2403.17370, ITP 2024): does every set of 30 points in the plane in general position contain an empty convex hexagon? Encoded via an $O(n^4)$-clause CNF connecting order-type axioms to hexagon-existence; UNSAT-for-"no hexagon"-at-$n=30$ found after 17,300 CPU-hours of parallel search, establishing $h(6)=30$; the entire SAT-encoding-to-geometry bridge was then re-verified from scratch inside the Lean theorem prover — an unusually strong verification bar (solver output re-derived formally, not merely proof-checked). Directly related to Erdős #107 — exact Erdős–Szekeres convex-polygon constant (Erdős–Szekeres): Balko & Valtr, "A SAT attack on the Erdős-Szekeres conjecture" (Eur. J. Combin. 66 (2017) 13–23), used the same style of attack to *disprove* a stronger structural conjecture of Peters–Szekeres about 7-point configurations, but the base conjecture $\mathrm{ES}(7)=33$ itself remains open and is a live 2025–2026 SAT-search target (Bogdan, arXiv:2512.24061, Dec 2025) — a clean illustration that a SAT attack can settle a *related* finite question while the target instance stays open. - Erdős discrepancy problem, $C=2$ case (Konev & Lisitsa, arXiv:1402.2184, 2014) is the canonical boundary-case illustration of what SAT search can and cannot do: they proved via a 13 GB DRUP certificate that every $\pm1$ sequence of length $\geq1161$ has discrepancy $>2$ against some homogeneous AP, resolving the conjecture for the single fixed constant $C=2$. This technique is intrinsically incapable of reaching the full conjecture (discrepancy unbounded, i.e. "for every $C$") because that is a statement over infinitely many finite instances with no uniform finite encoding — the general case was instead settled by Terence Tao's 2015 analytic proof (arXiv:1509.05363, entropy/Elliott-conjecture-flavored argument), a genuinely different, non-computational technique. This is the standard cautionary example cited whenever this concept page's applicability is scoped. - Van der Waerden numbers: $W(2,6)=1132$ (Kouril & Paul, exhaustive SAT-style parallel backtracking across Beowulf clusters with FPGA acceleration in the final phase) and $W(3,4)=293$ (Ahmed) are exact values pinned down purely by finite SAT/backtracking search over the (very large but finite) space of colorings avoiding a monochromatic AP of the target length — joems.springeropen.com/articles/10.1186/s42787-019-0021-1; arxiv.org/pdf/1004.0653 ("Exact Ramsey Theory: Green-Tao numbers and SAT"). - SAT+CAS (computer algebra system) hybrid verification is an emerging refinement for exact small Ramsey numbers: Li, Duggan, Bright, Ganesh, arXiv:2502.06055, produce independently checkable certificates (DRAT plus CAS-verified symmetry/isomorphism-rejection steps) for $R(3,8)$ and $R(3,9)$ bounds — combining a SAT solver's search power with a CAS's exact symbolic verification of the graph-isomorphism/symmetry-breaking side-conditions the SAT encoding relies on. - Proof-certificate formats and independent verification are the load-bearing trust mechanism. DRAT (Wetzler, Heule, Hunt; format spec arXiv:1610.06229) generalizes the earlier RUP/DRUP formats and Extended Resolution: a clausal proof is a sequence of clause-addition/clause-deletion steps, each checkable to preserve satisfiability in polynomial time via the "resolution asymmetric tautology" (RAT) property; drat-trim (github.com/marijnheule/drat-trim) is the reference checker, and formally verified checkers (used e.g. for Schur Number Five and, via a full from-scratch Lean re-derivation, for the empty hexagon number) close the "trust the SAT solver's own correctness" gap entirely — a landmark SAT-search result is not accepted on the word of the (often buggy, highly-optimized) solver binary, but on an independently, cheaply re-checkable certificate.

Technique

HOW to apply this to a new Erdős-style finite/small-case sub-question (recombination steps):

1. Isolate a genuinely finite sub-question. The conjecture itself may be asymptotic/"for all $n$" (not directly SAT-attackable, per the discrepancy-problem boundary case above), but almost every such conjecture has finite sub-targets: an exact small value in a sequence (Ramsey numbers, Schur numbers, van der Waerden numbers, $f(7)$ in Erdős–Szekeres), a "known counterexample-free up to $N$" table to extend by one more value, or a specific small dimension/order case (Keller's conjecture dimension 7). 2. Encode the combinatorial object as Boolean variables (edge indicators $x_{ij}$, coloring indicators, order-type/orientation predicates for point configurations, membership indicators for a subset) and every forbidden substructure as a clause or native CP-SAT constraint (triangle-freeness: $x_{ij}+x_{jk}+x_{ik}\le2$ for every triple; monochromatic-AP-freeness: a clause per arithmetic progression per color; clique-of-size-$k$ existence: standard SAT clique encodings). CP-SAT's native constraints (AllDifferent, linear, table) are preferable when available since LCG compiles them to clauses lazily and more efficiently than hand-written CNF. 3. Break symmetry aggressively — canonical/lexicographic-leader ordering constraints, or a dedicated preprocessor exploiting the automorphism group of the target object. This step is not optional: essentially every landmark result above (Pythagorean triples, Keller's conjecture, van der Waerden numbers) explicitly credits symmetry-breaking as the difference between an intractable and a tractable search, since without it the solver re-explores automorphic copies of the same partial assignment. 4. For hard instances, use cube-and-conquer (Heule, Kullmann, Wieringa, HVC 2011; Heule, Kullmann, Marek, IJCAI 2017): phase 1 uses a lookahead solver to split the instance into many (thousands to millions of) disjoint sub-cases ("cubes," partial assignments chosen to be individually easier), phase 2 hands each cube-conjoined-with-formula to an independent CDCL solver run, embarrassingly parallel across a cluster. This combines lookahead solvers' strength at *choosing good splitting structure* on hard/structured instances with CDCL solvers' strength at *exploiting learned clauses* within a bounded sub-case — the mechanism behind every petabyte-scale proof above. 5. Branch on the outcome. SAT: decode the witness, then run a small independent, from-scratch verifier checking it against the *original* mathematical statement (not the encoding) — this yields a citable, self-contained finite counterexample or extremal construction. UNSAT: emit a DRAT/LRAT certificate and check it with an independent checker (drat-trim, a formally verified checker, or — for maximal trust — a full formal re-derivation as done for the empty hexagon number) — this yields a citable, machine-checked non-existence proof at that exact finite scale. 6. State the scope precisely. A SAT-search result of this kind proves exactly "true/false at parameter value $n$" (or up to $n$), never the general asymptotic statement — extending it to "for all $n$" or "for all sufficiently large $n$" requires a separate, usually analytic/combinatorial, argument (cf. the Erdős discrepancy problem's $C=2$-via-SAT vs. general-$C$-via-Tao's-analysis split). When reporting a SAT-search contribution to an open Erdős problem, always frame it as extending a finite table / resolving a named finite sub-case, not as resolving the parent conjecture, unless the parent conjecture is itself finite (e.g. a specific exact Ramsey/Schur/van-der-Waerden number).

WHEN it applies: the target property must be checkable on a single object of *bounded, explicitly fixed size* (a graph on $n$ vertices, a coloring of $\{1,\dots,N\}$, a point configuration of $m$ points, a tiling in a fixed finite dimension) — i.e. the search space, while possibly astronomically large, must be genuinely finite and the property machine-checkable in the encoding. It does not directly apply to statements quantified over infinitely many scales (unbounded discrepancy constant, "for all sufficiently large $n$," continuum-cardinality set theory as in Erdős #601 — ordinal graphs: infinite path or full independent set) — those need a uniform/asymptotic argument instead, though SAT search can still supply supporting finite data points or fully resolve *bounded* special cases embedded in the asymptotic statement.

WHY it works (the mechanism, for recombination): SAT is NP-complete (Cook–Levin), so *any* finite combinatorial existence/non-existence question expressible with a polynomially-sized description reduces to it in principle; the practical payoff is that seven decades of CDCL/lookahead engineering plus cube-and-conquer parallelism now routinely search spaces of $10^{12}$–$10^{18}$ configurations that are utterly infeasible by direct enumeration, while the DRAT/LRAT certificate mechanism converts "the solver says UNSAT" (an untrustworthy claim about a hand-optimized, bug-prone binary) into "an independently, cheaply, and even formally re-checkable proof object" — decoupling the *finding* of a proof (expensive, solver-specific, unverified) from the *checking* of a proof (cheap, solver-agnostic, rigorous). This is exactly the same finding/checking asymmetry that underlies NP itself, applied at industrial scale to real open mathematics.

Related

- Erdős #107 — exact Erdős–Szekeres convex-polygon constant — Erdős–Szekeres convex-polygon problem; $f(6)=17$ known by exhaustive computer search (Peters–Szekeres 2006), $f(7)=33$ conjectured but open and under live SAT-search attack (Balko–Valtr 2017 disproved a related structural conjecture; Bogdan 2025 ongoing); sister problem Erdős #216 — the empty hexagon number g(6) (and non-existence for k≥7) (empty hexagon) fully resolved by exactly this SAT-search-plus-formal-verification pipeline (Heule & Scheucher 2024 + Lean re-derivation), the clearest worked precedent in this wiki for where this technique cracks a problem outright. - Erdős #128 — local edge density forces a triangle — sparse-halves triangle-free-graph conjecture; this page's Technique steps 1–4 (CP-SAT edge/subset encoding, McCormick-linearized sparsest-$k$-subgraph inner problem, symmetry via vertex-transitive candidates) are the proposed concrete attack surface there. - Erdős #552 — Ramsey number R(C4,Sn), dip below n+√n? — $C_4$-vs-star Ramsey number $f(n)$; Boza (arXiv:2409.12770) used SAT/ILP plus the House-of-Graphs database and degree-pruning to compute exact values for $n\in\{34,\dots,39,43\}$, extendable with the same toolkit. - Erdős #64 — min-degree-3 graphs contain a power-of-2 cycle — cubic/min-degree-3 graph cycle-spectrum problem; CP-SAT candidate generation and verification is flagged there alongside nauty/geng/plantri: canonical-construction-path exhaustive generation of graphs (min-degree / cubic / planar families) (geng/plantri exhaustive generation) as complementary finite-search machinery. - Erdős #1 — distinct subset sums need N ≫ 2^n and Erdős #52 — the sum-product problem for integers — both flag a bounded sub-conjecture (Conway–Guy for specific small $k$; OEIS A263996 small-$n$ extremal sets) as a concrete, currently-finite SAT/ILP target inside an otherwise-asymptotic open problem — direct illustrations of Technique step 1 ("isolate a genuinely finite sub-question"). - Lean 4 formalization of constructions and conditional reductions (Erdős-problem context) — the formal-verification endpoint this technique increasingly feeds into (DRAT/LRAT certificates checked by, or fully re-derived inside, Lean/Isabelle/ACL2 — e.g. the empty hexagon number and Schur Number Five). - Flag algebras — Razborov's SDP-based calculus for extremal graph/hypergraph densities — the semidefinite-programming sibling technique for *proving upper bounds* on extremal densities (as opposed to SAT's exact finite existence/non-existence); the two are complementary attack surfaces on the same class of extremal-graph problems (see Erdős #128 — local edge density forces a triangle's Related section). - Concept referenced but not yet split into its own page: "CP-SAT" / OR-Tools Lazy Clause Generation specifically (as opposed to raw CNF-SAT) — currently folded into this page per Erdős #128 — local edge density forces a triangle's anticipatory `concept/cp-sat` link; flagged here as a possible future page-split if OR-Tools-specific modeling technique (native global constraints, LNS, hybrid LP relaxations) grows enough independent material.