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.
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 direct encoding introduces a variable xc,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
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). They load
fine, and they remain utterly unsolved.
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.
Both encodings are computed live from the page's own derivation: p = n² pieces, 4 rotations, n² cells give 4n⁴ placement variables. The direct encoding forbids every disagreeing pair of placements across every seam; Heule's seam encoding names the colour on each seam and forbids disagreement once per seam. The bars are log-scale — each tick is ×10.
410 — pure-SAT ceiling16 — Eternity II
Beyond every demonstrated pure-SAT success on Eternity-style instances — loadable, and unsolved.
At n = 16, c = 17 the direct form reaches 262 k variables and ≈ 474 M conflict clauses — the same “hundreds of millions” the community reported for full-board CNFs.
What CDCL feeds on: a unit-propagation cascade
Six clauses, one decision. Assigning x₁ = true forces x₂, then x₃, x₄, x₅ — each step is a clause with a single live literal — until clause 6 has none left: conflict. Walking the chain back, the whole conflict compresses to one decision, so the solver learns the short clause ¬x₁. Eternity II starves exactly this: its chains are one link long, so its learned clauses come out wide and useless.
Counts are exact for the constraint families shown, except seam disagreement, which treats colours as uniform (×(1−1/c)); real piece sets deviate a little. The seam encoding uses sequential at-most-one for the cell and piece constraints, as the compact encodings in Heule's paper do. The 10×10 ceiling and the full-board CNF sizes are the ones this page reports from community experiments.
Derive the sizes once by hand; they stop being folklore.
Placement variables.p=n2 pieces, 4 rotations, n2 cells:
xc,p,r gives n2⋅p⋅4=4n4 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.
Cell and piece constraints. Every cell holds exactly one placement:
one long clause plus, pairwise, (24n2) exclusions per cell.
Every piece is used at most once: another (24n2) per piece.
Pairwise at-most-one is quadratic; this is what compact encodings
(sequential, commander) reduce to O(4n2) clauses each, at the price of
auxiliary variables.
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
(4n2)2(1−1/c) pairs per seam if colours were uniform. At
n=16, c=17: 480×10242×1716≈4.7×108 clauses, the "hundreds of millions" reported for full-board
CNFs, recovered from first principles.
Heule's seam trick. Name the colour of each seam: 2n(n−1)⋅c
auxiliary variables (8,160 at full size). Now each placement implies
its four seam colours (at most 16n4 binary clauses) and disagreement is
forbidden once per seam, not once per pair: (2c) 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.
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(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 on the
table constraints is polynomial per node, and Régin's GAC alldifferent
filter runs a bipartite matching in O(mn) per call (see the
alldifferent page). 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.
The systematic study is due to Ansótegui, Béjar, Fernàndez and Mateu, in a
CP 2008 paper
and an extended
journal version in Constraints,
with a companion paper asking, verbatim,
how hard the commercial puzzle actually is.
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 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 for the
full literature trail.
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 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.
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. 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.