Boolean Satisfiabilityand SAT Solvers
SAV, March 18th, 2015
Boolean Satisfiability
Goal: find a model that satisfies a propositional formula.The original NP-complete problem.“As hard as any other problem in NP.”S. Cook,The complexity of theorem proving procedures, STOC 1971.
a ∧ (¬b ∨ c)
a ∧ b ∧ (¬b ∨ ¬a)
a ↦ T, b ↦ F, c ↦ F
unsatisfiable
SAT in Practice
Ubiquitous in hardware/circuit designE.g. equivalence checking.Search/AI problemsE.g. reduce Sudoku to SAT.Dependency management in Eclipse.Software verificationBy itself, and as part of the SMT stack.
Decidability is Trivial
Fornvariables, enumerate all2npossible assignments.Obviously not very efficient. SAT solving is all about making this enumeration “smart”.
φ≡ a ∧ (¬b ∨ c)
Going to Clauses
SAT solving (almost) always applies to formulasnormalized toconjunctive normal form(CNF).
(a ∨ ¬b ∨ c) ∧ (¬a ∨ c ∨ d ∨ ¬e) ∧ (b ∨ ¬d ∨ e)
{ { a, b̅, c },{ a̅, c, d, e̅ }, { b, d̅, e } }
(a+b̅+c)(a̅ + c + d + e̅)(b + d̅ + e)
Note that a truth table is a kind ofdisjunctivenormal form (DNF).
First Approach: Resolution
Resolution eliminates one variable by producing a new clause (resolvent)from complementary ones.
a ∨ ¬b ∨ f
¬a ∨ ¬c ∨ d ∨ ¬e
¬b ∨ f ∨ ¬c ∨ d ∨ ¬e
Resolution
(a ∨ b) ∧ (a ∨ ¬b) ∧ (¬a ∨ c) ∧ (¬a ∨ ¬c)
a ∧ (¬a ∨ c) ∧ (¬a ∨ ¬c)
c ∧ ¬c
(Part of) Davis Putnam Algorithm
(Also: when a variable appears in only one polarity, remove all clauses containing it.)M. Davis, H. Putnam,A computing procedure for quantification theory, JACM, 1960.Problem: space explosion!DP isproof-oriented. Current algorithms aremodel-oriented.
Backtracking Search
∧(¬a ∨ ¬b ∨ ¬c )∧ ( ¬a ∨¬b ∨¬c )∧ ( ¬a ∨ ¬b∨ ¬c)
a
¬a
¬b
¬c
b
c
!
!
!
Boolean Constraint Propagation
“When all but one literal are falsified, it becomes implied.”
∧(¬a ∨ ¬b ∨ ¬c )∧ ( ¬a ∨¬b ∨¬c )∧ ( ¬a ∨ ¬b∨ ¬c)
a
¬a
¬b
¬c
b
c
Two-watched-literal Scheme for BCP
BCP can cut the search tree dramatically……but checking each clause for potential implications is expensive.Observation: as long as at least two literals in a clause are “not false”, that clause does not imply any new literal.Idea: for each clause, try to maintain that invariant.
Cutting Deeper: Learning
Idea: compute new clauses that are logically implied, and that may trigger more BCP.Use animplication graph. When a conflict is derived, look for asmall explanation.
Learning
∧(a ∨ d)∧ (a ∨ ¬c ∨ ¬h)∧ (a ∨ h ∨ ¬m)∧ (b ∨ k)∧ (¬g ∨ ¬c ∨i)∧ (¬g ∨ h ∨ ¬i)∧ (g ∨ h ∨ ¬j)∧ (g ∨ j ∨ ¬m)
¬a
, d
¬a
d
c
, ¬h
c
¬h
, ¬m
¬m
¬b
¬b
, k
k
g
, ¬i,i
g
i
¬i
¬(c ∧ g ∧ ¬h)
…and backtrack to c, then assert ¬g !
Learning
Learning has a dramatically positive impact.Learning also makesrestartspossible:Idea: after some number of literal assignments, drop the assignment stack and restart from zero.Goal: avoid locally difficultsubtrees.Clauses encode previous knowledge and make new search faster.
Picking Variable Assignments
Potential strategies:Fixed ordering,Frequencybased,“Maximal impact”.Overall favorite are activity-based heuristics:Pick variables that you have seen a lot in conflicts.Decay weights to favor recent conflicts.Cheap to compute/update.
More Engineering…
SAT dirty little secret: the enormous impact of preprocessing.Problems are generated automatically (“compiled”); many redundancies, symmetry, etc.Preprocessors look for subsumed clauses, equivalent clauses, etc.Typically, run with timeout, then DPLL search.Parallel SATState-of-the-art is to run instances with different parameters in parallel.
Scala Implementation
https://github.com/regb/scabolic
CafeSatis a SAT solver written entirely in ScalaIt implements most of the techniquesdescribed in this lectureSome evaluation of the impact of varioustechniques on performance can be found inthe paper:CafeSat: a modern SAT solver for Scala
0
Embed
Upload