Unit5 – Introducing SAT Solving
Course: C231 Introduction to AI
The SAT Problem
© Alessandra Russo Unit 5 – The SAT problem, slide 1
• Informal definition
• The SAT problem
• SAT algorithms
• Applications
Course: C231 Introduction to AI
Why is SAT important?
© Alessandra Russo
In theory
Canonical NP-Complete problem
In practice
Applied in many Computer Science problems:
Ø reachability analysis
Ø planning
Ø analysis of gene regulatory network
Ø fault diagnosis
Unit 5 – The SAT problem, slide 2
Course: C231 Introduction to AI
What is the Boolean Satisfiability problem?
© Alessandra Russo
Informally
Given a propositional formula 𝜑, the Boolean satisfiability (SAT)
problem posed on 𝜑 means to determine whether there exists a
variable assignment under which 𝜑 evaluates to true.
Formally
Let X be a set of propositional variables. Let F be a set of clauses
over X.
Ø F is Satisfiable iff there exists a v: X →{0,1} s.t. v ⊨ F
Ø F is Unsatisfiable iff v ⊭ F, for all v: X →{0,1}
Example
C1 = {¬x1∨x2, ¬x2∨x3} = (¬x1∨x2) ∧ (¬x2∨x3) Sat(C1) = Yes
C2 = C1 ∪{x1, ¬x3} = (x3∧¬x3) Sat(C2) = No
x1 = 0, x3 = 1,
Unit 5 – The SAT problem, slide 3
Course: C231 Introduction to AI
Why in CNF?
• There are efficient algorithms that can
transform formulae into CNF.
• Most SAT solvers can exploit CNF
– Easy to detect a conflict
– Easy to remember partial assignments that
don’t work (just add ‘conflict’ clauses)
© Alessandra Russo Unit 5 – The SAT problem, slide 4
Course: C231 Introduction to AI
It’s a hard problem..!
A k-SAT problem with input in CNF with at
most k literals in each clause…
• Complexity for different values of k:
– 2-SAT: in P
– 3-SAT: in NP-complete
– > 3-SAT: is also NP-complete
© Alessandra Russo Unit 5 – The SAT problem, slide 5
Course: C231 Introduction to AI
A classification of SAT algorithms
• Complete algorithms
– Proof systems – natural deduction, tableau, etc..
– Davis-Putman (DP)
• based on resolution
– Stalmarck’s method
– Davis-Logemann-Loveland (DLL/DPLL)
• search-based, basis for most successful solvers
– Conflict-Driven Clause Learning (CDCL)
• Incomplete algorithms
• Local search /hill climbing
• Genetic algorithms
© Alessandra Russo Unit 5 – The SAT problem, slide 6
Course: C231 Introduction to AI
Notation and Terminology
© Alessandra Russo
• Polarity of a variable in a clause
The “sign” with which the variable appears in the clause:
x1∨¬x2 x1 positive polarity, x2 negative polarity
• Resolution:
Two clauses C1 and C2 that contain a variable x with
opposite polarities, implies a new clause C3 that contains all
literals except x and ¬x.
{x1,¬x2} {x2,¬x3} {x1,¬x3}
16-
Feb
–
5
4
40
2
Clea
ner
• Clause shorthand notations
Let C = x1∨ x2∨¬x3∨¬x4 , we can write it
x1x2¬x3¬x4 or as x1+x2+¬x3+¬x4 or as {x1,x2,¬x3,¬x4}
Unit 5 – The SAT problem, slide 7
Course: C231 Introduction to AI
© Alessandra Russo
Davis-Putman (DP) Algorithm
Give a set S of clauses
For every variable in S
1. for every clause Ci containing the variable
and every clause Cj containing the negation of
the variable resolve Ci and Cj
2. add the resolvent to the set S of clauses
3. remove from S all original clauses containing
the variable or its negation.
Two possible termination cases:
o Derive the empty clause (conclude UNSAT)
o All variables have been selected
Unit 5 – The SAT problem, slide 8
Course: C231 Introduction to AI
© Alessandra Russo
Davis-Putman (DP): Example
Let S = {{p, q} {p, ¬q} {¬p, q} {¬p, ¬q} } choose p
S’ = {{p, q} {p, ¬q} {¬p, q} {¬p, ¬q} {q} {q, ¬q} {¬q} }
S’ = { {q} {q, ¬q} {¬q} } choose q
S’’ = { {q} {q, ¬q} {¬q} {q} {¬q} {}}
S’’ = { {}} EMPTY CLAUSE: UNSAT
What about tautologies?
Unit 5 – The SAT problem, slide 9
Course: C231 Introduction to AI
© Alessandra Russo
Davis-Putman (DP): Example 1
Let S = {{p, q} {p, ¬q} {¬p, q} {¬p, ¬q} } choose p
S’ = {{p, q} {p, ¬q} {¬p, q} {¬p, ¬q} {q} {q, ¬q} {¬q} }
S’ = { {q} {q, ¬q} {¬q} }
S’’ = { {q} {q, ¬q} {¬q} {q} {¬q} {}}
S’’ = { {}}
What about tautologies?
choose q
S’’ = { {}} EMPTY CLAUSE: UNSAT
S’’ = { {q} {¬q} }
Eliminate tautologies first
Unit 5 – The SAT problem, slide 10
Course: C231 Introduction to AI
© Alessandra Russo
Davis-Putman (DP): Example I1
Let S = { {p,¬q} {q}} choose q
S’ = {{p, ¬q} {q} {p}}
S’ = {{p}} No further variable can be chosen
Satisfiable and any assignment MUST make p true
BUT
• p appears only positively in the given set S of clauses.
• we could remove the clause that includes p from the beginning
and “remember” that p has to be true.
S = { {p,¬q} {q}} [p]
S = {{q}}
S = { }
[p, q]
[p, q]
Unit 5 – The SAT problem, slide 11
Course: C231 Introduction to AI
Basic Rules
© Alessandra Russo
Pure Literal rule
• Given a CNF formula F, expressed as a set S of clauses, a
literal is pure in F if it only occurs only as a positive or as a
negative literal in S.
S = {{¬x1, x2} {x3,¬x2}{x4,¬x5}{x5,¬x4}}
¬x1 and x3 are pure literals
• Clauses containing pure literals can be removed from the
formula (i.e. assign pure literals to the values that satisfy the clauses)
S= {{¬x1, x2} {x3,¬x2}{x4,¬x5}{x5,¬x4}}
S’ = {{x4,¬x5}{x5,¬x4}}
Assignment must make x1 = false and x3 = true
Remember [¬x1, x3]
Unit 5 – The SAT problem, slide 12
Course: C231 Introduction to AI
Basic Rules
© Alessandra Russo
Unit clause
S = { {x1, x2} {¬x1 x3} {¬x3 x4} {x1}}
Clause with a single literal. It is satisfied by assuming the literal to be true.
• Every clause (other than the unit clause itself), that contains the unit
clause, is removed
• In every clause that contains the negation of the unit clause, this
negated literal is deleted
unchangedunchanged¬x1 deletedremoved
S’ = { {x3} {¬x3 x4} {x1}}
Unit propagation rule
Once a literal has been assigned, its assignment needs to be propagated to
other clauses:
Using a partial assignment: a clause can be unit clause when all
literal except one are assigned based on a given partial assignment.
X1 become then pure literal
Unit 5 – The SAT problem, slide 13
Course: C231 Introduction to AI
Improved Davis-Putman (DP) Algorithm
© Alessandra Russo
M is a partial model of clauses processed so farDP(M, S):
S is set of clauses still to process
Iteratively apply the following steps:
Ø Select a variable x
Ø Apply resolution rule between every pair of clauses of the form
(x∨α) and (¬x∨β) in S
Ø Remove all clauses containing either x or ¬x
Ø Apply the pure literal rule and unit propagation
Terminate when either the empty clause or empty formula
(equivalently, a formula containing only pure literals) is derived
DP([], S) (At the beginning)
Unit 5 – The SAT problem, slide 14
Course: C231 Introduction to AI
© Alessandra Russo
Davis-Putman (DP) Algorithm II: example
S ={{x1, ¬x2, ¬x3}{¬ x1, ¬x2, ¬x3}{x2, x3}{x3, x4}{x3, ¬x4}}
M = {}
S1 ={{¬x2, ¬x3}{x2, x3}{x3, x4}{x3, ¬x4}}
S2 ={{¬x3, x3}{x3, x4}{x3, ¬x4}} tautology
S3 ={{x3, x4}{x3, ¬x4}} x3 pure literal
S4 ={} M = {x3}
Satisfiable provided that x3 is true.
Unit 5 – The SAT problem, slide 15
Course: C231 Introduction to AI
© Alessandra Russo
Improved Davis-Putman (DP) Algorithm
Key ideas:
Ø Resolution eliminates 1 variable at each step
Ø Use of pure literal rule and unit propagation
But still inefficient…..
Unit 5 – The SAT problem, slide 16
Course: C231 Introduction to AI
© Alessandra Russo
DLL (or DPLL) Algorithm
Basic idea:
Ø Instead of eliminating variables,
split on a given variable at each step
Ø Also apply the pure literal rule and unit
propagation
Unit 5 – The SAT problem, slide 17
Course: C231 Introduction to AI
Basic Rules and Notations for DLL
© Alessandra Russo
UNSAT(Sc) If Sc contains the {}, then F is unsatisfiable
SAT(Sc) If Sc = {} then F is satisfiable
MULT(L, Sc) If a literal occurs more than once in a clause in Sc, then all
but one can be deleted
SUB(C, Sc) A clause C in Sc can be deleted, if it is a superset of
another clause in Sc
TAUT(C, Sc) Delete from Sc any clause that contains a literal L and its
negation ¬L
PURE(L, Sc) If L is a pure literal in Sc, delete all clauses that contain L,
and add L to M (i.e. M = M∪{L}).
Let F be the initial set of clauses and let M = {} be initial assignment.
Let Sc be the current set of clauses:
Unit 5 – The SAT problem, slide 18
Course: C231 Introduction to AI
Basic Rules and Notations for DLL
© Alessandra Russo
UNIT(L, Sc) If Sc contain unit clause {L}, then delete all clauses in Sc that
include L, remove the element ¬L from the remaining clauses,
and add L to M (i.e. M = M∪{L}).
SPLIT(L,Sc) If Sc contains two clauses of the form
{….{Ck,L}..{Cm, ¬L}…}, branch the computation.
• One branch has M = M∪{L} and Sc is generated as in
UNIT rule assuming L to be the fact.
• Other branch has M = M∪{¬L} and Sc is generated as in
UNIT rule assuming ¬L to be the fact.
Let F be the initial set of clauses and let M = {} be initial assignment.
Let Sc be the current set of clauses:
Unit 5 – The SAT problem, slide 19
Course: C231 Introduction to AI
DLL Procedure (pseudo code)
© Alessandra Russo
DLL(M, S): boolean;
%M is a (partial) model so far and S are clauses still to process
1. If SAT(S) return true; %M is a (partial) model
2. If UNSAT(S) return false; % S has no models
3. If SUB(C, S) return DLL(M, S \ C);
4. If PURE(L, S) return DLL([L | M], S’), S’ = S \ { Ci | L in Ci}; %Make L true
5. If UNIT(L, S) return DLL([L | M], S’), S’ generated from S by removing
clauses containing L, and removing
¬L from rest.
6. If UNIT(¬L, S) return DLL([¬L | M], S’), S’ generated from S by removing
clauses containing ¬L, and
removing L from rest.
7. Otherwise, SPLIT(L, S) return DLL([L | M ], S’) ∨ DLL( [¬L | M], S”),
S’ formed as in Step 5 , and S” formed as in Step 6.
Unit 5 – The SAT problem, slide 20
Course: C231 Introduction to AI
DLL Example
© Alessandra Russo
S = {{x1,x2} {x4,¬x2, ¬x3} {¬x1, x3} {¬x4} } M = {}
S1 = {{x1,x2} {¬x2, ¬x3} {¬x1, x3}}
UNIT(¬x4, S) M = {¬x4}
S1 = {{¬x2, ¬x3} {x3}} S1 = {{x2} {¬x2, ¬x3}}
SPLIT(x1, S1)
M = {x1,¬x4}
SPLIT(¬x1, S1)
M = {¬x1,¬x4}
S2 = {{¬x2}} S2 = {{¬x3}}
UNIT(x3, S1)
M = {x3, x1,¬x4}
UNIT(x2, S1)
M = {x2, ¬x1,¬x4}
PURE(¬x2, S2)
M = {¬x2,x3, x1,¬x4}
S3 = { } S3 = { }
PURE(¬x3, S2)
M = {¬x3,x2,¬x1,¬x4}
Satisfiable Satisfiable
Unit 5 – The SAT problem, slide 21
Course: C231 Introduction to AI
Properties of DLL
• MULT, SUB, TAUT, UNIT rules are equivalence
preserving
S’ ≡ S
• PURE and SPLIT are unsatisfiability preserving.
– PURE: S is unsatisfiable ≡ S’ is unsatisfiable
– SPLIT: S is unsatisfiable ≡ S’ is unsatisfiable and
S” is unsatisfiable.
• Theorem
o DLL(M, S) halts with False if S has no models.
o DLL(M, S) halts with True and returns at least one
(partial) model of S if S is satisfiable.
© Alessandra Russo Unit 5 – The SAT problem, slide 22
Course: C231 Introduction to AI
Summary
Ø Introduced the notion of satisfiability (SAT)
Ø Described simple DP algorithm, based on resolutions
Ø Introduced simple simplification rules
o TAUT, SUB, PURE literals
Ø Unit propagation and SPLIT rules
Ø DLL/DPLL algorithm
© Alessandra Russo Unit 5 – The SAT problem, slide 23