When Propagation Isn't Enough - Constraint Propagation (CP-SAT)

Propagation is powerful but not complete. A weaker model can reach a fixpoint with domains still larger than one, so the solver must branch and then propagate again. This lesson separates two ideas that are easy to confuse: a fixpoint means no more pruning is available from the current rules, while a solution means every variable has been forced.

highlighted = computed this step

Reduced but unsolved

With only A<B, the fixpoint domains are A{1,2} B{2,3} C{1,2,3}. This is reduced, but not solved. Why: C is untouched, and A and B still each have more than one candidate, so the grid does not identify one assignment.

\text{some domains still have multiple candidates}

Propagation gets stuck

Another pass removes nothing. That does not mean the problem is solved; it means this propagator has reached a fixpoint. Why: local precedence reasoning has reached its limit for this weaker model.

\text{fixpoint does not always mean solved}

Then search branches

A CP-SAT solver alternates propagation with search. After propagation stalls, a branch fixes a candidate and propagation starts again. Why: branching supplies a new assumption, and propagation checks what that assumption forces or rules out.

\text{propagate}\rightarrow\text{branch}\rightarrow\text{propagate}

Diagram note

Propagation is sound here, but not complete: it never removes a feasible value, yet it may leave choices. The honest boundary is the propagate-then-branch loop, not a promise that propagation alone solves every instance. A real solver keeps this loop going: prune what is forced, branch when stuck, then prune again under the new assumption. Pixel positions are rounded for layout; every number shown is exact.

\text{sound pruning can still need search}