Propagate to Fixpoint - Constraint Propagation (CP-SAT)

Propagation is iterative: one constraint can make the next constraint remove more values. Applying B<C after A<B creates singleton domains for B and C, which means local information has traveled along the chain. The engine keeps applying constraints until a full pass changes nothing, the fixpoint condition.

highlighted = computed this step

B loses its high endpoint

B loses 3. The B<C constraint now sees B's current upper endpoint as unsupported. Why: B must stay below C, and that endpoint leaves no larger candidate value available for C.

B\not=3

C loses low endpoints

C loses 1 and 2. C must be larger than B, so low endpoints that cannot sit above any current B value are pruned. Why: each remaining value needs support on the other side of the precedence relation.

C\notin\{1,2\}

Keep applying constraints

The domains are now A{1,2} B{2} C{3}. This is the propagation loop in motion: one constraint changes a domain, then the next pass may make a neighboring constraint stronger. Why: we repeat until a full pass removes nothing. That fixpoint is a mechanical stopping rule, not a promise that every variable is assigned.

\text{repeat until no domain changes}

Diagram note

Just-pruned cells show the current B<C application; earlier-pruned cells stay marked as already removed. The diagram distinguishes this step's pruning from the history that made it possible. Read it as a state in a process, not as a standalone answer. Pixel positions are rounded for layout; every number shown is exact.

\text{propagation records each exact domain reduction}