No piece may be used twice: one global all-different constraint over 256 cells. Jean-Charles Régin showed in 1994 how bipartite matching filters it completely in polynomial time; its per-colour cousin is the strongest propagator anyone has measured on edge matching, with one sharp caveat about mismatch-tolerant searches.
Underneath the colour matching, Eternity II carries a second global law: the 256 cells must take 256 distinct pieces. Written as a constraint, that is a single all-different over the whole board. Most solvers enforce it in the weakest possible way (when a piece is placed, cross it off everywhere else), which misses a whole class of dead positions: five cells whose remaining candidates draw on only four pieces are already unsolvable, and simple crossing-off will not notice until much later.
Jean-Charles Régin showed that the all-different constraint can be filtered completely, in polynomial time: every candidate that appears in no valid global assignment gets removed. The construction is pure graph theory:
This paper effectively founded the field of global constraints in constraint programming: a constraint over hundreds of variables, filtered to optimality by one combinatorial algorithm instead of being decomposed into weak pairwise checks. Incremental versions (Régin 1995; Mehlhorn & Thiel 2000) repair the matching after a few deletions instead of recomputing it, which is what makes it affordable inside a search loop.
The construction is easier to believe than to picture, so here it is on a six-piece instance built to contain a trap: cells C1 and C2 both draw on only pieces P1 and P2, a Hall set. Crossing-off sees nothing wrong with C3 holding P2 as a candidate; the matching argument proves it can never happen. Build the matching first (watch an augmenting path evict and re-route an earlier assignment), then run the filter and watch the strongly connected components expose every edge that no maximum matching can use.
Six pieces, six cells, feasible edges in between. First build a maximum matching by augmenting paths — watch a taken piece get re-routed. Then Régin's insight: orient the graph around the matching, compute its strongly connected components, and every unmatched edge that crosses two components belongs to no maximum matching. Delete them, soundly — here that forces two cells that simple crossing-off never notices.
The bipartite graph: an edge wherever a piece is still in a cell's candidate list.
The payoff to notice: three edges deleted, and two cells forced. C3 must take P3 and C6 must take P6, conclusions that pairwise reasoning would only reach after branching. That is what "filtering to optimality" means: after Régin's pass, every surviving candidate genuinely participates in some complete assignment.
The same run, in words:
One invocation from scratch is two graph passes:
For the piece-level all-different on Eternity II, vertices (256 cells + 256 pieces) and at most edges, so million edge operations for a full build. That is small change on modern hardware, and it is the worst case, from scratch, with maximally loose domains. Inside a search nobody rebuilds: the incremental versions cited above keep the previous matching, repair it with a few augmenting paths after each domain change, and re-run the linear SCC pass, which comes to near-linear re-filtering per node in practice. The per-colour variant is smaller still: one graph per colour class over only the half-edges showing that colour, 22 little matchings instead of one big one. The polynomial label is the point: this is complete filtering of a global constraint for graph-algorithm prices, not search prices.
The same theorem applies at two different levels on this puzzle.
Per colour. For each colour, the half-edges showing it must pair up perfectly across adjacent cells: a perfect-matching condition per colour class. Ansótegui, Béjar, Fernández and Mateu built exactly this propagator on Régin's theorem for edge-matching CSPs and called it the most powerful global constraint they had found for these puzzles. That matches this project's experience: the per-colour filter is the strongest propagator in the project's exact-matching engine, the ingredient that (together with arc consistency) lifts a plain backtracker to 449 of 480 edges in under a minute (measured on this project's engine, not independently replicated). It earns its keep late: the project gates it to deep positions, where domains are tight enough for matchings to fail and the cost is repaid.
Per piece. The direct reading, remaining pieces versus empty cells, catches the Hall-style traps that crossing-off misses: whole groups of cells competing for too few pieces, detected before the pairwise machinery sees any contradiction. Since no move is ever forced on this puzzle, a filter that reasons about groups rather than single cells is exactly the kind of leverage in short supply.
The per-colour filter assumes every colour must match exactly. A Blackwood-style search breaks that assumption on purpose: its break indices license a budget of mismatches at late depths, so a board the filter proves "impossible" may be exactly the 470 the search is hunting. Running the per-colour matching filter inside a mismatch-tolerant search is unsound, full stop. On this project's engine it is switched off in that regime, and dropping it (with the rest of the strict propagators) was part of a large single-thread speedup.
The piece-level all-different is the exception, and it matters: even a mismatch-tolerant search never uses a piece twice. Piece uniqueness stays strict when colour matching does not, so Régin's filter over pieces remains sound in precisely the regime where everything else in the propagation family breaks. It is the one strong global propagator available to a record engine.
The cost side of the ledger is above, and it is polynomial all the way down. The benefit side, though, has a hole in it: Régin's original paper benchmarks a 25-variable toy, and there is no published measurement of the filter on a 256-variable all-different shaped like Eternity II. This project has not built the piece-level version either; its promise inside mismatch-tolerant searches is an argument, not a number. Treat it as the best-reasoned open bet on the shelf: sound where nothing else strong is, cost known to be polynomial, payoff unmeasured.