The CP-SAT Propagator Registry and Solver Loop

Every constraint in CP-SAT that needs runtime inference — AllDifferent, LinearConstraint, AtMostOne, Cumulative — is implemented as a propagator: an object that inherits from CpPropagator in sat/constraint_programming_propagator.cc and registers itself with the solver at model-build time.

class CpPropagator {
 public:
  // Called when the solver wants this propagator to run.
  // Returns false if a conflict was detected.
  virtual bool Propagate() = 0;

  // Called when backjumping unwinds the trail past a level this
  // propagator cares about. Lets the propagator undo any internal state.
  virtual void Untrail(int trail_index) {}

  // The propagator registers which integer variables it watches.
  // The solver calls Propagate() only when one of those variables
  // has had its domain reduced since the last call.
  void RegisterWith(GenericLiteralWatcher* watcher);
};

The registry itself lives in SatSolver as an ordered list of CpPropagator* pointers. The solver iterates them in registration order during every CP propagation round. Order matters for efficiency (cheaper propagators first reduces the cost per round) but not for correctness.

Now we can read the main loop in sat/sat_solver.cc with real understanding. The loop is not simply “CDCL OR CP” — it is a nested cycle where CDCL runs first, then CP, and neither layer branches until both have quiesced.

flowchart TD
  A([Branch: add decision to trail]) --> B
  B[CDCL Boolean Propagation
unit-propagate all clauses
original + learned + lazy] --> C{New assignments?}
  C -- Yes --> B
  C -- No: CDCL quiesced --> D
  D[Call CP Propagators in order
for each registered CpPropagator] --> E{Any propagator
posted new literal?}
  E -- Yes: re-run CDCL --> B
  E -- No: full quiescence --> F
  F{All variables
assigned?} -- Yes --> G([SAT — solution found])
  F -- No --> A
  B -- Conflict detected --> H[Conflict Analysis
implication graph
first-UIP cut]
  D -- Conflict detected --> H
  H --> I[Learn clause
post to DB
backjump on trail]
  I --> B
  style B fill:#1e3a8a,color:#bfdbfe
  style D fill:#4c1d95,color:#ddd6fe
  style H fill:#7f1d1d,color:#fca5a5
  style I fill:#065f46,color:#a7f3d0
  style F fill:#374151,color:#d1d5db

The ordering rule is important and non-obvious: CDCL always runs first. If a branch decision immediately propagates to a conflict via a Boolean clause, there is no point calling CP propagators — the solver needs to backjump immediately. Only when the Boolean layer has nothing more to say does the solver hand control to CP propagators. And when a CP propagator posts a new literal, the loop immediately returns to CDCL — the new trail entry may wake Boolean watch-lists that fire further unit clauses.

When a CP propagator detects that a domain reduction is forced — or that the current assignment creates a conflict — it cannot just silently update some internal state. It must communicate with the CDCL engine in CDCL’s language: Boolean literals and clauses.

This is lazy clause generation (LCG), first described in the constraint-programming literature by Ohrimenko, Stuckey, and Codish in 2009. ^{[Lazy Clause Generation Reengineered for Constraint Programming]}

The key insight: if a later conflict involves TeachA_R1_T4, conflict analysis will chase the reason pointer on that trail entry, find the lazy clause (¬TeachA_R1_T3 ∨ ¬TeachA_R1_T4), and resolve against it — just as it would against any original clause. The first-UIP cut and the backjump level computation from the previous lesson apply unchanged. CP and CDCL share the same trail infrastructure completely.

For lazy clause generation to work, there must be a systematic mapping from integer domain facts (e.g., “X ≥ 3”) to Boolean literals that CDCL can reason about. This encoding lives in sat/integer.h.

For a Boolean variable like TeachA_R1_T3 ∈ {0, 1}, there are only two literals: [X ≥ 1] (which equals “X is True”) and [X ≤ 0] (which equals “X is False”). For a larger integer like RoomSlot ∈ {0, 1, 2, 3, 4}, there are eight distinct bound literals — one per inequality boundary.

These literals appear on the trail interleaved with ordinary Boolean literals from original clauses and decisions. A CDCL propagation step cannot tell them apart: a literal is a literal, a reason clause is a reason clause, and the implication graph reconstruction machinery works identically.

The solver loop alternates layers until neither can make progress. But what does “quiescence” mean precisely, and what happens to both layers during conflict resolution?

Quiescence is the state where:

1. CDCL Boolean propagation has advanced qhead to the end of the trail — every trail entry has been checked for its effect on watching clauses.
2. Every registered CP propagator has been called and none has posted a new literal or clause.

Only at full quiescence does the solver invoke its branching heuristic (VSIDS from the previous lesson) to choose the next decision variable.