Transcript one - CSE

Propositional Satisfiability
(SAT)
Toby Walsh
Cork Constraint Computation Centre
University College Cork
Ireland
4c.ucc.ie/~tw/sat/
Every morning …
I cycle across the River
Lee in Cork …
And see this rather drab
house …
Every morning …
I read the plaque on the wall
of this house …
Dedicated to the memory of
George Boole …
Professor of Mathematics at
Queens College (now
University College Cork)
George Boole (1815-1864)

Boolean algebra
The Mathematical Analysis
of Logic, Cambridge,
1847
The Calculus of Logic,
Cambridge and Dublin
Mathematical journal, vol.
3, 1848

Reduced propositional
logic to algebraic
manipulations
George Boole (1815-1864)

Boolean algebra
The Mathematical Analysis
of Logic, Cambridge,
1847
The Calculus of Logic,
Cambridge and Dublin
Mathematical journal, vol.
3, 1848

Reduced propositional
logic to algebraic
manipulations
Outline

What is SAT?

How do we solve
SAT?

Why is SAT
important?
Propositional logic

Long history




Aristotle
Leibnitz
Boole
Foundation for formalizing deductive
reasoning

Used extensively to automate such reasoning
in Artificial Intelligence
A diplomatic problem

As chief of staff, you are to sent out invitations to
the embassy ball.
The ambassador instructs you to invite Peru or
exclude Qatar.
 The vice-ambassador wants you to invite Qatar or
Romania or both.
 A recent diplomatic incidents means that you cannot
invite both Romania and Peru
Who do you invite?

A diplomatic problem

As chief of staff, you are to
sent out invitations to the
embassy ball.
The ambassador instructs
you to invite Peru or
exclude Qatar.
 The vice-ambassador wants
you to invite Qatar or
Romania or both.
 A recent diplomatic
incidents means that you
cannot invite both Romania
and Peru
Who do you invite?


P v -Q

QvR

-(R & P)
A diplomatic problem

As chief of staff, you are to
sent out invitations to the
embassy ball.
The ambassador instructs
you to invite Peru or
exclude Qatar.
 The vice-ambassador wants
you to invite Qatar or
Romania or both.
 A recent diplomatic
incidents means that you
cannot invite both Romania
and Peru
Who do you invite?


P v -Q

QvR

-(R & P)
P,Q,-R or -P,-Q,R
Propositional satisfiability
(SAT)

Given a propositional
formula, does it have
a “model” (satisfying
assignment)?


1st decision problem
shown to be NPcomplete
Usually focus on
formulae in clausal
normal form (CNF)
Clausal Normal Form

Formula is a conjunction of
clauses


Each clause is a disjunction
of literals




C1 & C2 & …
L1 v L2 v L3, …
Empty clause contains no
literals (=False)
Unit clauses contains single
literal
Each literal is variable or its
negation

P, -P, Q, -Q, …
Clausal Normal Form

k-CNF


3-CNF



Each clause has k
literals
NP-complete
Best current complete
methods are exponential
2-CNF

Polynomial (indeed,
linear time)
Converting to CNF

Eliminate iff and implies



P iff Q => P implies Q, Q implies P
P implies Q => -P v Q
Push negation down


-(P & Q) => -P v -Q
-(P v Q) => -P & -Q
Converting to CNF

Clausify using De Morgan’s laws


E.g. P v (Q & R) => (P v Q) & (P v R)
In worst case, formula may grow
exponentially in size

Can introduce new literals to prevent this
blow up
How do we solve SAT?

Systematic methods



Local search methods




Truth tables
Davis Putnam procedure
GSAT
WalkSAT
Tabu search, SA, …
Exotic methods

DNA, quantum computing,
Truth tables

Enumerate all possible truth assignments
P Q R C1=P v Q C2=-Q v -R
T T T
T
F
T T F
T
T
T F T
T
T
T F F
…
C1&C2
F
T
T
Davis Putnam procedure

Introduced by Davis & Putnam in 1960


Resolution rule required exponential space
Modified by Davis, Logemann and Loveland in
1962



Resolution rule replaced by splitting rule
Trades space for time
Modified algorithm usually inaccurately called Davis
Putnam procedure
Davis Putnam procedure

Consider
(X or Y) & (-X or Z) & (-Y or Z) & …

Basic idea

Try X=true
Davis Putnam procedure

Consider
(X or Y) & (-X or Z) & (-Y or Z) & …

Basic idea


Try X=true
Remove clauses which must be satisfied
Davis Putnam procedure

Consider
(-X or Z) & (-Y or Z) & …

Basic idea



Try X=true
Remove clauses which must be satisfied
Simplify clauses containing -X
Davis Putnam procedure

Consider
(

Z) & (-Y or Z) & …
Basic idea




Try X=true
Remove clauses which must be satisfied
Simplify clauses containing -X
Can now deduce that Z must be true
Davis Putnam procedure

Consider
(

Z) & (-Y or Z) & …
Basic idea





Try X=true
Remove clauses which must be satisfied
Simplify clauses containing -X
Can now deduce that Z must be true
At any point, may have to backtrack and try X=false
instead
Procedure DPLL(C)
(SAT)
if C={} then SAT
(Empty) if empty clause in C then UNSAT
(Unit)
if unit clause, {l} then
DPLL(C[l/True])
(Split)
if DPLL(C[l/True]) then SAT else
DPLL(C[l/False])
Procedure DPLL(C)
(Pure)
(Taut)
if l is pure in C then
DPLL(C[l/True])
if l v -l in C then
DPLL(C - {l v -l})
Neither rules are needed for completeness
and do not tend to improve solving
efficiency
Procedure DPLL(C)
(SAT)
if C={} then SAT
(Empty) if empty clause in C then UNSAT
(Unit)
if unit clause, {l} then
DPLL(C[l/True])
(Split)
if DPLL(C[l/True]) then SAT else
DPLL(C[l/False])
Unit rule not needed for completeness but
improves efficiency greatly
Procedure DPLL(C)
Non-deterministic
Which literal do we branch upon?
Good choice can reduce solving time
significantly
Popular heuristics include:
MOM’s (most occurrences in minimal size
clauses)
Literal that gives “most” unit propagation
Procedure DPLL(C)
Other refinements
Non-chronological backtracking (conflict
directed backjumping, …)
Clause learning (at end of branch, identify cause
for failure and add this as an additional clause)
Fast data structures (two literal watching for fast
unit propagation)
Procedure DPLL(C)
Space complexity
O(n)
Time complexity
O(1.618^n)
Average and best case often much better than this
worst case (see next lecture)
Brief History of DP

1st generation (1960s)


2nd generation (1980s/90s)



SATO, satz, grasp, …
4th generation (2000s)

Actual Japanese 5th Generation Computer
(from FGC Museum archive)
POSIT, Tableau, …
3rd generation (mid 1990s)


DP, DLL
Chaff, BerkMin, …
5th generation?
Brief History of DP

1st generation (1960s)


2nd generation (1980s/90s)



SATO, satz, grasp, …
4th generation (2000s)

Actual Japanese 5th Generation Computer
(from FGC Museum archive)
POSIT, Tableau, …
3rd generation (mid 1990s)


DP, DLL
Chaff, BerkMin, …
5th generation?

Will it need a paradigm shift?
Moore’s Law

'0
0
Number
of vars
'9
6
'9
2
500
400
300
200
100
0
Are we keeping up with Moore’s law?
 Number of transistors doubles every 18 months
 Number of variables reported in random 3SAT experiments
doubles every 3 or 4 years
 We’re falling behind each year!
 Even though we’re getting better performance due to
Moore’s law!
Local search for SAT

Repair based methods


Instead of building up a solution, take
complete assignment and flip variable to
satisfy “more” clauses
Cannot prove UNSATisfiability

Often will solve MAX-SAT problem
Papadimitrou’s procedure


T:= random truth assignment
Repeat until T satisfies all clauses


v := variable in UNSAT clause
T := T with v’s value flipped
Semi-decision procedure
Solves 2-SAT in expected O(n^2) time
GSAT

[Selman, Levesque, Mitchell AAAI 92]
Repeat MAX-TRIES times or until clauses
satisfied


T:= random truth assignment
Repeat MAX-FLIPS times or until clauses satisfied


v := variable which flipping maximizes number of SAT
clauses
T := T with v’s value flipped
Adds restarts and greediness
Sideways flips important (large plateaus to
explore)
WalkSAT

[Selman, Kautz, Cohen AAAI 94]
Repeat MAX-TRIES times or until clauses
satisfied


T:= random truth assignment
Repeat MAX-FLIPS times or until clauses satisfied



c := unsat clause chosen at random
v:= var in c chosen either greedily or at random
T := T with v’s value flipped
Focuses on UNSAT clauses
Novelty

[McAllester, Selman, Kautz AAAI 97]
Repeat MAX-TRIES times or until clauses satisfied


T:= random truth assignment
Repeat MAX-FLIPS times or until clauses satisfied



c := unsat clause chosen at random
v:= var in c chosen greedily
If v was last var in clause flipped and rand(1)<p then
v:= var in c with 2nd highest score

T := T with v’s value flipped
Encourages diversity (like Tabu search)
Other local search methods




Simulated annealing
Tabu search
Genetic algorithms
Hybrid methods

Combine best features of systematic
methods (eg unit propagation) and local
search (eg quick recovery from failure)
Exotic methods




Quantum computing
DNA computing
Ant computing
…
Beyond the propositional





Linear 0/1 inequalities
Quantified Boolean satisfiability
Stochastic satisfiability
Modal satisfiability
…
Linear 0/1 inequalities

Constraints of the form:


Sum ai . Xi >= c
SAT can easily be expressed as linear
0/1 problem


X v -Y v Z => X + (1-Y) + Z >= 1
…
Linear 0/1 inequalities

Often good for describing problems
involving arithmetic



Counting constraints
Objective functions
Solution methods


Complete Davis-Putnam like methods
Local search methods like WalkSAT(PB)
Quantified Boolean formulae

Propositional SAT can be expressed as:


Can add universal quantifiers:


Exists P, Q, R . (P v Q) & (-Q v R) & …
Forall P . Exists Q, R . (P v Q) & (-Q v R) & ..
Useful in formal methods, conditional
planning …
Quantified Boolean formulae


SAT of QBF is PSPACE complete
Can be seen as game



Existential quantifiers trying to make it SAT
Universal quantifiers trying to make it UNSAT
Solution methods


Extensions of the DPLL procedure
Local search methods just starting to appear
Stochastic satisfiability

Randomized quantifier in addition to the
existential




With prob p, Q is True
With prob (1-p), Q is False
Can we satisfy formula in some fraction of possible
worlds?
Useful for modelling uncertainty present in real
world (eg planning under uncertainty)
Conclusions


Defined propositional SAT
Complete methods


Local search procedures


Davis Putnam, DPLL, …
GSAT, WalkSAT, Novelty, …
Extensions