Example 5. Consider the propagator f for the precedence constraint sa + 2 ≤ sb from Example 1. When applied to the domains D(si) = [ 0 .. 15 ] for i ∈ {*a, b*} it obtains f(D)(sa) = [ 0 .. 13 ], and f(D)(sb) = [ 2 .. 13 ]. The clausal explanation of the change in domain of sa is Jsb ≤ 15K → Jsa ≤ 13K, similarly the change in domain of sb is
¬Jsa ≤ −1K → ¬Jsb ≤ 1K (Jsa ≥ 0K → Jsb ≥ 2K). These become the clauses ¬Jsb ≤ 15K ∨ Jsa ≤ 13K and Jsa ≤ −1K ∨ ¬Jsb ≤ 1K. ✷
The explaining clauses of the propagation are added to the database of the SAT solver on which unit propagation is performed. Because the clauses will always have the form C → l where C is a conjunction of literals true in the current assignment, and l is a literal not true in the current assignmet, the newly added clause will always cause unit propagation, adding l to the current assignment.

Example 6. Consider the propagation from Example 5. The clauses ¬Jsb ≤ 15K∨Jsa ≤ 13K and Jsa ≤ −1K ∨ ¬Jsb ≤ 1K are added to the SAT theory. Unit propagation infers that Jsa ≤ 13K = *true* and ¬Jsb ≤ 1K = *true* since ¬Jsb ≤ 15K and Jsa ≤ −1K are *false*,
and adds these literals to the assignment. Note that the unit propagation is not finished, since for example the implied literal Jsa ≤ 14K, can be detected *true* as well. ✷
The unit propagation on the added clauses C is guaranteed to be as strong as the propagator f on the original domains, i.e. if *domain*(A) v D then *domain*(A0) v f(D)
where A0is the resulting assignment after addition of C and unit propagation (see [24]
for the formal results).

Note that a single new propagation may be explainable using different set of clauses. In order to get maximum benefit from the explanation we desire a "strongest" explanation as possible. A set of clauses C1 is *stronger* than a set of clauses C2 if C2 implies C1. In other words, C1 restricts the search space at least as much as C2.

Example 7. Consider explaining the propagation of the start time of the activity c described in Example 3 and Figure 2(c). The domain change J5 ≤ scK arises from the compulsory parts of activity b and e as well as the fact that activity c cannot start before time 3. An explanation of the propagation is hence J3 ≤ scK ∧ J3 ≤ sbK ∧ Jsb ≤ 3K ∧ J3 ≤
seK ∧ Jse ≤ 4K → J5 ≤ scK.

We can observe that if 2 ≤ sc then the same domain change J5 ≤ scK follows due to the compulsory parts of activity b and e. Therefore, a stronger explanation is obtained by replacing the literal J3 ≤ scK by J2 ≤ scK.

Moreover, the compulsory parts of the activity b in the ranges [ 3 .. 3 ] and [ 5 .. 7 ] are not necessary for the domain change. We only require that there is not enough resources at time 4 to schedule task c. Thus the refined explanation can be further strengthened by replacing J3 ≤ sbK∧Jsb ≤ 3K by Jsb ≤ 4K which is enough to force a compusory part of sb at time 4. This leads to the stronger explanation J2 ≤ scK∧Jsb ≤ 4K∧J3 ≤ seK∧Jse ≤
4K → J5 ≤ scK.

In this example the final explanation corresponds to a pointwise explanation in Schutt et al. [27]. Here, those pointwise explanations are used to explain the timetable propagation. For a full discussion about the best way to explain cumulative propagation see [27].