The Problem
History
DPLL
Resolution
WatchLit
Conclusion
SAT Solvers A Brief Introduction
Marcelo Finger
Department of Computer Science Instituto de Matem atica e Estat stica Universidade de S ao Paulo
Marcelo Finger SAT Solvers
IME-USP
The Problem
History
DPLL
Resolution
WatchLit
Conclusion
Topics
1 2 3 4 5 6
The Problem A Brief History of SAT Solvers The DPLL Algorithm DPLL and Resolution Watched Literals Conclusion
Marcelo Finger SAT Solvers
IME-USP
The Problem
History
DPLL
Resolution
WatchLit
Conclusion
The Problem
The Centrality of SAT
SAT is a central problem in Computer Science, with both theoretical and practical interests
Marcelo Finger SAT Solvers
IME-USP
The Problem
History
DPLL
Resolution
WatchLit
Conclusion
The Problem
The Centrality of SAT
SAT is a central problem in Computer Science, with both theoretical and practical interests SAT was the 1st NP-complete problem
Marcelo Finger SAT Solvers
IME-USP
The Problem
History
DPLL
Resolution
WatchLit
Conclusion
The Problem
The Centrality of SAT
SAT is a central problem in Computer Science, with both theoretical and practical interests SAT was the 1st NP-complete problem SAT received a lot of attention [1960-now]
Marcelo Finger SAT Solvers
IME-USP
The Problem
History
DPLL
Resolution
WatchLit
Conclusion
The Problem
The Centrality of SAT
SAT is a central problem in Computer Science, with both theoretical and practical interests SAT was the 1st NP-complete problem SAT received a lot of attention [1960-now] SAT has very ecient implementations
Marcelo Finger SAT Solvers
IME-USP
The Problem
History
DPLL
Resolution
WatchLit
Conclusion
The Problem
The Centrality of SAT
SAT is a central problem in Computer Science, with both theoretical and practical interests SAT was the 1st NP-complete problem SAT received a lot of attention [1960-now] SAT has very ecient implementations SAT has become the assembly language of hard-problems
Marcelo Finger SAT Solvers
IME-USP
The Problem
History
DPLL
Resolution
WatchLit
Conclusion
The Problem
The Centrality of SAT
SAT is a central problem in Computer Science, with both theoretical and practical interests SAT was the 1st NP-complete problem SAT received a lot of attention [1960-now] SAT has very ecient implementations SAT has become the assembly language of hard-problems SAT is logic
Marcelo Finger SAT Solvers
IME-USP
The Problem
History
DPLL
Resolution
WatchLit
Conclusion
The Setting: the language
Atoms: P = {p1 , . . . , pn } Literals: pi and pj p = p , p = p A clause is a set of literals. Ex: {p , q , r } or p q r A formula C is a set of clauses
Marcelo Finger SAT Solvers
IME-USP
The Problem
History
DPLL
Resolution
WatchLit
Conclusion
The Setting: semantics
Valuation for atoms v : P {0, 1}
Marcelo Finger SAT Solvers
IME-USP
The Problem
History
DPLL
Resolution
WatchLit
Conclusion
The Setting: semantics
Valuation for atoms v : P {0, 1} An atom p is satised if v (p ) = 1
Marcelo Finger SAT Solvers
IME-USP
The Problem
History
DPLL
Resolution
WatchLit
Conclusion
The Setting: semantics
Valuation for atoms v : P {0, 1} An atom p is satised if v (p ) = 1 Valuations are extended to all formulas
Marcelo Finger SAT Solvers
IME-USP
The Problem
History
DPLL
Resolution
WatchLit
Conclusion
The Setting: semantics
Valuation for atoms v : P {0, 1} An atom p is satised if v (p ) = 1 Valuations are extended to all formulas ) = 1 v () = 0 v (
Marcelo Finger SAT Solvers
IME-USP
The Problem
History
DPLL
Resolution
WatchLit
Conclusion
The Setting: semantics
Valuation for atoms v : P {0, 1} An atom p is satised if v (p ) = 1 Valuations are extended to all formulas ) = 1 v () = 0 v ( A clause c is satised (v (c ) = 1) if some literal c is satised
Marcelo Finger SAT Solvers
IME-USP
The Problem
History
DPLL
Resolution
WatchLit
Conclusion
The Setting: semantics
Valuation for atoms v : P {0, 1} An atom p is satised if v (p ) = 1 Valuations are extended to all formulas ) = 1 v () = 0 v ( A clause c is satised (v (c ) = 1) if some literal c is satised A formula C is satised (v (C ) = 1) if all clauses in C are satised
Marcelo Finger SAT Solvers
IME-USP
The Problem
History
DPLL
Resolution
WatchLit
Conclusion
The Problem
A formula C is satisable if exits v , v (C ) = 1. Otherwise, C is unsatisable
Marcelo Finger SAT Solvers
IME-USP
The Problem
History
DPLL
Resolution
WatchLit
Conclusion
The Problem
A formula C is satisable if exits v , v (C ) = 1. Otherwise, C is unsatisable
The SAT Problem
Given a formula C , decide if C is satisable. Witnesses: If C is satisable, provide a v such that v (C ) = 1; otherwise, give a proof that C is unsatisable.
Marcelo Finger SAT Solvers
IME-USP
The Problem
History
DPLL
Resolution
WatchLit
Conclusion
An NP Algorithm for SAT
NP-SAT(C )
Input: C , a formula in clausal form Output: v , if v (C ) = 1; no, otherwise.
1: 2: 3: 4: 5: 6:
Guess a v Show, in polynomial time, that v (C ) = 1 return v if no such v is guessable then return no end if
Marcelo Finger SAT Solvers
IME-USP
The Problem
History
DPLL
Resolution
WatchLit
Conclusion
A Na ve SAT Solver
NaiveSAT(C )
Input: C , a formula in clausal form Output: v , if v (C ) = 1; no, otherwise.
1: 2: 3: 4: 5: 6:
for every valuation v over p1 , . . . , pn do if v (C ) = 1 then return v end if end for return no
Marcelo Finger SAT Solvers
IME-USP
The Problem
History
DPLL
Resolution
WatchLit
Conclusion
A Brief History of SAT Solvers
[Davis & Putnam, 1960; Davis, Longemann & Loveland, 1962] The DPLL Algorithm, a complete SAT Solver
Marcelo Finger SAT Solvers
IME-USP
The Problem
History
DPLL
Resolution
WatchLit
Conclusion
A Brief History of SAT Solvers
[Davis & Putnam, 1960; Davis, Longemann & Loveland, 1962] The DPLL Algorithm, a complete SAT Solver [Tseitin, 1966] DPLL has exponential lower bound
Marcelo Finger SAT Solvers
IME-USP
The Problem
History
DPLL
Resolution
WatchLit
Conclusion
A Brief History of SAT Solvers
[Davis & Putnam, 1960; Davis, Longemann & Loveland, 1962] The DPLL Algorithm, a complete SAT Solver [Tseitin, 1966] DPLL has exponential lower bound [Cook 1971] SAT is NP-complete
Marcelo Finger SAT Solvers
IME-USP
The Problem
History
DPLL
Resolution
WatchLit
Conclusion
Incomplete SAT methods
Incomplete methods compute valuation if C is SAT; if C is unSAT, no answer. [Selman, Levesque & Mitchell, 1992] GSAT, a local search algorithm for SAT
Marcelo Finger SAT Solvers
IME-USP
The Problem
History
DPLL
Resolution
WatchLit
Conclusion
Incomplete SAT methods
Incomplete methods compute valuation if C is SAT; if C is unSAT, no answer. [Selman, Levesque & Mitchell, 1992] GSAT, a local search algorithm for SAT [Mitchell, Levesque & Selman, 1992] Hard and easy SAT problems
Marcelo Finger SAT Solvers
IME-USP
The Problem
History
DPLL
Resolution
WatchLit
Conclusion
Incomplete SAT methods
Incomplete methods compute valuation if C is SAT; if C is unSAT, no answer. [Selman, Levesque & Mitchell, 1992] GSAT, a local search algorithm for SAT [Mitchell, Levesque & Selman, 1992] Hard and easy SAT problems [Kautz & Selman, 1992] SAT planning
Marcelo Finger SAT Solvers
IME-USP
The Problem
History
DPLL
Resolution
WatchLit
Conclusion
Incomplete SAT methods
Incomplete methods compute valuation if C is SAT; if C is unSAT, no answer. [Selman, Levesque & Mitchell, 1992] GSAT, a local search algorithm for SAT [Mitchell, Levesque & Selman, 1992] Hard and easy SAT problems [Kautz & Selman, 1992] SAT planning [Kautz & Selman, 1993] WalkSAT Algorithm
Marcelo Finger SAT Solvers
IME-USP
The Problem
History
DPLL
Resolution
WatchLit
Conclusion
Incomplete SAT methods
Incomplete methods compute valuation if C is SAT; if C is unSAT, no answer. [Selman, Levesque & Mitchell, 1992] GSAT, a local search algorithm for SAT [Mitchell, Levesque & Selman, 1992] Hard and easy SAT problems [Kautz & Selman, 1992] SAT planning [Kautz & Selman, 1993] WalkSAT Algorithm [Gent & Walsh, 1994] SAT phase transition
Marcelo Finger SAT Solvers
IME-USP
The Problem
History
DPLL
Resolution
WatchLit
Conclusion
Incomplete SAT methods
Incomplete methods compute valuation if C is SAT; if C is unSAT, no answer. [Selman, Levesque & Mitchell, 1992] GSAT, a local search algorithm for SAT [Mitchell, Levesque & Selman, 1992] Hard and easy SAT problems [Kautz & Selman, 1992] SAT planning [Kautz & Selman, 1993] WalkSAT Algorithm [Gent & Walsh, 1994] SAT phase transition [Shang & Wah, 1998] Discrete Lagrangian Method (DLM)
Marcelo Finger SAT Solvers
IME-USP
The Problem
History
DPLL
Resolution
WatchLit
Conclusion
DPLL: Second Generation
Second Generation of DPLL SAT Solvers: Posit [1995], SATO [1997], GRASP [1999]. Heuristics but no learning.
Marcelo Finger SAT Solvers
IME-USP
The Problem
History
DPLL
Resolution
WatchLit
Conclusion
DPLL: Second Generation
Second Generation of DPLL SAT Solvers: Posit [1995], SATO [1997], GRASP [1999]. Heuristics but no learning. SAT competitions since 2002: [Link]
Marcelo Finger SAT Solvers
IME-USP
The Problem
History
DPLL
Resolution
WatchLit
Conclusion
DPLL: Second Generation
Second Generation of DPLL SAT Solvers: Posit [1995], SATO [1997], GRASP [1999]. Heuristics but no learning. SAT competitions since 2002: [Link] Aggregation of several techniques to SAT, such as learning, unlearning, backjumping, watched literal, special heuristics.
Marcelo Finger SAT Solvers
IME-USP
The Problem
History
DPLL
Resolution
WatchLit
Conclusion
DPLL: Second Generation
Second Generation of DPLL SAT Solvers: Posit [1995], SATO [1997], GRASP [1999]. Heuristics but no learning. SAT competitions since 2002: [Link] Aggregation of several techniques to SAT, such as learning, unlearning, backjumping, watched literal, special heuristics. Very competitive SAT solvers: Cha [2001], BerkMin [2002],zCha [2004].
Marcelo Finger SAT Solvers
IME-USP
The Problem
History
DPLL
Resolution
WatchLit
Conclusion
DPLL: Second Generation
Second Generation of DPLL SAT Solvers: Posit [1995], SATO [1997], GRASP [1999]. Heuristics but no learning. SAT competitions since 2002: [Link] Aggregation of several techniques to SAT, such as learning, unlearning, backjumping, watched literal, special heuristics. Very competitive SAT solvers: Cha [2001], BerkMin [2002],zCha [2004]. Applications to planning, microprocessor test and verication, software design and verication, AI search, games, etc.
Marcelo Finger SAT Solvers
IME-USP
The Problem
History
DPLL
Resolution
WatchLit
Conclusion
DPLL: Second Generation
Second Generation of DPLL SAT Solvers: Posit [1995], SATO [1997], GRASP [1999]. Heuristics but no learning. SAT competitions since 2002: [Link] Aggregation of several techniques to SAT, such as learning, unlearning, backjumping, watched literal, special heuristics. Very competitive SAT solvers: Cha [2001], BerkMin [2002],zCha [2004]. Applications to planning, microprocessor test and verication, software design and verication, AI search, games, etc. Some non-DPLL SAT solvers incorporate all those techniques: [Dixon 2004]
Marcelo Finger SAT Solvers IME-USP
The Problem
History
DPLL
Resolution
WatchLit
Conclusion
DPLL Through Examples
pq pq p t s p t s p s p s a
Marcelo Finger SAT Solvers
IME-USP
The Problem
History
DPLL
Resolution
WatchLit
Conclusion
Initial Simplifications
does not occur. Delete all clauses that contain , if pq pq p t s p t s p s p s a / /// // /// ///
Marcelo Finger SAT Solvers
IME-USP
The Problem
History
DPLL
Resolution
WatchLit
Conclusion
Construction of a Partial Valuation
Choose a literal: s . V = {s} Propagate choice: Delete clauses containing s . Delete s from other clauses. pq pq p t s / /// // /// /// p t s / /// // /// /// /// p s
Marcelo Finger SAT Solvers
IME-USP
The Problem
History
DPLL
Resolution
WatchLit
Conclusion
Unit Propagation
Enlarge the partial valuation with unit clauses. V = {s, p } Propagate unit clauses as before. p q / /// p q / /// p /
Another propagation step leads to V = {s, p , q , q }
Marcelo Finger SAT Solvers IME-USP
The Problem
History
DPLL
Resolution
WatchLit
Conclusion
Backtracking
Unit propagation may lead to contradictory valuation: } V = {s, p , q , q Backtrack to the previous choice, and propagate: V = { s}
pq pq / // p t s / // p t s p /// // s //
Marcelo Finger SAT Solvers
IME-USP
The Problem
History
DPLL
Resolution
WatchLit
Conclusion
New Choice
When propagation nishes, a new choice is made: p . V = { s , p}. This leads to an inconsistent valuation: V = { s , p, t , t} Backtrack to last choice: V = { s, p } p q / /// p q / /// p t /// /// / p t /// /// /
} Propagation leads to another contradiction: V = { s, p , q , q
Marcelo Finger SAT Solvers IME-USP
The Problem
History
DPLL
Resolution
WatchLit
Conclusion
The Formula is UnSAT
There is nowhere to backtrack to now! The formula is unsatisable, with a proof sketched below.
s p ( p s) q (p q ) q (p q )
s p t ( p t s) p t s) t ( p q (p q ) q (p q )
Marcelo Finger SAT Solvers
IME-USP
The Problem
History
DPLL
Resolution
WatchLit
Conclusion
The Resolution Inference For Clauses
Usual Resolution
D C C D Note that, as clauses are sets
Clauses as Sets
} {} {
} {, } {, {}
Marcelo Finger SAT Solvers
IME-USP
The Problem
History
DPLL
Resolution
WatchLit
Conclusion
DPLL Proofs and Resolution
s p ( p s) q (p q ) q (p q )
s p t ( p t s) p t s) t ( p q (p q ) q (p q )
Marcelo Finger SAT Solvers
IME-USP
The Problem
History
DPLL
Resolution
WatchLit
Conclusion
DPLL Proofs and Resolution
s p ( p s) p pq pq
s p t ( p t s) p t s) t ( p q (p q ) q (p q )
Marcelo Finger SAT Solvers
IME-USP
The Problem
History
DPLL
Resolution
WatchLit
Conclusion
DPLL Proofs and Resolution
s p pq pq p t ( p t s) t ( p t s) p q (p q ) q (p q ) p s s
Marcelo Finger SAT Solvers
IME-USP
The Problem
History
DPLL
Resolution
WatchLit
Conclusion
DPLL Proofs and Resolution
s p pq pq p s p s p t s s p q (p q ) p t s q (p q )
IME-USP
Marcelo Finger SAT Solvers
The Problem
History
DPLL
Resolution
WatchLit
Conclusion
DPLL Proofs and Resolution
s p pq pq p s p s p t s p t s pq s p pq
Marcelo Finger SAT Solvers
IME-USP
The Problem
History
DPLL
Resolution
WatchLit
Conclusion
DPLL Proofs and Resolution
s p pq pq p s p s p t s p t s pq s p pq
Marcelo Finger SAT Solvers
IME-USP
The Problem
History
DPLL
Resolution
WatchLit
Conclusion
Conclusion
DPLL is isomorphic to (a restricted form of) resolution
Marcelo Finger SAT Solvers
IME-USP
The Problem
History
DPLL
Resolution
WatchLit
Conclusion
Conclusion
DPLL is isomorphic to (a restricted form of) resolution DPLL inherits all properties of this (restricted form of resolution
Marcelo Finger SAT Solvers
IME-USP
The Problem
History
DPLL
Resolution
WatchLit
Conclusion
Conclusion
DPLL is isomorphic to (a restricted form of) resolution DPLL inherits all properties of this (restricted form of resolution In particular, DPLL inherits the exponential lower bounds
Marcelo Finger SAT Solvers
IME-USP
The Problem
History
DPLL
Resolution
WatchLit
Conclusion
Enhancing DPLL
For the reasons discussed, DPLL needs to be improved to achieve better eciency. Several techniques have been applied: Learning Unlearning Backjumping Watched literals Heuristics for choosing literals
Marcelo Finger SAT Solvers
IME-USP
The Problem
History
DPLL
Resolution
WatchLit
Conclusion
Enhancing DPLL
For the reasons discussed, DPLL needs to be improved to achieve better eciency. Several techniques have been applied: Learning Unlearning Backjumping Watched literals Heuristics for choosing literals
Marcelo Finger SAT Solvers
IME-USP
The Problem
History
DPLL
Resolution
WatchLit
Conclusion
Watched Literals
Marcelo Finger SAT Solvers
IME-USP
The Problem
History
DPLL
Resolution
WatchLit
Conclusion
The Cost of Unit Propagation
Empirical measures show that 80% of time DPLL is doing Unit Propagation Propagation is the main target for optimization Chaff introduced the technique of Watched Literals
Unit Propagation speed up No need to delete literals or clauses No need to watch all literals in a clause Constant time backtracking (very fast)
Marcelo Finger SAT Solvers
IME-USP
The Problem
History
DPLL
Resolution
WatchLit
Conclusion
DPLL and 3-valued Logic
DPLL underlying logic is 3-valued Given a partial valuation V = {1 , . . . , k } Let be any literal. if V 1(true) 0(false) if V V () = (undened) otherwise
Marcelo Finger SAT Solvers
IME-USP
The Problem
History
DPLL
Resolution
WatchLit
Conclusion
The Watched Literal Data Structure
Every clause c has two selected literals: c 1 , c 2 For each c , c 1 , c 2 are dynamically chosen and varies with time c 1 , c 2 are properly watched under partial valuation V if:
they are both undened; or at least one of them is true
Marcelo Finger SAT Solvers
IME-USP
The Problem
History
DPLL
Resolution
WatchLit
Conclusion
Dynamics of Watched Literals
Initially, V = A pair of watched literals is chosen for each clause. It is proper. Literal choice and unit propagation expand V One or both watched literals may be falsied If c 1 , c 2 become improper then
The falsied watched literal is changed
if no proper pair of watched literals can be found, two things may occur to alter V
Unit propagation (V is expanded) Backtracking (V is reduced)
Marcelo Finger SAT Solvers
IME-USP
The Problem
History
DPLL
Resolution
WatchLit
Conclusion
Example
clause c 1 c 2 pqr p = q = pq s p = q = pr s p= r = Initially V = A pair of literals was elected for each clause All are undened, all pairs are proper
Marcelo Finger SAT Solvers
IME-USP
The Problem
History
DPLL
Resolution
WatchLit
Conclusion
p is chosen
V = {p } All watched literals become (0, ), improper New literals are chosen to be watched clause c 1 c 2 pqr r = q = pq s s = q = p r s s= r =
Marcelo Finger SAT Solvers
IME-USP
The Problem
History
DPLL
Resolution
WatchLit
Conclusion
r is chosen
V = {p , r} WL in clauses 1,3 become improper No other *- or 1-literal to be chosen Unit propagation: q , s become true
clause pqr
c 1 r =0
c 2 /1 q= q = r =0
pq s s = /1 p r s s=
Marcelo Finger SAT Solvers
IME-USP
The Problem
History
DPLL
Resolution
WatchLit
Conclusion
Unit propagation leads to backtracking
V = {p , r, q , s} WL in clause 2 becomes improper No other *- or 1-literal to be chosen No unit propagation is possible: clause 2 is false clause c 1 c 2 pqr r =0 q =1 pq s s =0 q =0 pr s s=1 r =0
Marcelo Finger SAT Solvers
IME-USP
The Problem
History
DPLL
Resolution
WatchLit
Conclusion
Fast Backtracking
V is contracted to last choice point V = // {p , r, q , s} , r } /// /// // /// / {p
clause c 1 c 2 pqr r =1 q = pq s s = q = pr s s= r =1 Only aected WLs had to be recomputed No need to reestablish previous context from a stack of contexts Very quick backtracking
Marcelo Finger SAT Solvers
IME-USP
The Problem
History
DPLL
Resolution
WatchLit
Conclusion
Conclusion of the Talk
DPLL is > 40 years old, but still the most used strategy for SAT solvers
Marcelo Finger SAT Solvers
IME-USP
The Problem
History
DPLL
Resolution
WatchLit
Conclusion
Conclusion of the Talk
DPLL is > 40 years old, but still the most used strategy for SAT solvers Use of smart techniques have improved DPLLs performance: N = 15 N = 10 000
Marcelo Finger SAT Solvers
IME-USP
The Problem
History
DPLL
Resolution
WatchLit
Conclusion
Conclusion of the Talk
DPLL is > 40 years old, but still the most used strategy for SAT solvers Use of smart techniques have improved DPLLs performance: N = 15 N = 10 000 There are still very hard formulas that make DPLL exponential
Marcelo Finger SAT Solvers
IME-USP
The Problem
History
DPLL
Resolution
WatchLit
Conclusion
Conclusion of the Talk
DPLL is > 40 years old, but still the most used strategy for SAT solvers Use of smart techniques have improved DPLLs performance: N = 15 N = 10 000 There are still very hard formulas that make DPLL exponential Experiments show that these formulas do occur in practice
Marcelo Finger SAT Solvers
IME-USP
The Problem
History
DPLL
Resolution
WatchLit
Conclusion
Conclusion of the Talk
DPLL is > 40 years old, but still the most used strategy for SAT solvers Use of smart techniques have improved DPLLs performance: N = 15 N = 10 000 There are still very hard formulas that make DPLL exponential Experiments show that these formulas do occur in practice The future of SAT solvers lies in non-DPLL, non-clausal methods
Marcelo Finger SAT Solvers
IME-USP
The Problem
History
DPLL
Resolution
WatchLit
Conclusion
Conclusion of the Talk
DPLL is > 40 years old, but still the most used strategy for SAT solvers Use of smart techniques have improved DPLLs performance: N = 15 N = 10 000 There are still very hard formulas that make DPLL exponential Experiments show that these formulas do occur in practice The future of SAT solvers lies in non-DPLL, non-clausal methods But the techniques learned from DPLL are incorporated in new techniques
Marcelo Finger SAT Solvers
IME-USP