This preview shows page 1-2-16-17-18-33-34 out of 34 pages.

Save
View full document
View full document
Premium Document
Do you want full access? Go Premium and unlock all 34 pages.
Access to all documents
Download any document
Ad free experience
View full document
Premium Document
Do you want full access? Go Premium and unlock all 34 pages.
Access to all documents
Download any document
Ad free experience
View full document
Premium Document
Do you want full access? Go Premium and unlock all 34 pages.
Access to all documents
Download any document
Ad free experience
View full document
Premium Document
Do you want full access? Go Premium and unlock all 34 pages.
Access to all documents
Download any document
Ad free experience
View full document
Premium Document
Do you want full access? Go Premium and unlock all 34 pages.
Access to all documents
Download any document
Ad free experience
View full document
Premium Document
Do you want full access? Go Premium and unlock all 34 pages.
Access to all documents
Download any document
Ad free experience
View full document
Premium Document
Do you want full access? Go Premium and unlock all 34 pages.
Access to all documents
Download any document
Ad free experience
Premium Document
Do you want full access? Go Premium and unlock all 34 pages.
Access to all documents
Download any document
Ad free experience

Unformatted text preview:

Solvers for the Problem of Boolean Satisfiability (SAT)Will Klieber15-414Aug 31, 20112Why study SAT solvers? Many problems reduce to SAT.Formal verificationCAD, VLSIOptimizationAI, 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, andthe 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 -- RepresentationA CNF formula is represented by a set of clauses.Empty set represents a true formula.A clause is represented by a set of literalsEmpty 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 assignmentsExplosion! 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 PropagationDavis-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 ASet 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
Download Lecture
Our administrator received your request to download this document. We will send you the file to your email shortly.
Loading Unlocking...
Login

Join to view Lecture and access 3M+ class-specific study document.

or
We will never post anything without your permission.
Don't have an account?
Sign Up

Join to view Lecture 2 2 and access 3M+ class-specific study document.

or

By creating an account you agree to our Privacy Policy and Terms Of Use

Already a member?