Lazy Clause Generation: CP-SAT's Hybrid Core

In pure CP, when a propagator removes a value from a domain, it just does it — no record is kept of why. If search backtracks, the same removal is re-discovered the same way at every subsequent visit. There is no memory across branches.

Lazy Clause Generation (LCG) breaks that cycle. Every domain reduction must come with an explanation: a minimal set of currently-true literals that together imply the reduction. That explanation is immediately turned into a SAT clause and handed to the CDCL engine. Now if the same sub-configuration appears on a later branch, the clause fires via unit propagation — no propagator call needed.

The clause has exactly one positive literal — the consequence — and one negative literal per reason. ^{[Explaining Propagators in CP-SAT]} This matches the structure of the asserting clauses you saw in the CDCL lesson: a clause with exactly one literal at the current decision level, enabling unit propagation immediately after backjumping.

The OR-Tools C++ source defines the explanation contract in sat/integer.h. Every propagator that calls integer_trail->Enqueue(...) to raise a lower bound or lower an upper bound passes a reason object — either a direct vector of literals, or a callback of type LazyReasonFunction. ^{[OR-Tools CP-SAT source: sat/integer.h]}

// Explanation via a pre-computed literal vector (eager — rare in practice)
bool Enqueue(IntegerLiteral i_lit,
             absl::Span<const Literal> literal_reason,
             absl::Span<const IntegerLiteral> integer_reason);

// Explanation via a lazy callback (preferred — most propagators use this)
bool EnqueueWithLazyReason(IntegerLiteral i_lit,
                           int id,
                           IntegerValue propagation_slack,
                           LazyReasonInterface* lazy_reason);

The lazy form stores only (id, propagation_slack) — a lightweight token — on the trail. When CDCL conflict analysis reaches this trail entry, it calls:

class LazyReasonInterface {
 public:
  virtual void Explain(int id,
                       IntegerValue propagation_slack,
                       IntegerVariable var_to_explain,
                       std::vector<Literal>* literals,
                       std::vector<IntegerLiteral>* integer_literals) = 0;
};

Explain() receives the same id and slack token it stored, plus the variable whose bound it is explaining, and fills literals and integer_literals with the reason set. The propagator’s Explain() implementation reconstructs the conflict from its own internal state at that point — which is valid because CDCL conflict analysis only runs while the trail is still at or above the level of the propagation being explained.

The linear propagator in sat/linear_propagator.cc is the canonical example. ^{[OR-Tools CP-SAT source: sat/linear_propagator.cc]} When propagating a constraint of the form $a_1 x_1 + a_2 x_2 + \cdots + a_n x_n \leq b$, and it determines that $x_j$‘s upper bound must drop, it stores an id pointing into the constraint’s coefficient array. On Explain(), it recomputes which other variables’ current bounds account for the slack that forced $x_j$‘s reduction.

The cumulative constraint — “a set of jobs, each needing some resource capacity, must not exceed total capacity at any time” — is the core of teacher/room/time scheduling. It is also the best illustration of what a CP explanation looks like in practice.

Suppose jobs A and B are both assigned to slots [2, 5) (both need the one machine), and job C has current lower bound lb(C) = 3. The cumulative propagator detects that [2, 5) is over-subscribed — capacity 1, but two jobs overlap there. It concludes: job C cannot start before slot 5 (because slots 2–4 are already fully booked). It calls EnqueueWithLazyReason(lb_lit(C, 5), id, slack).

When CDCL later asks for the explanation, Explain() returns:

$(\text{start}_A \geq 2) \wedge (\text{start}_A + 3 > 2) \wedge (\text{start}_B \geq 2) \wedge (\text{start}_B + 3 > 2) \Rightarrow \text{start}_C \geq 5$

Negated as a clause: $\neg(\text{start}_A \geq 2) \vee \neg(\text{start}_A + 3 > 2) \vee \neg(\text{start}_B \geq 2) \vee \neg(\text{start}_B + 3 > 2) \vee (\text{start}_C \geq 5)$.

This clause is exactly as tight as the propagation demands — it includes only the bounds of A and B that matter for the conflict window, not every constraint touching those variables. A looser explanation (including irrelevant facts) would still be sound, but would produce a clause that fires in fewer future situations, wasting the learning opportunity.

The widget below lets you manipulate a 3-job cumulative scenario and watch the explanation clause being built step by step, mirroring exactly what Explain() does in C++.

Recall from the CDCL lesson: when CDCL hits a conflict (a variable forced to both true and false), it walks the implication graph backwards from the conflict node, applying the first-UIP cut to find the asserting clause. ^{[Lazy Clause Generation: Combining the Power of SAT and CP for Solving Long-Horizon Hybrid Problems]}

In CP-SAT, the implication graph includes both SAT implications (unit propagation via two-watched literals) and CP implications (bounds tightened by propagators). The boundary between them is invisible to conflict analysis — every trail entry has a reason, whether that reason came from a SAT clause or from a CP propagator’s Explain() callback.

flowchart TD
  D1["Decision: start_A = 2"]:::decision
  D2["Decision: start_B = 2"]:::decision
  P1["Propagation via 2WL\n(some other clause)"]:::sat
  CP1["CP: Cumulative fires\nlb(C) ≥ 5"]:::cp
  CP2["CP: AtMostOne fires\n¬assign_C_slot3"]:::cp
  CONF["Conflict: C needs slot 3\nbut lb(C) ≥ 5"]:::conflict
  D1 --> CP1
  D2 --> CP1
  P1 --> CP2
  CP1 --> CONF
  CP2 --> CONF
  classDef decision fill:#7c3aed,color:#fff,stroke:none
  classDef sat fill:#0e7490,color:#fff,stroke:none
  classDef cp fill:#059669,color:#fff,stroke:none
  classDef conflict fill:#dc2626,color:#fff,stroke:none

When conflict analysis reaches lb(C) ≥ 5 (a CP-propagated node), it calls Explain() on the cumulative constraint. The returned literals become the predecessors of that node in the implication graph. Analysis continues through them as if they had always been explicit. The resulting learned clause may reference a mixture of SAT literals and integer bound literals — that is fine, because both live in the same Boolean trail.

Level 3: [start_A = 2]  ← decision
Level 3: [start_B = 2]  ← decision
Level 3: lb(C) ≥ 5       ← cumulative propagator, lazy reason id=17
Level 3: ¬assign_C_sl3  ← AtMostOne propagator (from prior lesson example)
  → CONFLICT: C must be in slot 3, but lb(C)≥5 rules that out

This is the payoff. The widget below models a small scheduling problem under all three regimes — vary the number of jobs, time slots, and constraint tightness to see backtrack counts and clause counts diverge.

Pure CP re-solves every sub-problem from scratch. When it backtracks from a dead end caused by slots 2–5 being overloaded, it has no record of why it failed — the next branch may hit exactly the same dead end. Arc-consistency propagation is strong but local; it cannot reuse knowledge across backtrack points.

Pure SAT encodes everything eagerly. Before search even starts, it must generate clauses for every possible bound relationship — for $n$ jobs over a horizon of $H$ slots, that is $O(n^2 H)$ clauses covering constraints that may never be relevant. The CDCL engine then churns through a bloated database where most clauses are never queried.

LCG generates clauses only for the propagations that actually fire. In practice, on a 10-job scheduling problem, roughly 80–95% of the clauses a pure SAT encoding would pre-generate are never needed. The ones that are generated carry CP-level reasoning — they encode statements like “if A occupies slots 2–5 and B occupies slots 3–6, then C cannot start before slot 6” — far more semantically rich than the flat pairwise exclusions a SAT encoder would produce. ^{[Lazy Clause Generation: Combining the Power of SAT and CP for Solving Long-Horizon Hybrid Problems]}