Two methods for finding a model of a formula
Incomplete=they may fail
Two different kinds of incompleteness (more later)
Both work on CNFs
Works on CNFs: {C1, ..., Cm}
Find a model = find an interpretation satisfying all clauses
Principle:
if I satisfies 3 clauses and I' 5, the latter is "closer" to be a model than the former
works by picking an interpretation and iteratively trying to increase the number of satisfied clauses
Given an interpretation I, try to change the value of a single
variable
(if true make it false and vice versa)
Does this change increase the number of satisfied clauses?
Try this for all variables
given I, change the value of a variable
determine the number of satisfied clauses
do this for all variables
pick the best, in terms of number of satisfied clauses
(one point missing)
limit=we change a variable at time
possible situation: I → I' → I'' → I
we keep cycling over them because the other close interpretations satisfy less clauses
we are stuck in a local maximum
(w.r.t. the surrounding interpretations, we have reached a maximum, but this is
not the overall maximum)
but a model exists
after a fixed number of iterations (say, 10000), GSAT stops and picks another random interpretation
try this for a fixed number of times (say, 10)
still, we may end up in a local maximum every time
GSAT is incomplete
in general, we cannot tell in advance whether GSAT will work on a
particular formula
(only way is: try it and see if it finds a model)
Still works on CNFs: {C1, ..., Cm}
Principle:
if a clause contains a single literal, every model makes that literal true
replace every occurrence of that variable with its value
obvious on an example (next)
{x, ¬x ∨ y, x ∨ ¬z, y ∨ z, y ∨ ¬z}
every model of this set has x=true
(otherwise, the clause x would be false)
model=interpretation that satisfies all clauses
(cont.)
{x, ¬x ∨ y, x ∨ ¬z, y ∨ z, y ∨ ¬z}
every model of this set has x=true
under this assumption:
from unit clauses to truth values
propagate truth values to clauses
repeat, if needed
{x, ¬x ∨ ¬y, x ∨ ¬z, y ∨ z, y ∨ ¬z}
x=true
replace x=true in the set and simplify:
{x, ¬x ∨ ¬y, x ∨ ¬z, y ∨ z, y ∨ ¬z} =
{true, ¬true ∨ ¬y, true ∨ ¬z, y ∨ z, y ∨ ¬z} =
{true, false ∨ ¬y, true ∨ ¬z, y ∨ z, y ∨ ¬z} =
{¬y, y ∨ z, y ∨ ¬z}
simplifications based on:
(cont.)
so far: x=true and the set simplifies to:
{¬y, y ∨ z, y ∨ ¬z}
all models has y false
set y=false and simplify:
{¬y, y ∨ z, y ∨ ¬z} =
{true, false ∨ z, false ∨ ¬z} =
{z, ¬z}
contradiction
the set is unsatisfiable
next: formal definition of algorithm
accumulate truth values in a partial interpretation I
partial interpretation=truth evaluation of some variables
initially, no variable is evaluated
(full) interpretations are a particular case (all variables evaluated)
stop on contradiction in the partial interpretation
try to make all propagations at the same time
stop on contradiction in I or I'
{x ∨ y ∨ ¬ z, y, ¬x ∨ w, ¬y ∨ w}
y=true → I
formula becomes:
{x ∨ y ∨ ¬ z, y, ¬x ∨ w,
¬y ∨ w} =
{¬x ∨ w, w}
w=true → I
replace in formula and simplify:
{¬x ∨ w, w} = ∅
all clauses are satisfied by I={y=true, w=true}
formula is satisfied
model=any extension of I to all variables
(e.g., x=false, y=true, z=true, w=true}
{x ∨ y, x ∨ ¬y, ¬z ∨ ¬x ∨ y, ¬x ∨ ¬y, z}
add z=true to I
replace z with its truth value and simplify:
{x ∨ y, x ∨ ¬y, ¬z ∨ ¬x ∨ y, ¬x ∨ ¬y, z} =
{x ∨ y, x ∨ ¬y, ¬x ∨ y, ¬x ∨ ¬y}
no unit clause
algorithm stops
(cont.)
formula {x ∨ y, x ∨ ¬y, ¬x ∨ y, ¬x ∨ ¬y} is inconsistent
yet, unit propagation did not reach contradiction
happened also in the previous example, with a consistent formula
if unit propagation does not reach contradiction, we cannot say whether formula is consistent or not
unit propagation is incomplete
GSAT and Unit Propagation are incomplete in two different ways:
last point on next page
Horn clause: a clause containing at most a positive literal
= contains zero or one positive literal
examples:
(last two examples: zero positive literal, still Horn)
Horn formula: set of Horn clauses
unit propagation is complete on Horn formulae
in general, it is not because it might not reach contradiction even if formula is unsatisfiable
never the case on Horn formulae
unit propagation does not reach contradiction on an Horn formula ⇒ formula is satisfiable
assume unit propagation does not reach contradiction
let I be the partial interpretation and F the set of remaining clauses
all clauses are made of at least two literals, none of them evaluated in I
at most one positive=at least one negative
setting all variables to false, all clauses are satisfied
conclusion:
if unit propagation does not reach contradiction, the set is satisfiable
(model is I plus all other variables set to false
{ x1 ∨ ¬x2 ∨ ¬x3, ¬x1 ∨ x2 ∨ ¬x3, x4 ∨ ¬x5, x5, ¬x1 ∨ x3 ∨ ¬x4, ¬x2 ∨ ¬x4 ∨ ¬x5 }
(cont.){ x1 ∨ ¬x2 ∨ ¬x3, ¬x1 ∨ x2 ∨ ¬x3, x4 ∨ ¬x5, x5, ¬x1 ∨ x3 ∨ ¬x4, ¬x2 ∨ ¬x4 ∨ ¬x5 }
x5 is a unit clause
set x5=true
replace x5 with true
{
x1 ∨ ¬x2 ∨ ¬x3,
¬x1 ∨ x2 ∨ ¬x3,
x4 ∨ ¬x5,
x5,
¬x1 ∨ x3 ∨ ¬x4,
¬x2 ∨ ¬x4 ∨ ¬x5
}
simplify:
{ x1 ∨ ¬x2 ∨ ¬x3, ¬x1 ∨ x2 ∨ ¬x3, x4, ¬x1 ∨ x3 ∨ ¬x4, ¬x2 ∨ ¬x4 }
(cont.){ x1 ∨ ¬x2 ∨ ¬x3, ¬x1 ∨ x2 ∨ ¬x3, x4, ¬x1 ∨ x3 ∨ ¬x4, ¬x2 ∨ ¬x4 }
set x4=true
replace:
{
x1 ∨ ¬x2 ∨ ¬x3,
¬x1 ∨ x2 ∨ ¬x3,
x4,
¬x1 ∨ x3 ∨ ¬x4,
¬x2 ∨ ¬x4
}
simplify:
{ x1 ∨ ¬x2 ∨ ¬x3, ¬x1 ∨ x2 ∨ ¬x3, ¬x1 ∨ x3, ¬x2 }
(cont.){ x1 ∨ ¬x2 ∨ ¬x3, ¬x1 ∨ x2 ∨ ¬x3, ¬x1 ∨ x3, ¬x2 }
clause ¬x2 is unary
set x2=false
replace:
{
x1 ∨ ¬x2 ∨ ¬x3,
¬x1 ∨ x2 ∨ ¬x3,
¬x1 ∨ x3,
¬x2
}
simplify:
{ ¬x1 ∨ ¬x3, ¬x1 ∨ x3 }
{ ¬x1 ∨ ¬x3, ¬x1 ∨ x3 }
no unit clause
propagation stops
set remaining variables to false:
all clauses are binary and Horn,
so they contain at least a negative literal each
setting all variables to false makes them true
result is assignment { x1=false, x2=false, x3=false, x4=true, x5=true }
this is a model of the original CNF
worst case?
{ x1∨¬x2, x2∨¬x3, ... x98∨¬x99, x99∨¬x100, x100 }
first scan produces I'={x100=true}
scan for replacing removes x100 and simplifies x99∨¬x100 to x99
second scan produces I'={x99=true}
scan for replacing removes x99 and simplifies x98∨¬x99 to x98
etc.
100+99+98...=?
like a triangle, area is base*height/2
cost is in the order of n2, where n is the number of variables
the problem with the previous set was:
we need to scan the whole set just to find out that x100 was only contained in the last two clauses
the solution:
create a data structure for finding the clauses that contain a given variable
array of n lists, where n is the number of variables
each list contains the clauses that contain a variables
first, assign number to clauses:
{ | x1∨¬x2, | x2∨¬x3, | ... | x98∨¬x99, | x99∨¬x100, | x100 | } |
C1 | C2 | ... | C98 | C99 | C100 |
second, scan the set and add each clauses to the lists
x1 | : | C1 | |
x2 | : | C1 | C2 |
... | |||
x99 | : | C98 | C99 |
x100 | : | C99 | C100 |
{ | x1∨¬x2, | x2∨¬x3, | ... | x98∨¬x99, | x99∨¬x100, | x100 | } |
C1 | C2 | ... | C98 | C99 | C100 |
x1 | : | C1 | |
x2 | : | C1 | C2 |
... | |||
x99 | : | C98 | C99 |
x100 | : | C99 | C100 |
scan the set, get x100=true
the list of x100 contains C99 and C100
simplify these clauses
C99 becomes unary, set x99=true
repeat
the data structure eliminates the need for scanning the set of clauses for simplifying
building the data structure is linear:
scan the set once, adding each clause to the lists of all variables it contains
every time we get a new value, we can immediately find the clauses that need simplification
linear for 3CNF (in general, for clauses of fixed length)
can be made linear in general
(use two lists, one for the clauses containing xi and one for the clauses containing ¬xi; use a counter for the number of literals left in clauses)