Publish on 13th November 2019
Category: Birds
0

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

SAT and SAT Solvers - lara.epfl.ch