
## 2.3.3. Nogood Generation

Since all the propagation steps in lazy clause generation have been mapped to unit propagation on clauses, we can perform nogood generation just as in a SAT solver.

The nogood generation is based on an *implication graph* and the *first unique implication point* (1UIP). The graph is a directed graph where nodes represent fixed literals and directed edges reasons why a literal became *true*, and is extended as the search progresses. Each unit propagation marks the literal it makes true with the clause that caused the unit propagation. The true literals are kept in a stack showing the order that they were determined as true by unit consequence or decisions.

For clarity purpose, we do not differentiate between literal and node. A literal is fixed either by a search decision or unit propagation. In the first case the graph is extended only by the literal and in the second case by the literal and incoming edges to that literal from all other literals in the clause on that the unit propagation assigned the *true* value to the literal.

Example 8. Consider the strongest explanation J2 ≤ scK ∧ Jsb ≤ 4K ∧ J3 ≤ seK ∧ Jse ≤
4K → J5 ≤ scK from Example 7. It is added to the SAT database as clause ¬J2 ≤
scK ∨ ¬Jsb ≤ 4K ∨ ¬J3 ≤ seK ∨ ¬Jse ≤ 4K ∨ J5 ≤ scK and unit propagation sets J5 ≤ scK true. Therefore the implication graph is extended by the edges J2 ≤ scK → J5 ≤ scK,
Jsb ≤ 4K → J5 ≤ scK, J3 ≤ seK → J5 ≤ scK, and Jse ≤ 4K → J5 ≤ scK. ✷
Every node and edge is associated with the search level at which they are added to the graph. Once a conflict encounters a nogood which is the 1UIP in LCG is calculated based on the implication graph. A conflict is recognized when the unit propagation reaches a clause where all literals are false. This clause is the starting point of the analysis and builds a first tentative nogood. Now, literals in the tentative nogood are replaced by the literals from its incoming edges in the reverse order of the graph extension. This process holds on until the tentative nogood includes exactly one literal from the current decision level. The resulting nogood is called *1UIP* (first unique implication point), since it corresponds to a cut through the implication graph that has one node in the current decision level.

Example 9. Considered the Rcpsp/max instance from Example 1 on page 2.

Assume an initial domain of D*init* = [ 0 .. 15 ] then after the initial propagation of the precedence constraints the domains are D(sa) = [ 0 .. 8 ], D(sb) = [ 2 .. 10 ], D(sc) = [ 3 .. 12 ], D(sd) = [ 0 .. 10 ], and D(sb) = [ 3 .. 13 ]. Note that no tighter bounds can be inferred by the cumulative propagator.

Assume search now sets sa ≤ 0. This sets the literal Jsa ≤ 0K as true, and unit propagation on the domain clauses will set Jsa = 0K, Jsa ≤ 1K, Jsa ≤ 2K, etc. In the remainder of the example we will ignore propagation of the domain clauses and concentrate on the "interesting propagation".

The precedence constraint sc − 6 ≤ sa will force sc ≤ 6 with explanation Jsa ≤ 0K →
Jsc ≤ 6K. The the precedence constraint sb + 1 ≤ sc will force sb ≤ 5 with explanation Jsc ≤ 6K → Jsb ≤ 5K.