

![0_image_0.png](0_image_0.png)

The timetable propagator for cumulative will use the compulsory part of activity a in [0..2) to force sd ≥ 2. The explanation for this is Jsa ≤ 0K → Jsd ≥ 2K. The the precedence sd + 3 ≤ se forces se ≥ 5 with explanation Jsd ≥ 2K → Jse ≥ 5K.

Suppose next that search sets sb ≤ 2. There is no propagation from precedence constraints or the cumulative constraint. It does create a compulsory part of sb from
[2..7) but there is no propagation.

Suppose now that search sets sd ≤ 2. Then the precedence constraint se − 3 ≤ sd forces se ≤ 5 with explanation Jsd ≤ 2K → Jse ≤ 5K. This creates a compulsory part of d in [2..3) and a compulsory part of e in [5..7). In fact all the activities a, b, d and e are fixed now. Timetable propagation sees since all resources are used at time 5 then activity c cannot start before time 6. A reason for this is Jsb ≥ 2K∧Jsb ≤ 5K (which forces b to use 2 resources in [5..7)), plus Jse ≥ 5K ∧ Jse ≤ 5K (which forces e to use 2 resources in [5..7)), plus Jsc ≥ 3K (which forces c to overlap this time. Hence an explanation is Jsb ≥ 2K ∧ Jsb ≤ 5K ∧ Jse ≥ 5K ∧ Jse ≤ 5K ∧ Jsc ≥ 3K → Jsc ≥ 6K.

This forces a compulsory part of c at time 6 which causes a resource overload at that time. An explanation of the failure is Jsb ≥ 2K ∧ Jsb ≤ 5K ∧ Jse ≥ 5K ∧ Jse ≤ 5K ∧ Jsc ≥
6K ∧ Jsc ≤ 6K → *f ail*. The edges are shown in the conflict graph as dashed (for clarity).

The nogood generation process starts from this original explanation. It removes the last literal in the explanation by replacing it by its explanation. Replacing Jsc ≥ 6K by its explanation creates the new nogood Jsb ≥ 2K ∧ Jsb ≤ 5K ∧ Jse ≥ 5K ∧ Jse ≤ 5K ∧ Jsc ≥
3K ∧ Jsc ≤ 6K → *f ail*. Since this nogood has only one literal that was made true after the last decision level Jse ≤ 5K this is the 1UIP nogood. Rewritten as a clause it is Jsb ≤ 1K ∨ ¬Jsb ≤ 5K ∨ Jse ≤ 4K ∨ ¬Jse ≤ 5K ∨ Jsc ≤ 2K ∨ ¬Jsc ≤ 6K. ✷
After discovering a new nogood C the lazy clause generation solver, like a SAT solver, adds the clause C to the theory, and backtracks to the decision level of the second newest literal in nogood C. At this point we are guaranteed that the clause will unit propagate.

After unit propagation finishes search proceeds as usual.

Example 10. Continuing Example 9, the solver backtracks to the decision level of the