SAT: Propositional Satisfiability

A tutorial

What is SAT?
Given a propositional formula in CNF, find an assignment to
:Boolean variables that makes the formula true

11==(x
(x22xx33))
22==((xx11xx44))
33==((xx22xx44))
AA=={x
{x11=0,
=0,xx22=1,
=1,xx33=0,
=0,xx44=1}
=1}

SATisfying
assignment!

?Why SAT
Fundamental problem from theoretical point of
view
Cook theorem, 1971: the first NP-complete problem.

Numerous applications:

Solving any NP problem...

Verification: Model Checking, theorem-proving, ...
AI: Planning, automated deduction, ...
Design and analysis: CAD, VLSI
Physics: statistical mechanics (models for spin-glass
material)

SAT made some progress

CNF-SAT

Conjunctive Normal Form: Conjunction of

disjunction of literals. Example:
(:x1 :x2) (x2 x4 : x1) ...

Experience shows that CNF-SAT solving is faster

than solving a general propositional formula.

There exists a polynomial transformation of a

general propositional formula to CNF, with
addition of || variables.

(CNF) SAT basic definitions: literals

A literal is a variable or its negation.

Var(l) is the variable associated with a literal l.
A literal is called negative if it is a negated
variable, and positive otherwise.

SAT basic definitions: literals

If var(l) is unassigned, then l is unresolved.

Otherwise, l is satisfied by an assignment if
(var(l)) = 1 and l is positive, or
(var(l)) = 0 and l is negative,
and unsatisfied otherwise.

SAT basic definitions: clauses

The state of an n-literal clause C under

a partial assignment is:

Satisfied if at least one of Cs literals is

satisfied,
Conflicting if all of Cs literals are
unsatisfied,
Unit if n-1 literals in C are unsatisfied and 1
literal is unresolved, and
Unresolved otherwise.

SAT basic definitions: clauses

Example

SAT basic definitions: the unit clause

rule

The unit clause rule: in a unit clause the

unresolved literal must be satisfied.

A Basic SAT algorithm

Given

in CNF: (x,y,z),(-x,y),(-y,z),(-x,-y,-z)

-x

(y ),(-y ,z ),(-y ,-z )

y

-y

(z ),(-z )
z

-z
()

()

()

Decide()

(y ,z ),(-y ,z )
z

-z
()

(y ),(-y )
-y

y
()

()

Deduce()
Resolve_Conflict()

Basic Backtracking Search

Organize the search in the form of a
decision tree

Each node corresponds to a decision

Depth of the node in the decision tree is

called the decision level

Notation: x=v@d
x is assigned v 2 {0,1} at decision level d

Backtracking Search in Action

x1
x1 = 0@1

x2 = 0@2

x2

x3 = 1@2
{(x1,0), (x2,0), (x3,1)}

11==(x
(x22xx33))
22==((xx11xx44))
33==((xx22xx44))
x1 = 1@1 x4 = 0@1 x2 = 0@1

x3 = 1@1
{(x1,1), (x2,0), (x3,1) , (x4,0)}

No backtrack in this
example, regardless of

Backtracking Search in Action

x1
x1 = 1@1
x4 = 0@1

x2 = 0@1
x3 = 1@1

conflict

Add a
clause
x1 = 0@1

x2

11==(x
(x22xx33))
22==((xx11xx44))
33==((xx22xx44))
44==((xx11xx22xx33))
x2 = 0@2 x3 = 1@2

{(x1,0), (x2,0), (x3,1)}

A Basic SAT algorithm (DPLLbased)

Choose the next
variable and value.
Return False if all
variables are assigned

While (true)
{

if (!Decide()) return (SAT);

while (!Deduce())
}

if (!Resolve_Conflict()) return (UNSAT);

Apply unit clause rule.

Return False if reached
a conflict

Backtrack until
no conflict.
Return False if impossible

Decision heuristics
DLIS (Dynamic Largest Individual Sum)

Maintain a counter for each literal: in how

many unresolved clauses it appears ?
Decide on the literal with the largest counter.
Requires O(#literals) queries for each
decision.

Decision heuristics
MOM (Maximum Occurrence of clauses of Minimum size).

Let f*(x) be the # of unresolved shortest

clauses containing x. Choose x that maximizes:
((f*(x) + f*(!x)) * 2k + f*(x) * f*(!x)

k is chosen heuristically.
The idea:
Give preference to satisfying small clauses.
Among those, give preference to balanced
variables (e.g. f*(x) = 3, f*(!x) = 3 is better
than f*(x) = 1, f*(!x) = 5).

Implication graphs and learning

Current truth assignment: {x9=0@1 ,x10=0@3, x11=0@3, x12=1@2, x13=1@2}
Current decision assignment: {x1=1@6}

1 ==(
(xx1 1xx2)2)
1

x2=1@6

2 ==(
(xx1 1xx3 3xx9)9)
2
3 ==(
(xx2 2xx3 3xx4)4)
3
4 ==(
(xx4 4xx5 5xx1010) )
4
5 ==(
(xx4 4xx6 6xx1111) )
5
6 ==(
(xx5 5xx6)6)
6
7 ==(x(x1 xx7 xx12) )
7
1
7
12
8 ==(x(x1xx8) )
8
1
8
9 ==(
(xx7 7xx8 8xx1313) )
9

x10=0@3

1
x1=1@6

2
2
x9=0@1

3
3
x3=1@6

4
4
x4=1@6

5
5

x5=1@6

6
6

conflict

x6=1@6

x11=0@3

We learn the conflict clause 10 : (: x1 x9 x11 x10)

and backtrack to the highest (deepest) dec. level in this clause (6).

Implication graph, flipped

assignment
1 ==(
(xx1 1xx2)2)
1

x13=1@2

2 ==(
(xx1 1xx3 3xx9)9)
2
3 ==(
(xx2 2xx3 3xx4)4)
3
4 ==(
(xx4 4xx5 5xx1010) )
4
5 ==(
(xx4 4xx6 6xx1111) )
5
6 ==(
(xx5 5xx6)6)
6
7 ==(x(x1 xx7 xx12) )
7
1
7
12
8 ==(x(x1xx8) )
8
1
8
9 ==(
(xx7 7xx8 8xx1313) )
9
10 : :(:(:xx1 xx9 xx11 xx10) )
10
1
9
11
10

x8=1@6

x9=0@1

10

x10=0@3

10

8
x1=0@6

10

x11=0@3
Due to the
conflict clause

7
7

9
9

x7=1@6

x12=1@2

We learn the conflict clause 11 : (:x13 x9 x10 x11 :x12)

and backtrack to the highest (deepest) dec. level in this clause (3).

Non-chronological backtracking
3

Which assignments caused

the conflicts ?

Decision
level

x9= 0@1
x10= 0@3
x11= 0@3
x12= 1@2

These assignments
are sufficient for
causing a conflict.

x1

x13= 1@2

Backtrack to decision level

3

Nonchronological
backtracking

Non-chronological backtracking (option

#1)

So the rule is: backtrack to the largest decision

level in the conflict clause.

Q: What if the flipped assignment works ?

A: continue to the next decision level, leaving
the current one without a decision variable.

Backtracking back to this level will lead to another

conflict and further backtracking.

Non-chronological Backtracking
x1 = 0
x2 = 0
x3 = 1

x3 = 0

x4 = 0
x5 = 0

x6 = 0
...

x5 = 1
x7 = 1
x9 = 0

x9 = 1

More Conflict Clauses

Def: A Conflict Clause is any clause implied by the

formula
Let L be a set of literals labeling nodes that form a cut
in the implication graph, separating the conflict node
from the roots.
Claim: l2L:l is
a Conflict Clause.
1. (x10 :x1 x9 x11)
x =0@3
2

10

x2=1@6

1
x1=1@6

2
2
x9=0@1

3
3
x3=1@6

x5=1@6

x4=1@6

5
5
x11=0@3

2. (x10 :x4 x11)

conflict

x6=1@6

3. (x10 :x2 :x3 x11)

Conflict clauses

How many clauses should we add ?

If not all, then which ones ?

Shorter ones ?
Check their influence on the backtracking
level ?
The most influential ?

The answer requires two definitions:

Asserting clauses
Unique Implication points (UIPs)

Asserting clauses

Def: An Asserting Clause is a Conflict Clause

with a single literal from the current decision
level. Backtracking (to the right level) makes it
a Unit clause.
Modern solvers only consider Asserting
Clauses.

Conflict-driven backtracking

(option

#2)

Previous method: backtrack to highest decision level

in conflict clause (and erase it).
A better method (empirically): backtrack to the
second highest decision level in the clause, without
erasing it. The asserted literal is implied at that
level.
3

In our example: (x10 :x4 x11)

Previously we backtracked to decision level 6.

Now we backtrack to decision level 3. x4 = 0@3 is implied.

Conflict-driven Backtracking
x1 = 0
x2 = 0

x5 = 1

x3 = 1

x7 = 1

x9 = 1

x4 = 0

x3 = 1

x6 = 0

x5 = 0

x9 = 0

...

Conflict-Driven Backtracking

So the rule is: backtrack to the second highest

decision level dl, but do not erase it.

If the conflict clause has a single literal, backtrack to

decision level 0.

Q: It seems to waste work, since it erases

assignments in decision levels higher than dl,
unrelated to the conflict.
A: indeed. But allows the SAT solver to redirect
itself with the new information.

Progress of a SAT solver

work invested in refuting x=1

(some of it seems wasted)
C

x=1
C5

C2

Decision
Level

C1

BCP

Refutation of x=1

C4
C3

Time

Decision
Conflict

Conflict clauses and Resolution

The Resolution is a sound inference rule:

Example:

Conflict clauses and resolution

Consider the following example:

Conflict clause: c5: (x2 :x4

x10)

Conflict clauses and resolution

Conflict clause: c5: (x2 :x4

Resolution order: x4,x5,x6,x7

T1 = Resolve(c4,c3,x7) = (:x5 :x6)

T2 = Resolve(T1, c2, x6) = (:x4 :x5 X10 )
T3 = Resolve(T2,c1,x5) = (x2 :x4 x10 )

x10)

Finding the conflict clause:

cl is asserting
the first UIP

Applied to our example:

GSAT: stochastic SAT solving

Given a CNF formula , choose max_triesandmax_flips
fori=1tomax_tries{
T:=randomlygeneratedtruthassignment
forj=1tomax_flips{
ifTsatisfiesreturnTRUE

Many
alternative
heuristics

[Link]
the#ofsatisfiedclauses(breaktiesrandomly).
T:=Twithvsassignmentflipped.}}

Numerous progressing heuristics

Hill-climbing
Tabu-list
Simulated-annealing
Random-Walk
Min-conflicts
...

: Formulation of problems as SAT

k-Coloring
The K-Coloring problem:
Given an undirected graph G(V,E) and a natural number k, is
there an assignment color:

: Formulation of problems as SAT

k-Coloring
xi,j = node i is assigned the color j (1 i n, 1 j k)
Constraints:
i) At least one color to each node: (x1,1 x1,2 x1,k )
n k

V ( xi , j )

i 1 j 1

ii) At mostn one

k 1 kcolor to each node:
(xi , j xi ,t )
i 1 j 1 t j 1

iii) Coloring constraints: for each i,j such that (i,j) 2 E:

k

(xi ,c x j ,c )

c 1