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