# SAT and CSP encodings > Write the puzzle as clauses and hand it to an industrial solver: the obvious move, tried since 2008. Why complete solvers stall on the full board, and where their verdicts still earn their keep as impossibility proofs. - Canonical page (with interactive figures/demos): https://eternity2.dev/research/build/exact/sat-csp-encodings/ - Updated: 2026-07-02 - Topics: exact-methods - Source: Heule, Solving edge-matching problems with satisfiability solvers (2008) — https://www.cs.cmu.edu/~mheule/publications/eternity.pdf - Source: Ansótegui, Béjar, Fernàndez & Mateu, Edge Matching Puzzles as Hard SAT/CSP Benchmarks (CP 2008) — https://link.springer.com/chapter/10.1007/978-3-540-85958-1_39 - Source: Ansótegui, Béjar, Fernàndez & Mateu, On the hardness of solving edge matching puzzles as SAT or CSP problems (Constraints, Springer) — https://link.springer.com/article/10.1007/s10601-012-9128-9 - Source: Ansótegui, Béjar, Fernàndez & Mateu, How Hard is a Commercial Puzzle: the Eternity II Challenge (CCIA 2008) — https://repositori.udl.cat/bitstreams/0b6533fe-54e5-4070-85fe-80f7d35837d8/download --- Modern SAT solvers settle industrial problems with millions of variables, so the obvious move is to write Eternity II as clauses and let CDCL do the digging. People have been making exactly this move since 2008. The encodings are clean and the small sizes fall instantly; the full puzzle does not budge. Understanding why is a lesson in what conflict-driven search actually feeds on. ## The encoding The direct encoding introduces a variable $x_{c,p,r}$ for "piece $p$ sits at cell $c$ with rotation $r$", then three families of constraints: every cell holds exactly one placement, every piece is used at most once, and any two placements that disagree across a shared edge are mutually excluded. The same model reads naturally as a CSP: one variable per cell, placements as domain values, an *alldifferent* over pieces, and table constraints on adjacent cells. That formulation is the one the benchmark papers study alongside the clausal one. The direct clausal form blows up fast, because the pairwise edge-disagreement clauses multiply. Marijn Heule's [2008 paper](https://www.cs.cmu.edu/~mheule/publications/eternity.pdf) showed the standard remedy: introduce auxiliary variables for the colour shown on each internal seam, so a placement implies its four seam colours and disagreement is excluded once per seam rather than once per pair. With compact encodings, symmetry breaking, and solver tuning, Heule solved edge-matching instances well beyond what the naive encoding reached. Even so, community-built CNFs of the full 16×16 puzzle run to roughly a hundred thousand variables and hundreds of millions of clauses (as reported on the [community mailing list](https://groups.io/g/eternity2)). They load fine, and they remain utterly unsolved. ## Take the measure of it Numbers with fourteen digits stop meaning anything in prose, so measure them instead. The explorer below computes both encodings live from the derivation above. Slide the board size across the community's pure-SAT ceiling at 10×10 and up to the full 16×16, and watch the log-scale bars. Underneath it, a six-clause instance shows the other half of the story: the unit-propagation cascade that CDCL's clause learning feeds on, and that this puzzle starves. > **[Figure]** Interactive: SAT/CSP encoding size blowup — interactive: EncodingSizeLab. Rendered on the canonical page (link above); not shown in this markdown export. ## Step by step Derive the sizes once by hand; they stop being folklore. 1. **Placement variables.** $p = n^2$ pieces, $4$ rotations, $n^2$ cells: $x_{c,p,r}$ gives $n^2 \cdot p \cdot 4 = 4n^4$ variables. At $n = 16$ that is $262{,}144$ raw placements; pruning the impossible ones (border pieces only sit on the rim, corners only in corners) brings this down to the "roughly a hundred thousand variables" the community CNFs actually carry. 2. **Cell and piece constraints.** Every cell holds exactly one placement: one long clause plus, pairwise, $\binom{4n^2}{2}$ exclusions per cell. Every piece is used at most once: another $\binom{4n^2}{2}$ per piece. Pairwise at-most-one is quadratic; this is what compact encodings (sequential, commander) reduce to $O(4n^2)$ clauses each, at the price of auxiliary variables. 3. **The direct conflict clauses: the blow-up.** The board has $2n(n-1)$ internal seams. For each seam, every pair of placements that disagrees across it gets a binary clause: about $(4n^2)^2 (1 - 1/c)$ pairs per seam if colours were uniform. At $n = 16$, $c = 17$: $480 \times 1024^2 \times \tfrac{16}{17} \approx 4.7 \times 10^8$ clauses, the "hundreds of millions" reported for full-board CNFs, recovered from first principles. 4. **Heule's seam trick.** Name the colour of each seam: $2n(n-1) \cdot c$ auxiliary variables ($8{,}160$ at full size). Now each placement *implies* its four seam colours (at most $16n^4$ binary clauses) and disagreement is forbidden once per seam, not once per pair: $\binom{c}{2}$ clauses per seam, about $65{,}000$ total. The conflict machinery collapses by three orders of magnitude. That is exactly why Heule's instances reached sizes the naive encoding never touched, and why the ceiling still sits near 10×10 rather than 16×16: size was never the only problem. ## What it costs - **The solver, in the worst case: exponential.** SAT is NP-complete, and CDCL is a resolution-based procedure: on families with exponential resolution lower bounds, *no* run of it can be subexponential. Its industrial success is a statement about typical structure, not worst-case cost, and an instance built at the hardness peak is as far from typical as it gets. - **Unit propagation: cheap by design.** With two watched literals per clause, a clause is only examined when one of its two watches is falsified, and each visit costs $O(\text{clause length})$ to find a new watch. Propagation is why CDCL can afford millions of decisions per second even on enormous CNFs; loading Eternity II was never the issue. - **Conflict analysis: pay proportional to the implication graph.** Each conflict is analysed by walking the implication graph back to a cut (first-UIP), costing time linear in the graph traversed, and yields one learned clause whose pruning power depends on being *short*. That is the step this puzzle starves: flat implication chains make the walk trivial and the learned clause wide. Full price, no product. - **The CSP side has the same shape.** Enforcing [arc consistency](/research/build/reduce/arc-consistency) on the table constraints is polynomial per node, and Régin's GAC *alldifferent* filter runs a bipartite matching in $O(m\sqrt{n})$ per call (see the [alldifferent page](/research/build/reduce/alldiff-regin)). Polynomial propagation atop an exponential search tree: strong locally, helpless globally. - **Where the account balances.** On the full board, worst-case behaviour is the observed behaviour. On pinned subproblems, the same machinery returns UNSAT in under two seconds, an impossibility theorem per query at the price of a database lookup. The costs did not change; the question did. ## What the published benchmarks showed The systematic study is due to Ansótegui, Béjar, Fernàndez and Mateu, in a [CP 2008 paper](https://link.springer.com/chapter/10.1007/978-3-540-85958-1_39) and an extended [journal version in Constraints](https://link.springer.com/article/10.1007/s10601-012-9128-9), with a companion paper asking, verbatim, [how hard the commercial puzzle actually is](https://repositori.udl.cat/bitstreams/0b6533fe-54e5-4070-85fe-80f7d35837d8/download). Their headline: generalized edge-matching puzzles make excellent SAT/CSP benchmarks precisely because difficulty is tunable: vary the number of colours and solve time rises to a sharp peak where solutions are scarce but real. Eternity II's colour counts sit at that peak, by design; the [phase transition page](/research/why/phase-transition) walks through it. In practice, complete solvers dispatch small boards in seconds and then hit an exponential cliff; community experiments over the years put the practical ceiling for pure SAT on Eternity-style instances somewhere around the 10×10 scale, far short of 16×16. See the [papers page](/research/papers) for the full literature trail. ## Why CDCL stalls on the full board CDCL earns its power from clause learning: when propagation hits a conflict, the solver walks the implication graph back to a small set of decisions that caused it, and records that combination as forbidden. The learned clause is short and general when conflicts arise from long chains of unit propagation. Eternity II starves that mechanism. This project's analysis of its own CSP engine (hedged accordingly: measured here, not independently replicated) found the implication structure is nearly flat (a domain deletion traces back to a single neighbouring placement, not to a deep chain), so conflict analysis has almost nothing to compress, and the learned [no-goods](/research/build/reduce/nogood-learning) come out wide and specific instead of short and general. Worse, conflicts surface late: with strong propagation running, domain wipeouts essentially never occurred before depth 50, with the median deep in the board. A wide clause about a deep, specific configuration prunes almost nothing else. Add an instance deliberately tuned to the hardness peak, and the full puzzle is close to a worst case for conflict-driven search. ## Where the exact verdicts still pay None of this makes the encodings useless; it relocates them. A complete solver's UNSAT answer is a theorem, and on subproblems those theorems come cheap. This project's most productive use of SAT (same hedge as above) is as an *oracle on regions*: pin most of a strong board, free a neighbourhood of its remaining mismatches, and ask for a fully matched completion. The answer comes back UNSAT, typically in under two seconds, and proves that no local rearrangement of that region can ever finish the board, which is the machinery behind the [rigidity wall](/research/why/rigidity-wall). The same trick screens whole border rings: pin a candidate border, free all 191 interior cells, and a sub-second UNSAT certifies that border can never carry a perfect interior. And within a CSP search engine, the same idea in miniature (recording hard no-goods at propagation failures so a structural dead end is never re-entered) is sound by construction and cheap to check with SAT-style watched literals. That is the division of labour: as a frontal solver of the full puzzle, CDCL is outmatched; as a fast generator of impossibility certificates for pieces of it, nothing else comes close. ## Related - [MOSAIC](https://eternity2.dev/research/lab/experiments/raphael-anjou/pipelines/mosaic) — Tile the board into small blocks, solve each one to proven optimality, and glue them together, paying for the seams instead of forbidding them. From scratch, with no record to copy, it reaches 448. - [Papers](https://eternity2.dev/research/papers) — The academic literature on Eternity II and edge-matching puzzles, drawn from the project's research notes and the community reading list, and ranked by how useful each paper actually is if your goal is to write a solver. - [Tuned to the hardness peak](https://eternity2.dev/research/why/phase-transition) — Eternity II uses 22 colors. They split 17 interior to 5 frame-only, and that 17 is exactly where this kind of puzzle is hardest to solve. - [The rigidity wall](https://eternity2.dev/research/why/rigidity-wall) — Every record board we have is frozen in place. You cannot nudge your way from a great board to a perfect one, and we can prove it.