[ 3 .. 7 ] respectively. This in turn causes the start times of activities d and e to become
[ 0 .. 0 ] and [ 3 .. 4 ] respectively creating compulsory parts in the ranges [ 0 .. 0 ] and [ 4 .. 4 ] respectively. The later causes the start time of activity c to become fixed at 5 generating the compulsory part in [ 5 .. 7 ] which causes that the start time of activity e becomes fixed at 3. This is illustrated in Figure 2(c). In this case the timetable propagation results in a final schedule in the right of Figure 1. ✷

## 2.2. Boolean Satisfiability

Let B be a set of Boolean variables. A *literal* l is Boolean variable b ∈ B or its negation
¬b. The negation of a literal ¬l is defined as ¬b if l = b and b if l ≡ ¬b. A *clause* C is a set of Boolean variables understood as a disjunction. Hence clause {l1*, . . . , l*n} is satisfied if at least one literal liis true. An *assignment* A is a set of Boolean literals that does not include a variable and its negation, i.e. @b ∈ B.{b, ¬b} ⊆ A. An assignment can be seen as a partial valuation on Boolean variables, {b 7→ true |b ∈ A} ∪ {b 7→ *false* |¬b ∈ A}. A
theory T is a set of clauses. A SAT problem (*T, A*) consists of a set of clauses T and an assignment over (some of) the variables occuring in T.

A Davis-Putnam-Loveland-Logemann (DPLL) SAT solver is a form of finite domain propation solver specialized for Boolean clauses. Each clause is propagated by so called unit propagation. Given an assignment A, unit propagation detects failure using clause C is such that {¬l | l ∈ C} ⊆ A, and unit propagation detects a new unit consequence l if C ≡ {l} ∪ C
0 and {¬l 0| l 0 ∈ C
0} ⊆ A, in which case it adds l to the current assignment A. Unit propagation continues until failure is detected, or no new unit consequences can be determined.

SAT solvers exhaustively apply unit propagation to the current assignment A to generate all the consequences possible A0. They then choose an unfixed Boolean variable b and create two equivalent problem (T, A0 ∪ {b}), (T, A0 *∪ {¬*b}) and recursively search these subproblems. The Boolean literals added to the assignment by choice are termed decision literals.

Modern DPLL based SAT solving is a powerful approach to solving combinatorial optimization problems because it records nogoods that prevent the search from revisiting similar parts of the search space. The SAT solver records an explanation for each unit consequence discovered (the clause that caused unit propagation), and on failure uses these explanations to determine a set of mutually incompatible decisions, a *nogood* which is added as a new clause to the theory of the problem. These nogoods drastically reduce the size of the search space needed to be examined. Another advantage of SAT solvers is that they track which Boolean variables are involved in the most failures (called *active* variables), and use a powerful autonomous search procedure which concentrates on the variables that are most active. The disadvantages of SAT solvers are the restriction to Boolean variables and the sometime huge models that are required to represent a problem because the only constraints expressible are clauses.