# Exact methods

> Solvers that can prove things: SAT and CSP encodings, integer programming and its relaxations, exact-cover, meet-in-the-middle, and iterated projection maps. Complete methods stall on the full board, but their verdicts earn their keep as impossibility proofs on sub-boards.

- Canonical page (with interactive figures/demos): https://eternity2.dev/research/build/exact/
- Updated: 2026-07-13

---
Solvers that can prove things: SAT and CSP encodings, integer programming and its relaxations, exact-cover, meet-in-the-middle, and iterated projection maps. Complete methods stall on the full board, but their verdicts earn their keep as impossibility proofs on sub-boards.

The pages below go technique by technique: what each is in a line, what it
actually reached on the real 16×16 board, where it stops, and the labs and
measurements to back it. For the whole territory at once, start with
[a map of every known approach](/research/build/approaches-map).

## Pages in this section

- [Exact cover and dancing links](https://eternity2.dev/research/build/exact/exact-cover-dlx) — Eternity II states cleanly as an exact-cover problem, and Knuth's Algorithm X with dancing links is the classic machine for those. Where it genuinely shines (small boards, exhaustive counting) and the two reasons it does not crack the 16×16: an unshrunk search tree, and no partial credit.
- [Meet in the middle](https://eternity2.dev/research/build/exact/meet-in-the-middle) — Enumerate two halves of a problem and join them on a shared interface, trading memory for an exponent cut in half. The classic Horowitz–Sahni trick, what it looks like on bands of the board, and what this project's BANDSAW experiment measured, including the one-sided method that beat it.
- [SAT and CSP encodings](https://eternity2.dev/research/build/exact/sat-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.
- [LP and ILP relaxations: half a piece everywhere](https://eternity2.dev/research/build/exact/lp-relaxations) — Write Eternity II as an integer program, drop the integrality, and a linear solver reaches zero error in seconds, with 30% of one piece and 20% of another sharing a corner. Eighteen years of community campaigns measured where the fractional comfort ends: a plateau at 420–440 edges the moment the pieces must be whole, an ILP wall at 8×8, and an academic best of 461-in-an-hour. What the optimizer's road teaches, and where LP still earns its keep.
- [Iterated maps and divide-and-concur](https://eternity2.dev/research/build/exact/iterated-maps) — The physicist's attack on constraint satisfaction: split the puzzle into two constraint sets that are each easy to project onto, then iterate a map whose fixed points are solutions. Veit Elser's method made the cover of PNAS, yet on the Eternity II list it remains a road admired, tested once, and never marched down.

## Related

- [A map of every known approach](https://eternity2.dev/research/build/approaches-map) — The survey the community keeps asking for and never finds: every family of attack tried on Eternity II, what each one actually reached, where it walls out, and a link to the deep page. One organising insight runs through all of them.
- [The techniques](https://eternity2.dev/research/build/techniques) — The technique shelf: the algorithms and pruning ideas that recur in every serious Eternity II solver, each with what it is, what it costs, and what it actually bought when measured on this puzzle.