程序代写代做代考 algorithm AI Unit5 - Introducing SAT Solving

Unit5 – Introducing SAT Solving

Course: C231 Introduction to AI

The SAT Problem

• Informal definition

• The SAT problem

• SAT algorithms

• Applications

Course: C231 Introduction to AI

Why is SAT important?

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?

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)

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

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

Course: C231 Introduction to AI

Notation and Terminology

• 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

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

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

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

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

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

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

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

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

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

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

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

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)

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

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.

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

Related Posts