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:
Build the bipartite graph of cells versus pieces, with an edge wherever a
piece is still in a cell's domain.
Compute a maximum matching (Hopcroft–Karp, O(mn)). If it fails
to cover every cell, the position is dead; backtrack immediately.
Orient the graph around the matching and compute its strongly connected
components (Tarjan, linear time). A theorem of Berge then identifies, in
one pass, exactly which edges belong to some maximum matching.
Every edge that belongs to none is a candidate that can be deleted from
its cell's domain, soundly.
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.
▶Interactive: Régin's matching filter at workExplore →
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.
matching 0/60 edges deleted
The bipartite graph: an edge wherever a piece is still in a cell's candidate list.
Domains
C1P1P2
C2P1P2
C3P2P3
C4P3P4P5
C5P4P5
C6P5P6
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.
Build the bipartite graph. Cells on one side, pieces on the other, an
edge wherever a piece is still in a cell's domain: six cells, six pieces,
thirteen edges in the demo.
Grow a matching by augmenting paths. C1 takes P1. C2 also wants P1:
instead of giving up, follow the alternating path C2–P1–C1–P2. P1 is
taken, but its owner C1 has a free alternative, P2. Flip every edge on the
path: C1 slides to P2, C2 gets P1, and the matching has grown by one.
Repeat until every cell is covered. If some cell ever exhausts its paths,
there is no complete assignment and the search backtracks on the spot.
Orient the graph. Matched edges point cell → piece; unmatched edges
point piece → cell. Now an alternating cycle in the original graph is a
directed cycle in this one.
Compute strongly connected components (Tarjan, one linear pass). In
the demo, {C1, C2, P1, P2} form one component (they trade their two
pieces around a cycle) and {C4, C5, P4, P5} another.
Apply Berge's rule. An unmatched edge can join some maximum matching
only if it lies on an alternating cycle (same SCC) or on an alternating
path from a free vertex (none here; the matching is perfect). Everything
else is dead: C3–P2, C4–P3 and C6–P5 each cross two components, so they
are deleted, provably rather than heuristically.
Read off the reductions. C3's domain drops to {P3}, C6's to {P6}:
two forced placements found without a single branch.
Maximum matching via Hopcroft–Karp: O(mn) for m feasible
edges over n vertices, the dominant term.
SCC decomposition via Tarjan: O(n+m), linear, plus the same again
to sweep the edges and delete.
For the piece-level all-different on Eternity II, n=512 vertices (256
cells + 256 pieces) and m at most 256×256=65,536 edges, so
mn≈1.5 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.