Classical Satisfiability Algorithms
IA085: Satisfiability and Automated Reasoning
Martin Jonáš
FI MUNI, Spring 2024
Last Time
• basic logical notions (entailment, equivalence, satisfiability, . . .)
• applications of satisfiability,
• conversion of a formula to equisatisfiable CNF of linear size
Today, we assume that all formulas are in CNF.
1 / 35
Our Goal
An algorithm that can decide satisfiability of formulas with thousands of variables
and millions of clauses.
2 / 35
Exhaustive search
Exhaustive search
1 ExhaustiveSearch(formula Φ) {
2 foreach truth assignment µ to Atoms(Φ)
3 res ← evaluate ϕ under µ
4 if res == ⊤
5 return SAT
6 return UNSAT
7 }
3 / 35
Exhaustive search in practice
• virtually never used in practice
• for unsatisfiable instances always needs 2|Atoms(φ)| steps
• for satisfiable instances can easily need exponential number of steps
Just buy a big powerful GPU?
• atoms on Earth ∼ 1050 ∼ number of truth assignments to 166 variables
• atoms in the universe ∼ 1080 ∼ number of truth assignments to 266 variables
4 / 35
Propositional resolution
Resolution rule
Rule for deriving new clauses from existing ones
{A, l1, . . . , ln} {¬A, l′
1, . . . , l′
m}
{l1, . . . , ln, l′
1, . . . , l′
m}
In general form
A ∨ φ ¬A ∨ ψ
φ ∨ ψ
Notation and terminology
• Resolve(x, C1, C2) returns the resulting formula
• Resolve(x, C1, C2) is called resolvent of C1 and C2 on x
Correctness
C1 ∧ C2 |= Resolve(x, C1, C2)
5 / 35
Resolution rule: notable instances
A ¬A ∨ B
B
6 / 35
Resolution rule: notable instances
A ¬A ∨ B
B =
A A → B
B = modus ponens
6 / 35
Resolution rule: notable instances
A ¬A ∨ B
B =
A A → B
B = modus ponens
¬B ¬A ∨ B
¬A =
¬B A → B
¬A = modus tollens
6 / 35
Resolution rule: notable instances
A ¬A ∨ B
B =
A A → B
B = modus ponens
¬B ¬A ∨ B
¬A =
¬B A → B
¬A = modus tollens
¬A ∨ B ¬B ∨ C
¬A ∨ C
6 / 35
Resolution rule: notable instances
A ¬A ∨ B
B =
A A → B
B = modus ponens
¬B ¬A ∨ B
¬A =
¬B A → B
¬A = modus tollens
¬A ∨ B ¬B ∨ C
¬A ∨ C =
A → B B → C
A → C = transitivity
6 / 35
Proving unsatisfiability by resolution
Observations
• if C1, C2 ∈ Φ and R is a resolvent of C1 and C2, then Φ |= R
• therefore Φ ≡ Φ ∪ {R}
7 / 35
Proving unsatisfiability by resolution
Observations
• if C1, C2 ∈ Φ and R is a resolvent of C1 and C2, then Φ |= R
• therefore Φ ≡ Φ ∪ {R}
Resolution method
• extend Φ with all possible resolvents of clauses from Φ
• if ∅ ∈ Φ at some point, return UNSAT
• if no more clauses can be derived and ∅ ̸∈ Φ, return SAT
7 / 35
Proving unsatisfiability by resolution
{{A, B},
{¬B, C},
{¬B, ¬C},
{¬A, ¬B, ¬D},
{¬A, B, ¬D},
{¬A, B, D}
8 / 35
Proving unsatisfiability by resolution
{{A, B},
{¬B, C},
{¬B, ¬C},
{¬A, ¬B, ¬D},
{¬A, B, ¬D},
{¬A, B, D}
8 / 35
Proving unsatisfiability by resolution
{{A, B},
{¬B, C},
{¬B, ¬C},
{¬A, ¬B, ¬D},
{¬A, B, ¬D},
{¬A, B, D}
{¬B},
8 / 35
Proving unsatisfiability by resolution
{{A, B},
{¬B, C},
{¬B, ¬C},
{¬A, ¬B, ¬D},
{¬A, B, ¬D},
{¬A, B, D}
{¬B},
8 / 35
Proving unsatisfiability by resolution
{{A, B},
{¬B, C},
{¬B, ¬C},
{¬A, ¬B, ¬D},
{¬A, B, ¬D},
{¬A, B, D}
{¬B},
{A},
8 / 35
Proving unsatisfiability by resolution
{{A, B},
{¬B, C},
{¬B, ¬C},
{¬A, ¬B, ¬D},
{¬A, B, ¬D},
{¬A, B, D}
{¬B},
{A},
8 / 35
Proving unsatisfiability by resolution
{{A, B},
{¬B, C},
{¬B, ¬C},
{¬A, ¬B, ¬D},
{¬A, B, ¬D},
{¬A, B, D}
{¬B},
{A},
{¬A, B},
8 / 35
Proving unsatisfiability by resolution
{{A, B},
{¬B, C},
{¬B, ¬C},
{¬A, ¬B, ¬D},
{¬A, B, ¬D},
{¬A, B, D}
{¬B},
{A},
{¬A, B},
8 / 35
Proving unsatisfiability by resolution
{{A, B},
{¬B, C},
{¬B, ¬C},
{¬A, ¬B, ¬D},
{¬A, B, ¬D},
{¬A, B, D}
{¬B},
{A},
{¬A, B},
{B},
8 / 35
Proving unsatisfiability by resolution
{{A, B},
{¬B, C},
{¬B, ¬C},
{¬A, ¬B, ¬D},
{¬A, B, ¬D},
{¬A, B, D}
{¬B},
{A},
{¬A, B},
{B},
8 / 35
Proving unsatisfiability by resolution
{{A, B},
{¬B, C},
{¬B, ¬C},
{¬A, ¬B, ¬D},
{¬A, B, ¬D},
{¬A, B, D}
{¬B},
{A},
{¬A, B},
{B},
∅ }
8 / 35
Resolution Method: Properties
Theorem (Soundness)
If the resolution method returns UNSAT, the formula Φ is unsatisfiable.
Theorem (Completeness)
If the formula is unsatisfiable, the resolution method returns UNSAT.
9 / 35
Resolution Method: Properties
Resolution method is not used in practice
• the size of Φ never decreases
• the size of Φ grows quickly (often exponentially)
• as presented, the algorithm is not deterministic
10 / 35
Systematic resolution: Davis-Putnam algorithm
Davis-Putnam algorithm (1960)
• eagerly apply simple resolution cases first -- unit resolution (unit
propagation)
• fix an order of variables in which to resolve
• for a variable x, use resolution on all clauses that can be resolved on x at
once and remove the original clauses
11 / 35
Davis-Putnam algorithm: Unit propagation
Variable assignment
• for example
{A, B}, {C, ¬D}, {¬A, D}
A
= {{C, ¬D}, {D}}
• Φ v
= {C \ {¬v} | C ∈ Φ and v ̸∈ C}
• similarly for Φ ¬v
Unit propagation
• if Φ contains a unit clause ({l} ∈ Φ), we can directly assign its value
• for example
{{A, ¬B}, {B}, {B, C}, {C, ¬D, A}} {{A}, {C, ¬D, A}}
12 / 35
Davis-Putnam algorithm: Variable elimination
• divide Φ = Ψ ∪ Ψx ∪ Ψ¬x where clauses in Ψ do not contain x, clauses in Ψx
contain x positively, and Ψ¬x contain x negatively
• EliminateVar(x, Φ) = Ψ ∪ {Resolve(x, C1, C2) | C1 ∈ Ψx, C2 ∈ Ψ¬x} without
tautological clauses
Φ = {{A, B}, {¬B, C}, {¬B, ¬C}, {¬A, ¬B, ¬D}, {¬A, B, ¬D}, {¬A, B, D}}
EliminateVar(A, Φ) = {{¬B, C}, {¬B, ¬C},
{B, ¬B, ¬D},
{B, ¬D},
{B, D}}
13 / 35
Davis-Putnam algorithm: Variable elimination
• divide Φ = Ψ ∪ Ψx ∪ Ψ¬x where clauses in Ψ do not contain x, clauses in Ψx
contain x positively, and Ψ¬x contain x negatively
• EliminateVar(x, Φ) = Ψ ∪ {Resolve(x, C1, C2) | C1 ∈ Ψx, C2 ∈ Ψ¬x} without
tautological clauses
Φ = {{A, B}, {¬B, C}, {¬B, ¬C}, {¬A, ¬B, ¬D}, {¬A, B, ¬D}, {¬A, B, D}}
EliminateVar(A, Φ) = {{¬B, C}, {¬B, ¬C},
{B, ¬B, ¬D},
{B, ¬D},
{B, D}}
13 / 35
Davis-Putnam Algorithm
1 DP(formula Φ):
2 while Φ contains unit clause {l}:
3 Φ ← Φ l
4
5 if Φ = ∅ return SAT
6 if ∅ ∈ Φ return UNSAT
7
8 v ← PickVariable(Φ)
9 Φ ← EliminateVar(v, Φ)
10 return DP(Φ)
14 / 35
Davis-Putnam algorithm: Properties
Theorem (Soundness)
If DP(Φ) returns UNSAT, the formula Φ is unsatisfiable.
Theorem (Completeness)
If the formula Φ is unsatisfiable, DPLL(Φ) returns UNSAT.
Proof idea.
Invariant: at every step, the formula Φ is equisatisfiable with the original.
• Unit propagation is satisfiability preserving.
• Variable elimination is satisfiability preserving.
15 / 35
Davis-Putnam algorithm: Properties
Theorem (Soundness)
If DP(Φ) returns UNSAT, the formula Φ is unsatisfiable.
Theorem (Completeness)
If the formula Φ is unsatisfiable, DPLL(Φ) returns UNSAT.
Proof idea.
Invariant: at every step, the formula Φ is equisatisfiable with the original.
• Unit propagation is satisfiability preserving.
• Variable elimination is satisfiability preserving.
Corollary (Complexity)
15 / 35
Davis-Putnam algorithm: Properties
Theorem (Soundness)
If DP(Φ) returns UNSAT, the formula Φ is unsatisfiable.
Theorem (Completeness)
If the formula Φ is unsatisfiable, DPLL(Φ) returns UNSAT.
Proof idea.
Invariant: at every step, the formula Φ is equisatisfiable with the original.
• Unit propagation is satisfiability preserving.
• Variable elimination is satisfiability preserving.
Corollary (Complexity)
Unless P = NP, the procedure DP does not run in polynomial time.
15 / 35
Resolution lower bounds
Pigeonnhole formula PHPn
• Can n + 1 pigeons be assigned to n boxes such that there is at most one
pigeon in one box?
• variables xi,j -- pigeon i is in the box j
• for each 1 ≤ i ≤ n + 1 a clause 1≤j≤n xi,j
• for each 1 ≤ j ≤ n and 1 ≤ i < i′ ≤ n + 1 a clause ¬xi,j ∨ ¬xi′,j
• obviously unsatisfiable
16 / 35
Resolution lower bounds
Pigeonnhole formula PHPn
• Can n + 1 pigeons be assigned to n boxes such that there is at most one
pigeon in one box?
• variables xi,j -- pigeon i is in the box j
• for each 1 ≤ i ≤ n + 1 a clause 1≤j≤n xi,j
• for each 1 ≤ j ≤ n and 1 ≤ i < i′ ≤ n + 1 a clause ¬xi,j ∨ ¬xi′,j
• obviously unsatisfiable
Theorem (Haken, 1985)
Every resolution proof of PHPn has size 2Ω(n).
16 / 35
Davis-Putnam-Logemann-Loveland
algorithm (DPLL)
DPLL
Davis-Putnam-Logemann-Loveland algorithm (1962)
• replace the resolution step in DP by variable assignment
• assign one value; if UNSAT, backtrack and try the opposite value
• eagerly apply unit propagation whenever possible
17 / 35
DPLL
1 DPLL(formula Φ):
2 while Φ contains unit clause {l}:
3 Φ ← Φ l
4
5 if Φ = ∅ return SAT
6 if ∅ ∈ Φ return UNSAT
7
8 v ← PickVariable(Φ)
9 if DPLL(Φ v
) == SAT:
10 return SAT
11 return DPLL(Φ ¬v
)
18 / 35
DPLL: Example
{{A, B}, {¬A, B}, {¬A, C, ¬B}, {¬A, ¬C, ¬B}}
{{B}, {C, ¬B}, {¬C, ¬B}} {{B}}
{{C}, {¬C}} ∅
SAT
{∅}
UNSAT
A
B
C
¬A
B
19 / 35
DPLL: Example
{{A, B}, {¬A, B}, {¬A, C, ¬B}, {¬A, ¬C, ¬B}}
{{B}, {C, ¬B}, {¬C, ¬B}} {{B}}
{{C}, {¬C}} ∅
SAT
{∅}
UNSAT
A
B
C
¬A
B
19 / 35
DPLL: Example
{{A, B}, {¬A, B}, {¬A, C, ¬B}, {¬A, ¬C, ¬B}}
{{B}, {C, ¬B}, {¬C, ¬B}} {{B}}
{{C}, {¬C}} ∅
SAT
{∅}
UNSAT
A
B
C
¬A
B
19 / 35
DPLL: Example
{{A, B}, {¬A, B}, {¬A, C, ¬B}, {¬A, ¬C, ¬B}}
{{B}, {C, ¬B}, {¬C, ¬B}} {{B}}
{{C}, {¬C}} ∅
SAT
{∅}
UNSAT
A
B
C
¬A
B
19 / 35
DPLL: Example
{{A, B}, {¬A, B}, {¬A, C, ¬B}, {¬A, ¬C, ¬B}}
{{B}, {C, ¬B}, {¬C, ¬B}} {{B}}
{{C}, {¬C}} ∅
SAT
{∅}
UNSAT
A
B
C
¬A
B
19 / 35
DPLL: Example
{{A, B}, {¬A, B}, {¬A, C, ¬B}, {¬A, ¬C, ¬B}}
{{B}, {C, ¬B}, {¬C, ¬B}} {{B}}
{{C}, {¬C}} ∅
SAT
{∅}
UNSAT
A
B
C
¬A
B
19 / 35
DPLL: Example
{{A, B}, {¬A, B}, {¬A, C, ¬B}, {¬A, ¬C, ¬B}}
{{B}, {C, ¬B}, {¬C, ¬B}} {{B}}
{{C}, {¬C}} ∅
SAT
{∅}
UNSAT
A
B
C
¬A
B
19 / 35
DPLL: Example
{{A, B}, {¬A, B}, {¬A, C, ¬B}, {¬A, ¬C, ¬B}}
{{B}, {C, ¬B}, {¬C, ¬B}} {{B}}
{{C}, {¬C}} ∅
SAT
{∅}
UNSAT
A
B
C
¬A
B
19 / 35
DPLL: Properties
Theorem (Soundness)
If DPLL(Φ) returns SAT, the formula Φ is satisfiable.
Theorem (Completeness)
If the formula Φ is satisfiable, DPLL(Φ) returns SAT.
Corollary (Complexity)
Unless P = NP, the procedure DPLL does not run in polynomial time.
20 / 35
UNSAT DPLL → Resolution
{{A, B}1, {¬B, C}2, {¬B, ¬C}3, {¬A, ¬B, ¬D}4, {¬A, B, ¬D}5, {¬A, B, D}6}
21 / 35
UNSAT DPLL → Resolution
{{A, B}1, {¬B, C}2, {¬B, ¬C}3, {¬A, ¬B, ¬D}4, {¬A, B, ¬D}5, {¬A, B, D}6}
{{¬B, C}2, {¬B, ¬C}3, {¬B, ¬D}4, {B, ¬D}5, {B, D}6} {{B}1, {¬B, C}2, {¬B, ¬C}3}
{{C}2, {¬C}3, {¬D}4} {{¬D}5, {D}6} {{C}2, {¬C}3}
{∅3, {¬D}4} {∅6} {∅3}
A
B
C
¬B
¬D
¬A
B
C
21 / 35
UNSAT DPLL → Resolution
{{A, B}1, {¬B, C}2, {¬B, ¬C}3, {¬A, ¬B, ¬D}4, {¬A, B, ¬D}5, {¬A, B, D}6}
{{¬B, C}2, {¬B, ¬C}3, {¬B, ¬D}4, {B, ¬D}5, {B, D}6} {{B}1, {¬B, C}2, {¬B, ¬C}3}
{{C}2, {¬C}3, {¬D}4} {{¬D}5, {D}6} {{C}2, {¬C}3}
{∅3, {¬D}4} {∅6} {∅3}
{¬B, ¬C}3 {¬A, B, D}6 {¬B, ¬C}3
A
B
C
¬B
¬D
¬A
B
C
21 / 35
UNSAT DPLL → Resolution
{{A, B}1, {¬B, C}2, {¬B, ¬C}3, {¬A, ¬B, ¬D}4, {¬A, B, ¬D}5, {¬A, B, D}6}
{{¬B, C}2, {¬B, ¬C}3, {¬B, ¬D}4, {B, ¬D}5, {B, D}6} {{B}1, {¬B, C}2, {¬B, ¬C}3}
{{C}2, {¬C}3, {¬D}4} {{¬D}5, {D}6} {{C}2, {¬C}3}
{∅3, {¬D}4} {∅6} {∅3}
{¬B, ¬C}3 {¬A, B, D}6 {¬B, ¬C}3{¬B, C}2 {¬A, B, ¬D}5 {¬B, C}2
{A, B}1
A
B
C
¬B
¬D
¬A
B
C
21 / 35
UNSAT DPLL → Resolution
{¬B, ¬C}3 {¬A, B, D}6 {¬B, ¬C}3{¬B, C}2 {¬A, B, ¬D}5 {¬B, C}2
{A, B}1
A
B
C
¬B
¬D
¬A
B
C
21 / 35
UNSAT DPLL → Resolution
{¬B} {¬A, B} {¬B}
{¬B, ¬C}3 {¬A, B, D}6 {¬B, ¬C}3{¬B, C}2 {¬A, B, ¬D}5 {¬B, C}2
{A, B}1
A
B
C
¬B
¬D
¬A
B
C
21 / 35
UNSAT DPLL → Resolution
{¬B} {¬A, B} {¬B}
∅
{¬A} {A}
{¬B} {¬A, B} {¬B}
{¬B, ¬C}3 {¬A, B, D}6 {¬B, ¬C}3{¬B, C}2 {¬A, B, ¬D}5 {¬B, C}2
{A, B}1
A
B
C
¬B
¬D
¬A
B
C
21 / 35
UNSAT DPLL → Resolution
A run of DPLL with result UNSAT corresponds to a tree resolution proof
• replace all derived ∅ leaves by the corresponding original input clauses
• to each unit propagation step, add the original clause of the unit clause that
triggered the unit propagation
• complete the resolution
Corollary (Time Complexity)
DPLL has exponential time complexity (e.g., for PHP formulas).
Theorem (Space Complexity)
DPLL has polynomial space complexity.
22 / 35
DPLL in practice
• DPLL is almost never used in practice
• basis of Conflict-Driven Clause Learning (CDCL) used in most of the modern
SAT solvers
23 / 35
Implementing DPLL
Real implementation of DPLL
• the previous theoretical description is not suitable for practical
implementation
• each modification of formula Φ is too expensive
• do not modify the formula, modify the partial assignment instead
Clause status
• contains satisfied literal → satisfied
• all literals are assigned opposite values → falsified / conflict clause
• one literal is unassigned, other literals are assigned opposite values → unit
clause
• otherwise undetermined
24 / 35
DPLL: Searching in assignments
(A ∨ B) ∧ (¬A ∨ B) ∧ (¬A ∨ C ∨ ¬B) ∧ (¬A ∨ ¬C ∨ ¬B)
[]
[A] [¬A]
[A, B] [¬A, B]
SAT
[A, B, C]
CONFLICT
decide A
propagate B
propagate C
backtrack ¬A
propagate B
25 / 35
DPLL: Searching in assignments
(A ∨ B) ∧ (¬A ∨ B) ∧ (¬A ∨ C ∨ ¬B) ∧ (¬A ∨ ¬C ∨ ¬B)
[]
[A] [¬A]
[A, B] [¬A, B]
SAT
[A, B, C]
CONFLICT
decide A
propagate B
propagate C
backtrack ¬A
propagate B
25 / 35
DPLL: Searching in assignments
(A ∨ B) ∧ (¬A ∨ B) ∧ (¬A ∨ C ∨ ¬B) ∧ (¬A ∨ ¬C ∨ ¬B)
[]
[A] [¬A]
[A, B] [¬A, B]
SAT
[A, B, C]
CONFLICT
decide A
propagate B
propagate C
backtrack ¬A
propagate B
25 / 35
DPLL: Searching in assignments
(A ∨ B) ∧ (¬A ∨ B) ∧ (¬A ∨ C ∨ ¬B) ∧ (¬A ∨ ¬C ∨ ¬B)
[]
[A] [¬A]
[A, B] [¬A, B]
SAT
[A, B, C]
CONFLICT
decide A
propagate B
propagate C
backtrack ¬A
propagate B
25 / 35
DPLL: Searching in assignments
(A ∨ B) ∧ (¬A ∨ B) ∧ (¬A ∨ C ∨ ¬B) ∧ (¬A ∨ ¬C ∨ ¬B)
[]
[A] [¬A]
[A, B] [¬A, B]
SAT
[A, B, C]
CONFLICT
decide A
propagate B
propagate C
backtrack ¬A
propagate B
25 / 35
DPLL: Searching in assignments
(A ∨ B) ∧ (¬A ∨ B) ∧ (¬A ∨ C ∨ ¬B) ∧ (¬A ∨ ¬C ∨ ¬B)
[]
[A] [¬A]
[A, B] [¬A, B]
SAT
[A, B, C]
CONFLICT
decide A
propagate B
propagate C
backtrack ¬A
propagate B
25 / 35
DPLL: Searching in assignments
(A ∨ B) ∧ (¬A ∨ B) ∧ (¬A ∨ C ∨ ¬B) ∧ (¬A ∨ ¬C ∨ ¬B)
[]
[A] [¬A]
[A, B] [¬A, B]
SAT
[A, B, C]
CONFLICT
decide A
propagate B
propagate C
backtrack ¬A
propagate B
25 / 35
DPLL: Searching in assignments
(A ∨ B) ∧ (¬A ∨ B) ∧ (¬A ∨ C ∨ ¬B) ∧ (¬A ∨ ¬C ∨ ¬B)
[]
[A] [¬A]
[A, B] [¬A, B]
SAT
[A, B, C]
CONFLICT
decide A
propagate B
propagate C
backtrack ¬A
propagate B
25 / 35
Partial assignment representation
Trail
• stack of currently assigned literals
• trail = [A, ¬C]
• used during backtracking
Map of values
• maps each variable to true/false/unknown
• value[A] = true, value[B] = unknown, value[C] = false
• used to evaluate clauses
26 / 35
Decision and Backtracking
• do not use recursion for backtracking, manage the stack explicitly (faster and
will be useful later)
• keep list of positions of decision literals that can be reverted if needed
• e.g. for trail = [A, ¬B, C, D, ¬E], decisions = [0, 2]:
– literals trail[0] = A and trail[2] = C were decisions
– other literals were unit propagated or set during backtracking
Desired functionalities
• Decide(x,v): sets x to v; can be flipped using backtracking
• Assign(x,v): sets x to v; cannot be flipped using backtracking
• Backtrack(): undo all assignments up to the last decision, Assign the
decided variable to the opposite value
• How to implement?
27 / 35
Unit propagation
UnitPropagate()
• detects unit clauses
• keeps a queue of unit assignments that have to be performed
• assigns value to all unit literals until fixed point
• can detect conflicts
28 / 35
DPLL: Realistic
1 def DPLL(formula Φ):
2 InitializeDatastructures()
3
4 if UnitPropagation() == CONFLICT:
5 return UNSAT
6
7 while not all variables are assigned:
8 v ← PickUnassignedVariable()
9
10 Decide(v, false)
11 while UnitPropagation() == CONFLICT:
12 if decisions == []:
13 return UNSAT
14 Backtrack()
15
16 return SAT
29 / 35
Unit propagation: naive
Naive unit propagation
• go through the list of clauses
• unit clause → Assign the unassigned literal and repeat
• clause that has all literals assigned to false → return CONFLICT
30 / 35
Unit propagation: naive
Naive unit propagation
• go through the list of clauses
• unit clause → Assign the unassigned literal and repeat
• clause that has all literals assigned to false → return CONFLICT
Less naive unit propagation
• all unit propagations (except the first one) occur after variable
decision/assignment
• precompute for each literal occurs[l], the list of clauses that contain l
• after decision/assignment of l, only check the clauses in occurs[¬l]
30 / 35
Unit propagation: need something better
Still not good enough, a variable can occur in a large number of clauses.
Most of the runtime is spent in unit propagation → must be as cheap as possible!
Idea
Do not check clauses for which we are sure that contain at least two unassigned
literals.
31 / 35
Unit propagation: head-tail lists
Head-tail lists (SATO solver, 1997)
• for each clause, remember positions of its first and last unassigned literals
(head and tail)
• for each literal, remember list of clauses where it is head and where it is tail
• during unit propagation, only check clauses where the negation of literal is
head/tail
• needs to maintain the invariant during backtracking
32 / 35
Unit propagation: head-tail lists
Head-tail lists (SATO solver, 1997)
• for each clause, remember positions of its first and last unassigned literals
(head and tail)
• for each literal, remember list of clauses where it is head and where it is tail
• during unit propagation, only check clauses where the negation of literal is
head/tail
• needs to maintain the invariant during backtracking
x
↑
∨ ¬y ∨ z ∨ ¬v ∨ ¬w ∨
↓
u
Variable assignment:
32 / 35
Unit propagation: head-tail lists
Head-tail lists (SATO solver, 1997)
• for each clause, remember positions of its first and last unassigned literals
(head and tail)
• for each literal, remember list of clauses where it is head and where it is tail
• during unit propagation, only check clauses where the negation of literal is
head/tail
• needs to maintain the invariant during backtracking
x
↑
∨ ¬y ∨ z ∨ ¬v ∨ ¬w ∨
↓
u
Variable assignment:
32 / 35
Unit propagation: head-tail lists
Head-tail lists (SATO solver, 1997)
• for each clause, remember positions of its first and last unassigned literals
(head and tail)
• for each literal, remember list of clauses where it is head and where it is tail
• during unit propagation, only check clauses where the negation of literal is
head/tail
• needs to maintain the invariant during backtracking
x
↑
∨ ¬y ∨ z ∨ ¬v ∨ ¬w ∨
↓
u
Variable assignment: y
32 / 35
Unit propagation: head-tail lists
Head-tail lists (SATO solver, 1997)
• for each clause, remember positions of its first and last unassigned literals
(head and tail)
• for each literal, remember list of clauses where it is head and where it is tail
• during unit propagation, only check clauses where the negation of literal is
head/tail
• needs to maintain the invariant during backtracking
x
↑
∨ ¬y ∨ z ∨ ¬v ∨ ¬w ∨
↓
u
Variable assignment: y
32 / 35
Unit propagation: head-tail lists
Head-tail lists (SATO solver, 1997)
• for each clause, remember positions of its first and last unassigned literals
(head and tail)
• for each literal, remember list of clauses where it is head and where it is tail
• during unit propagation, only check clauses where the negation of literal is
head/tail
• needs to maintain the invariant during backtracking
x
↑
∨ ¬y ∨ z ∨ ¬v ∨ ¬w ∨
↓
u
Variable assignment: y , v
32 / 35
Unit propagation: head-tail lists
Head-tail lists (SATO solver, 1997)
• for each clause, remember positions of its first and last unassigned literals
(head and tail)
• for each literal, remember list of clauses where it is head and where it is tail
• during unit propagation, only check clauses where the negation of literal is
head/tail
• needs to maintain the invariant during backtracking
x
↑
∨ ¬y ∨ z ∨ ¬v ∨ ¬w ∨
↓
u
Variable assignment: y , v
32 / 35
Unit propagation: head-tail lists
Head-tail lists (SATO solver, 1997)
• for each clause, remember positions of its first and last unassigned literals
(head and tail)
• for each literal, remember list of clauses where it is head and where it is tail
• during unit propagation, only check clauses where the negation of literal is
head/tail
• needs to maintain the invariant during backtracking
x
↑
∨ ¬y ∨ z ∨ ¬v ∨ ¬w ∨
↓
u
Variable assignment: y , v , ¬x
32 / 35
Unit propagation: head-tail lists
Head-tail lists (SATO solver, 1997)
• for each clause, remember positions of its first and last unassigned literals
(head and tail)
• for each literal, remember list of clauses where it is head and where it is tail
• during unit propagation, only check clauses where the negation of literal is
head/tail
• needs to maintain the invariant during backtracking
x ∨ ¬y ∨ z
↑
∨ ¬v ∨ ¬w ∨
↓
u
Variable assignment: y , v , ¬x
32 / 35
Unit propagation: head-tail lists
Head-tail lists (SATO solver, 1997)
• for each clause, remember positions of its first and last unassigned literals
(head and tail)
• for each literal, remember list of clauses where it is head and where it is tail
• during unit propagation, only check clauses where the negation of literal is
head/tail
• needs to maintain the invariant during backtracking
x ∨ ¬y ∨ z
↑
∨ ¬v ∨ ¬w ∨
↓
u
Variable assignment: y , v , ¬x , ¬u
32 / 35
Unit propagation: head-tail lists
Head-tail lists (SATO solver, 1997)
• for each clause, remember positions of its first and last unassigned literals
(head and tail)
• for each literal, remember list of clauses where it is head and where it is tail
• during unit propagation, only check clauses where the negation of literal is
head/tail
• needs to maintain the invariant during backtracking
x ∨ ¬y ∨ z
↑
∨ ¬v ∨
↓
¬w ∨ u
Variable assignment: y , v , ¬x , ¬u
32 / 35
Unit propagation: head-tail lists
Head-tail lists (SATO solver, 1997)
• for each clause, remember positions of its first and last unassigned literals
(head and tail)
• for each literal, remember list of clauses where it is head and where it is tail
• during unit propagation, only check clauses where the negation of literal is
head/tail
• needs to maintain the invariant during backtracking
x ∨ ¬y ∨ z
↑
∨ ¬v ∨
↓
¬w ∨ u
Variable assignment: y , v , ¬x , ¬u , w
32 / 35
Unit propagation: head-tail lists
Head-tail lists (SATO solver, 1997)
• for each clause, remember positions of its first and last unassigned literals
(head and tail)
• for each literal, remember list of clauses where it is head and where it is tail
• during unit propagation, only check clauses where the negation of literal is
head/tail
• needs to maintain the invariant during backtracking
x ∨ ¬y ∨ z
↑
∨ ¬v ∨
↓
¬w ∨ u
Variable assignment: y , v , ¬x , ¬u , w
32 / 35
Unit propagation: head-tail lists
Head-tail lists (SATO solver, 1997)
• for each clause, remember positions of its first and last unassigned literals
(head and tail)
• for each literal, remember list of clauses where it is head and where it is tail
• during unit propagation, only check clauses where the negation of literal is
head/tail
• needs to maintain the invariant during backtracking
x ∨ ¬y ∨ z
↑
∨ ¬v ∨
↓
¬w ∨ u
Variable assignment: y , v , ¬x , ¬u , w
Unit: z
32 / 35
Unit propagation: head-tail lists
Head-tail lists (SATO solver, 1997)
• for each clause, remember positions of its first and last unassigned literals
(head and tail)
• for each literal, remember list of clauses where it is head and where it is tail
• during unit propagation, only check clauses where the negation of literal is
head/tail
• needs to maintain the invariant during backtracking
x ∨ ¬y ∨ z
↑
∨ ¬v ∨
↓
¬w ∨ u
Variable assignment: y , v , ¬x , ¬u
32 / 35
Unit propagation: head-tail lists
Head-tail lists (SATO solver, 1997)
• for each clause, remember positions of its first and last unassigned literals
(head and tail)
• for each literal, remember list of clauses where it is head and where it is tail
• during unit propagation, only check clauses where the negation of literal is
head/tail
• needs to maintain the invariant during backtracking
x ∨ ¬y ∨ z
↑
∨ ¬v ∨
↓
¬w ∨ u
Variable assignment: y , v , ¬x , ¬u
32 / 35
Unit propagation: head-tail lists
Head-tail lists (SATO solver, 1997)
• for each clause, remember positions of its first and last unassigned literals
(head and tail)
• for each literal, remember list of clauses where it is head and where it is tail
• during unit propagation, only check clauses where the negation of literal is
head/tail
• needs to maintain the invariant during backtracking
x ∨ ¬y ∨ z
↑
∨ ¬v ∨
↓
¬w ∨ u
Variable assignment: y , v , ¬x
32 / 35
Unit propagation: head-tail lists
Head-tail lists (SATO solver, 1997)
• for each clause, remember positions of its first and last unassigned literals
(head and tail)
• for each literal, remember list of clauses where it is head and where it is tail
• during unit propagation, only check clauses where the negation of literal is
head/tail
• needs to maintain the invariant during backtracking
x ∨ ¬y ∨ z
↑
∨ ¬v ∨ ¬w ∨
↓
u
Variable assignment: y , v , ¬x
32 / 35
Unit propagation: head-tail lists
Head-tail lists (SATO solver, 1997)
• for each clause, remember positions of its first and last unassigned literals
(head and tail)
• for each literal, remember list of clauses where it is head and where it is tail
• during unit propagation, only check clauses where the negation of literal is
head/tail
• needs to maintain the invariant during backtracking
x ∨ ¬y ∨ z
↑
∨ ¬v ∨ ¬w ∨
↓
u
Variable assignment: y , v
32 / 35
Unit propagation: head-tail lists
Head-tail lists (SATO solver, 1997)
• for each clause, remember positions of its first and last unassigned literals
(head and tail)
• for each literal, remember list of clauses where it is head and where it is tail
• during unit propagation, only check clauses where the negation of literal is
head/tail
• needs to maintain the invariant during backtracking
x
↑
∨ ¬y ∨ z ∨ ¬v ∨ ¬w ∨
↓
u
Variable assignment: y , v
32 / 35
Unit propagation: head-tail lists
Head-tail lists (SATO solver, 1997)
• for each clause, remember positions of its first and last unassigned literals
(head and tail)
• for each literal, remember list of clauses where it is head and where it is tail
• during unit propagation, only check clauses where the negation of literal is
head/tail
• needs to maintain the invariant during backtracking
x
↑
∨ ¬y ∨ z ∨ ¬v ∨ ¬w ∨
↓
u
Variable assignment: y
32 / 35
Unit propagation: head-tail lists
Head-tail lists (SATO solver, 1997)
• for each clause, remember positions of its first and last unassigned literals
(head and tail)
• for each literal, remember list of clauses where it is head and where it is tail
• during unit propagation, only check clauses where the negation of literal is
head/tail
• needs to maintain the invariant during backtracking
x
↑
∨ ¬y ∨ z ∨ ¬v ∨ ¬w ∨
↓
u
Variable assignment: y
32 / 35
Unit propagation: head-tail lists
Head-tail lists (SATO solver, 1997)
• for each clause, remember positions of its first and last unassigned literals
(head and tail)
• for each literal, remember list of clauses where it is head and where it is tail
• during unit propagation, only check clauses where the negation of literal is
head/tail
• needs to maintain the invariant during backtracking
x
↑
∨ ¬y ∨ z ∨ ¬v ∨ ¬w ∨
↓
u
Variable assignment:
32 / 35
Unit propagation: head-tail lists
Head-tail lists (SATO solver, 1997)
• for each clause, remember positions of its first and last unassigned literals
(head and tail)
• for each literal, remember list of clauses where it is head and where it is tail
• during unit propagation, only check clauses where the negation of literal is
head/tail
• needs to maintain the invariant during backtracking
x
↑
∨ ¬y ∨ z ∨ ¬v ∨ ¬w ∨
↓
u
Variable assignment:
32 / 35
Unit propagation: head-tail lists
Head-tail lists (SATO solver, 1997)
• for each clause, remember positions of its first and last unassigned literals
(head and tail)
• for each literal, remember list of clauses where it is head and where it is tail
• during unit propagation, only check clauses where the negation of literal is
head/tail
• needs to maintain the invariant during backtracking
x
↑
∨ ¬y ∨ z ∨ ¬v ∨ ¬w ∨
↓
u
Variable assignment:
32 / 35
Unit propagation: two watched literals
Two watched literals (ZCHAFF solver, 2001)
• for each clause, remember positions of its two unassigned literals (watched
literals)
• for each literal, remember list of clauses where it is watched
• during unit propagation, only check clauses where the negation of literal is
watched
• nothing needs to be done during backtracking!
33 / 35
Unit propagation: two watched literals
Two watched literals (ZCHAFF solver, 2001)
• for each clause, remember positions of its two unassigned literals (watched
literals)
• for each literal, remember list of clauses where it is watched
• during unit propagation, only check clauses where the negation of literal is
watched
• nothing needs to be done during backtracking!
x
↑
∨
↓
¬y ∨ z ∨ ¬v ∨ ¬w ∨ u
Variable assignment:
33 / 35
Unit propagation: two watched literals
Two watched literals (ZCHAFF solver, 2001)
• for each clause, remember positions of its two unassigned literals (watched
literals)
• for each literal, remember list of clauses where it is watched
• during unit propagation, only check clauses where the negation of literal is
watched
• nothing needs to be done during backtracking!
x
↑
∨
↓
¬y ∨ z ∨ ¬v ∨ ¬w ∨ u
Variable assignment:
33 / 35
Unit propagation: two watched literals
Two watched literals (ZCHAFF solver, 2001)
• for each clause, remember positions of its two unassigned literals (watched
literals)
• for each literal, remember list of clauses where it is watched
• during unit propagation, only check clauses where the negation of literal is
watched
• nothing needs to be done during backtracking!
x
↑
∨
↓
¬y ∨ z ∨ ¬v ∨ ¬w ∨ u
Variable assignment: y
33 / 35
Unit propagation: two watched literals
Two watched literals (ZCHAFF solver, 2001)
• for each clause, remember positions of its two unassigned literals (watched
literals)
• for each literal, remember list of clauses where it is watched
• during unit propagation, only check clauses where the negation of literal is
watched
• nothing needs to be done during backtracking!
x
↑
∨ ¬y ∨
↓
z ∨ ¬v ∨ ¬w ∨ u
Variable assignment: y
33 / 35
Unit propagation: two watched literals
Two watched literals (ZCHAFF solver, 2001)
• for each clause, remember positions of its two unassigned literals (watched
literals)
• for each literal, remember list of clauses where it is watched
• during unit propagation, only check clauses where the negation of literal is
watched
• nothing needs to be done during backtracking!
x
↑
∨ ¬y ∨
↓
z ∨ ¬v ∨ ¬w ∨ u
Variable assignment: y , v
33 / 35
Unit propagation: two watched literals
Two watched literals (ZCHAFF solver, 2001)
• for each clause, remember positions of its two unassigned literals (watched
literals)
• for each literal, remember list of clauses where it is watched
• during unit propagation, only check clauses where the negation of literal is
watched
• nothing needs to be done during backtracking!
x
↑
∨ ¬y ∨
↓
z ∨ ¬v ∨ ¬w ∨ u
Variable assignment: y , v
33 / 35
Unit propagation: two watched literals
Two watched literals (ZCHAFF solver, 2001)
• for each clause, remember positions of its two unassigned literals (watched
literals)
• for each literal, remember list of clauses where it is watched
• during unit propagation, only check clauses where the negation of literal is
watched
• nothing needs to be done during backtracking!
x
↑
∨ ¬y ∨
↓
z ∨ ¬v ∨ ¬w ∨ u
Variable assignment: y , v , ¬x
33 / 35
Unit propagation: two watched literals
Two watched literals (ZCHAFF solver, 2001)
• for each clause, remember positions of its two unassigned literals (watched
literals)
• for each literal, remember list of clauses where it is watched
• during unit propagation, only check clauses where the negation of literal is
watched
• nothing needs to be done during backtracking!
x ∨ ¬y ∨
↓
z ∨ ¬v ∨ ¬w
↑
∨ u
Variable assignment: y , v , ¬x
33 / 35
Unit propagation: two watched literals
Two watched literals (ZCHAFF solver, 2001)
• for each clause, remember positions of its two unassigned literals (watched
literals)
• for each literal, remember list of clauses where it is watched
• during unit propagation, only check clauses where the negation of literal is
watched
• nothing needs to be done during backtracking!
x ∨ ¬y ∨
↓
z ∨ ¬v ∨ ¬w
↑
∨ u
Variable assignment: y , v , ¬x , ¬u
33 / 35
Unit propagation: two watched literals
Two watched literals (ZCHAFF solver, 2001)
• for each clause, remember positions of its two unassigned literals (watched
literals)
• for each literal, remember list of clauses where it is watched
• during unit propagation, only check clauses where the negation of literal is
watched
• nothing needs to be done during backtracking!
x ∨ ¬y ∨
↓
z ∨ ¬v ∨ ¬w
↑
∨ u
Variable assignment: y , v , ¬x , ¬u
33 / 35
Unit propagation: two watched literals
Two watched literals (ZCHAFF solver, 2001)
• for each clause, remember positions of its two unassigned literals (watched
literals)
• for each literal, remember list of clauses where it is watched
• during unit propagation, only check clauses where the negation of literal is
watched
• nothing needs to be done during backtracking!
x ∨ ¬y ∨
↓
z ∨ ¬v ∨ ¬w
↑
∨ u
Variable assignment: y , v , ¬x , ¬u , w
33 / 35
Unit propagation: two watched literals
Two watched literals (ZCHAFF solver, 2001)
• for each clause, remember positions of its two unassigned literals (watched
literals)
• for each literal, remember list of clauses where it is watched
• during unit propagation, only check clauses where the negation of literal is
watched
• nothing needs to be done during backtracking!
x ∨ ¬y ∨
↓
z ∨ ¬v ∨ ¬w
↑
∨ u
Variable assignment: y , v , ¬x , ¬u , w
33 / 35
Unit propagation: two watched literals
Two watched literals (ZCHAFF solver, 2001)
• for each clause, remember positions of its two unassigned literals (watched
literals)
• for each literal, remember list of clauses where it is watched
• during unit propagation, only check clauses where the negation of literal is
watched
• nothing needs to be done during backtracking!
x ∨ ¬y ∨
↓
z ∨ ¬v ∨ ¬w
↑
∨ u
Variable assignment: y , v , ¬x , ¬u , w
Unit: z
33 / 35
Unit propagation: two watched literals
Two watched literals (ZCHAFF solver, 2001)
• for each clause, remember positions of its two unassigned literals (watched
literals)
• for each literal, remember list of clauses where it is watched
• during unit propagation, only check clauses where the negation of literal is
watched
• nothing needs to be done during backtracking!
x ∨ ¬y ∨
↓
z ∨ ¬v ∨ ¬w
↑
∨ u
Variable assignment: y , v , ¬x , ¬u
33 / 35
Unit propagation: two watched literals
Two watched literals (ZCHAFF solver, 2001)
• for each clause, remember positions of its two unassigned literals (watched
literals)
• for each literal, remember list of clauses where it is watched
• during unit propagation, only check clauses where the negation of literal is
watched
• nothing needs to be done during backtracking!
x ∨ ¬y ∨
↓
z ∨ ¬v ∨ ¬w
↑
∨ u
Variable assignment: y , v , ¬x , ¬u
33 / 35
Unit propagation: two watched literals
Two watched literals (ZCHAFF solver, 2001)
• for each clause, remember positions of its two unassigned literals (watched
literals)
• for each literal, remember list of clauses where it is watched
• during unit propagation, only check clauses where the negation of literal is
watched
• nothing needs to be done during backtracking!
x ∨ ¬y ∨
↓
z ∨ ¬v ∨ ¬w
↑
∨ u
Variable assignment: y , v , ¬x
33 / 35
Unit propagation: two watched literals
Two watched literals (ZCHAFF solver, 2001)
• for each clause, remember positions of its two unassigned literals (watched
literals)
• for each literal, remember list of clauses where it is watched
• during unit propagation, only check clauses where the negation of literal is
watched
• nothing needs to be done during backtracking!
x ∨ ¬y ∨
↓
z ∨ ¬v ∨ ¬w
↑
∨ u
Variable assignment: y , v , ¬x
33 / 35
Unit propagation: two watched literals
Two watched literals (ZCHAFF solver, 2001)
• for each clause, remember positions of its two unassigned literals (watched
literals)
• for each literal, remember list of clauses where it is watched
• during unit propagation, only check clauses where the negation of literal is
watched
• nothing needs to be done during backtracking!
x ∨ ¬y ∨
↓
z ∨ ¬v ∨ ¬w
↑
∨ u
Variable assignment: y , v
33 / 35
Unit propagation: two watched literals
Two watched literals (ZCHAFF solver, 2001)
• for each clause, remember positions of its two unassigned literals (watched
literals)
• for each literal, remember list of clauses where it is watched
• during unit propagation, only check clauses where the negation of literal is
watched
• nothing needs to be done during backtracking!
x ∨ ¬y ∨
↓
z ∨ ¬v ∨ ¬w
↑
∨ u
Variable assignment: y , v
33 / 35
Unit propagation: two watched literals
Two watched literals (ZCHAFF solver, 2001)
• for each clause, remember positions of its two unassigned literals (watched
literals)
• for each literal, remember list of clauses where it is watched
• during unit propagation, only check clauses where the negation of literal is
watched
• nothing needs to be done during backtracking!
x ∨ ¬y ∨
↓
z ∨ ¬v ∨ ¬w
↑
∨ u
Variable assignment: y
33 / 35
Unit propagation: two watched literals
Two watched literals (ZCHAFF solver, 2001)
• for each clause, remember positions of its two unassigned literals (watched
literals)
• for each literal, remember list of clauses where it is watched
• during unit propagation, only check clauses where the negation of literal is
watched
• nothing needs to be done during backtracking!
x ∨ ¬y ∨
↓
z ∨ ¬v ∨ ¬w
↑
∨ u
Variable assignment: y
33 / 35
Unit propagation: two watched literals
Two watched literals (ZCHAFF solver, 2001)
• for each clause, remember positions of its two unassigned literals (watched
literals)
• for each literal, remember list of clauses where it is watched
• during unit propagation, only check clauses where the negation of literal is
watched
• nothing needs to be done during backtracking!
x ∨ ¬y ∨
↓
z ∨ ¬v ∨ ¬w
↑
∨ u
Variable assignment:
33 / 35
Unit propagation: two watched literals
Two watched literals (ZCHAFF solver, 2001)
• for each clause, remember positions of its two unassigned literals (watched
literals)
• for each literal, remember list of clauses where it is watched
• during unit propagation, only check clauses where the negation of literal is
watched
• nothing needs to be done during backtracking!
x ∨ ¬y ∨
↓
z ∨ ¬v ∨ ¬w
↑
∨ u
Variable assignment:
33 / 35
Unit propagation: two watched literals
Two watched literals (ZCHAFF solver, 2001)
• for each clause, remember positions of its two unassigned literals (watched
literals)
• for each literal, remember list of clauses where it is watched
• during unit propagation, only check clauses where the negation of literal is
watched
• nothing needs to be done during backtracking!
x ∨ ¬y ∨
↓
z ∨ ¬v ∨ ¬w
↑
∨ u
Variable assignment:
33 / 35
Next time
Conflict-Driven Clause Learning (CDCL)
• DPLL search (unit propagation, backtracking)
• + using resolution to learn new clauses after conflict
• + non-chronological backtracking
34 / 35
Next time
Conflict-Driven Clause Learning (CDCL)
• DPLL search (unit propagation, backtracking)
• + using resolution to learn new clauses after conflict
• + non-chronological backtracking
Modern SAT Solvers
• CDCL
• + two watched literal scheme
• + variable decision heuristics
• + dynamic restarts
• + preprocessing/inprocessing
34 / 35
Project
You can already start implementing your SAT solver
• input in DIMACS format
• DPLL-like assignment decisions and backtracking
• unit propagation with two watched literal scheme
35 / 35