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.
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.
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.
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.
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.
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.