Solvers for the Problem of Boolean Satisfiability (SAT)Will Klieber15-414Aug 31, 20112Why study SAT solvers? Many problems reduce to SAT.Formal verificationCAD, VLSIOptimizationAI, planning, automated deduction Modern SAT solvers are often fast. Other solvers (QBF, SMT, etc.) borrow techniques from SAT solvers. SAT solvers and related solvers are still active areas of research.3Negation-Normal Form (NNF) A formula is in negation-normal form iff:all negations are directly in front of variables, andthe only logical connectives are: “∧”, “∨”, “¬”.A literal is a variable or its negation.Convert to NNF by pushing negations inward:¬(P ∧ Q) ⇔ (¬P ∨ ¬Q)¬(P∨Q)⇔(¬P∧¬Q)(De Morgan’s Laws)4Disjunctive Normal Form (DNF)Recall: A literalis a variable or its negation. A formula is in DNF iff:it is a disjunction of conjunctions of literals. Every formula in DNF is also in NNF. A simple (but inefficient) way convert to DNF:Make a truth table for the formula φ.Each row where φis true corresponds to a conjunct.(ℓ11∧ ℓ12∧ ℓ13) conjunction 1∨ (ℓ21∧ ℓ22∧ ℓ23) conjunction 2∨ (ℓ31∧ ℓ32∧ ℓ33) conjunction 35Conjunctive Normal Form (CNF) A formula is in CNF iff:it is a conjunction of disjunctions of literals. Modern SAT solvers use CNF. Any formula can be converted to CNF.Equivalent CNF can be exponentially larger. Equi-satisfiable CNF (Tseitin encoding):Only linearly larger than original formula.(ℓ11∨ ℓ12∨ ℓ13) clause1∧ (ℓ21∨ ℓ22∨ ℓ23) clause2∧ (ℓ31∨ ℓ32∨ ℓ33) clause36Tseitin transformation to CNF Introduce new variables to represent subformulas. E.g, to convert (A ∨ (B ∧ C)):Replace (B ∧ C) with a new variable g1.Add clauses to equate g1with (B ∧ C).Gives value of g1for all 4 possible assignments to {B, C}.Original: ∃x. φ(x)Transformed:∃x.∃g. ψ(x, g)(A ∨ g1) ∧ (B ∨ ¬g1) (¬B→¬g1)∧ (C ∨ ¬g1) (¬C→¬g1)∧ (¬B ∨ ¬C ∨ g1) ((B∧C)→g1)7Tseitin transformation to CNF(A ∨ g1) ∧ (¬g1∨ B) (g1→B)∧ (¬g1∨ C) (g1→C)∧ (¬B ∨ ¬C ∨ g1) ((B∧C)→g1)(g1→(B∧C))∧((B∧C)→g1)(g1⇔(B∧C))Convert (A ∨ (B ∧ C)) to CNF by introducing newvariable g1for (B ∧ C).8SAT Solvers -- RepresentationA CNF formula is represented by a set of clauses.Empty set represents a true formula.A clause is represented by a set of literalsEmpty set represents a false clause.A variable is represented by a positive integer.The logical negation of a variable is represented by the arithmetic negation of its number.E.g., ((x1 ∨ x2) ∧ (¬ x1 ∨ ¬ x2)) is represented by{{1, 2}, {-1, -2}}9Naïve Approach SAT problem: Given a boolean formula φ, does there exist an assignment that satisfies φ? Naïve approach: Search all assignments!nvariables → 2^npossible assignmentsExplosion! SAT is NP-complete: Worst case is likely O(2^n), unless P=NP.But for many cases that arise in practice,we can do much better.10Unit PropagationDavis-Putnam-Logemann-Loveland (DPLL)Unit Clause: Clause with exactly one literal.Algorithm: If a clause has exactly one literal, then assign it true.Repeat until there are no more unit clauses. Example:((x1 ∨ x2) ∧ (¬ x1 ∨ ¬ x2) ∧ (x1))(( T ∨ x2) ∧ ( F ∨ ¬ x2) ∧ (T))(( T ) ∧ ( ¬ x2 ))T11Helper functiondef AssignLit(ClauseList, lit):ClauseList = deepcopy(ClauseList)for clause in copy(ClauseList):if lit in clause: ClauseList.remove(clause)if -lit in clause: clause.remove(-lit)return ClauseList>>> AssignLit([[1, 2, -3], [-1, -2, 4], [3, 4]], 1)[[-2, 4], [3, 4]]>>> AssignLit([[1, 2, -3], [-1, -2, 4], [3, 4]], -1)[[2, -3], [3, 4]]Assumption: No clause contains both a variable and its negation.from copy import copy, deepcopy12Naïve Solverdef AssignLit(ClauseList, lit):ClauseList = deepcopy(ClauseList)for clause in copy(ClauseList):if lit in clause: ClauseList.remove(clause)if -lit in clause: clause.remove(-lit)return ClauseListdef IsSatisfiable(ClauseList):# Test if no unsatisfied clauses remainif len(ClauseList) == 0: return True# Test for presense of empty clauseif [] in ClauseList: return False# Split on an arbitrarily decided literalDecLit = ClauseList[0][0]return (IsSatisfiable(AssignLit(ClauseList, DecLit)) orIsSatisfiable(AssignLit(ClauseList, -DecLit)))13DPLL Solverdef IsSatisfiable(ClauseList):# Unit propagationrepeat until fixed point:for each unit clause UC in ClauseList:ForcedLit = UC[0]ClauseList = AssignLit(ClauseList, ForcedLit)# Test if no unsatisfied clauses remainif len(ClauseList) == 0: return True# Test for presense of empty clauseif [] in ClauseList: return False# Split on an arbitrarily decided literalDecLit = (choose a variable occuring in ClauseList)return (IsSatisfiable(AssignLit(ClauseList, DecLit)) orIsSatisfiable(AssignLit(ClauseList, -DecLit)))unchangedGRASP: an efficient SAT solverOriginal Slides by Pankaj ChauhanModified by Will KlieberPlease interrupt me if anything is not clear!15Terminology CNF formula ϕx1,…, xn: n variablesω1,…, ωm: m clauses Assignment ASet of (variable, value) pairs.Notation: {(x1,1), (x2,0)}, {x1:1, x2:0}, {x1=1, x2=0}, {x1, ¬x2} |A| < n →partial assignment {x1=0, x2=1, x4=1}|A| = n → complete assignment {x1=0, x2=1, x3=0, x4=1}ϕ|A= 0 → falsifying assignment {x1=1, x4=1}ϕ|A= 1 → satisfying assignment {x1=0, x2=1, x4=1}ϕ|A= X → unresolved asgnment {x1=0, x2=0, x4=1}φ = ω1∧ ω2∧ ω3ω1= (x2 ∨ x3) ω2= (¬x1 ∨ ¬x4)ω3= (¬x2 ∨ x4)A = {x1=0, x2=1, x3=0, x4=1}φ = ω1∧ ω2∧ ω3ω1= (x2 ∨ x3) ω2= (¬x1 ∨ ¬x4)ω3= (¬x2 ∨ x4)A = {x1=0, x2=1, x3=0, x4=1}16Terminology An assignment partitions the clause database into three classes:Satisfied, falsified, unresolved Free literal: an unassigned literal Unit clause: has exactly one free literal17Basic Backtracking Search Organize the search in the form of a decision tree.Each node is a decision variable.Outgoing edges: assignment to the decision variable.Depth of node in decision tree is decision level δ(x).“ x=v @ d ” means variable x is assigned value v atdecision level d.x2x2= 0@2x1= 0@1x1x1= 1@1x2x2= 1@218Basic
View Full Document