Classical Satisfiability Algorithms
IA085: Satisfiability and Automated Reasoning
Martin Jonáš
FI MUNI, Spring 2025
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
4 / 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
Davis-Putnam algorithm
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
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).
Corollary (Complexity)
The procedure DP does not run in polynomial time.
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
1. replace all derived ∅ leaves by the corresponding original input clauses
2. to each unit propagation step, add the original clause of the unit clause that
triggered the unit propagation
3. 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 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
• for each unit clause Assign the unassigned literal and repeat
• found clause that has all literals assigned to false → return CONFLICT
30 / 35
Unit propagation: naive
Naive unit propagation
• go through the list of clauses
• for each unit clause Assign the unassigned literal and repeat
• found 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