Guest
|
 Posted: Sat Jul 26, 2008 9:12 am Post subject: 3SAT - Reviving Resolution |
 |
|
It is known that resolution proofs for the
unsatisfiability of certain types of Boolean
Satisfibility problems, like the pigeon hole
problem, must be exponential in size.
Even when resolution is provably polynomial,
like resolving 2-clauses, the average number of
steps is often close to the worse case.
Even so, resolution is a powerful method for
reducing Boolean expressions.
I describe a method to convert 3SAT into 2+SAT.
2+SAT is a combination of 2-clauses and 3-clauses.
I show how at least half of the variables
in the 2+SAT instance can always be resolved
in a polynomial number of operations.
The resolved 2+SAT expression can often
be further reduced using the pure literal rule,
subsumption, and more resolution.
I have previously posted the following transformation.
Given the 3SAT clause (a+b+c):
(a+b+c) =
(v1+v2+v3)&
(a+~v1)&(b+~v2)&(c+~v3)&
(~v1+~v2)&(~v1+~v2)&(~v2+~v3)
where v1, v2, and v3 are unique to this clause.
Notice that the original variables, a,b, and c,
only appear in 2-clauses. This means resolving
the original variables can only result in 2-clauses.
Assume we have the 3SAT instance: V & W & X & Y & Z where
V = (a+b+c)
W = (~a+~b+~c)
X = (a+~d+~e)
Y = (b+d+f)
Z = (~c+e+~f)
Converting the 3SAT instance using the method above and
resolving for the original variables a,b,c,d,e, and f we get:
(a+b+c)&(~a+~b+~c)&(a+~d+~e)&(b+d+f)&(~c+e+~f)
=
(v1+v2+v3)&(w1+w2+w3)&(x1+x2+x3)&(y1+y2+y3)&(z1+z2+z3)&
(~v1+~v2)&(~v1+~v3)&(~v2+~v3)&
(~w1+~w2)&(~w1+~w3)&(~w2+~w3)&
(~x1+~x2)&(~x1+~x3)&(~x2+~x3)&
(~y1+~y2)&(~y1+~y3)&(~y2+~y3)&
(~z1+~z2)&(~z1+~z3)&(~z2+~z3)&
(~v1+~w1)&(~w1+~x1)&
(~v2+~w2)&(~w2+~y1)&
(~v3+~w3)&(~v3+~z1)&
(~x2+~y2)&
(~x3+~z2)&
(~y3+~z3)
Notice the last set of 2-clauses. Consider (~v1+~w1).
v1 maps to the literal a in clause V.
w1 maps to the literal ~a in clause W.
All the 2-clauses in the last section are of this form:
(a+~a)
where a and ~a are literals in the original 3SAT instance.
Any 3SAT instance can be converted directly to this form.
Each clause, V, is replaced by:
V => (v1+v2+v3)(~v1+~v2)(~v1+~v3)(~v2+~v3)
If v1 maps to literal a in the original clause V,
and w1 maps to literal ~a in clause W, then there
is a 2-clause: (~v1+~w1).
If the 2+SAT instance has a satisfying assignment
where clause variable v1 is true, then there is
a satisfying assignment of the original 3SAT instance
where the literal a is true.
If there is a satisfying assignment where v1 is false,
there is a satisfying assignment where some literal
in V, other than literal a, is true. In our example,
this means v2 (=b) or v3 (=c) is true. Literal a may
be true or false in this satisfying assignment.
In our example above it is possible for v1 (literal a in clause V)
to be false and x1 (literal a in clause X) to be true.
Once a 3SAT instance has been converted to this 2+SAT form,
the following three statements are true.
1) If a clause literal is pure we can assume it is true.
A literal is pure if its inverse does not appear in any clause.
2) If the inverse of a clause literal only appears in 2-clauses,
the clause variable can be resolved in a polynomial number of steps.
In our example, the resolution of v1 gives:
(v1+v2+v3)&(~v1+~w1) => (~w1+v2+v3)
The resolvent of a 3-clause and a 2-clause is, at worse,
another 3-clause. There can be, at most, O(n^3) 3-clauses.
3) All clause variables that map to un-negated literals in
the original clause can be resolved in polynomial time.
This follows from (2) and the structure of the 2+SAT instance.
Initially, no clause variable appears negated in a 3-clause.
Assume we resolve v1 which maps to the un-negated literal, a.
~v1 only appears in 2-clauses where the other literal in the
2-clause maps to a negated literal in the original expression.
For example,
w1 in (~v1+~w1) maps to the negated literal, ~a, in clause W.
This means any resolvent 3-clause will only have negated
clause literals that map to negated literals in the original clause.
As long as we only resolve clause variables that map to
un-negated literals in the original expression, all resolvent
clauses will be, at worst, 3-clauses.
Worked example:
Since we want to determine a satisfying assignment for the
original expression, I will need to keep track of formulas
for the resolved variables. I will start by resolving v1.
I will assume v1 is always false unless it must be true.
v1 must be true if both v2 and v3 are false:
v=~v2&~v3
(a+b+c)&(~a+~b+~c)&(a+~d+~e)&(b+d+f)&(~c+e+~f)
=
(v1+v2+v3)&(w1+w2+w3)&(x1+x2+x3)&(y1+y2+y3)&(z1+z2+z3)&
(~v1+~v2)&(~v1+~v3)&(~v2+~v3)&
(~w1+~w2)&(~w1+~w3)&(~w2+~w3)&
(~x1+~x2)&(~x1+~x3)&(~x2+~x3)&
(~y1+~y2)&(~y1+~y3)&(~y2+~y3)&
(~z1+~z2)&(~z1+~z3)&(~z2+~z3)&
(~v1+~w1)&(~w1+~x1)&(~v2+~w2)&(~w2+~y1)&
(~v3+~w3)&(~v3+~z1)&(~x2+~y2)&(~x3+~z2)&(~y3+~z3)
Resolving on v1:
v1=~v2&~v3
(~w1+v2+v3)&(w1+w2+w3)&(x1+x2+x3)&(y1+y2+y3)&(z1+z2+z3)&
(~v2+~v3)&
(~w1+~w2)&(~w1+~w3)&(~w2+~w3)&
(~x1+~x2)&(~x1+~x3)&(~x2+~x3)&
(~y1+~y2)&(~y1+~y3)&(~y2+~y3)&
(~z1+~z2)&(~z1+~z3)&(~z2+~z3)&
(~w1+~x1)&(~v2+~w2)&(~w2+~y1)&
(~v3+~w3)&(~v3+~z1)&(~x2+~y2)&
(~x3+~z2)&(~y3+~z3)
Clause variables v1,v2,v3,x1,y1,y2,y3, and z2
all map to un-negated literals in the original
expression.
Resolving for v1,v2,v3,x1,y1,y2,y3, and z2 in order:
v1=~v2&~v3;
v2=w1&~v3;
v3=w1&w2;
x1=~x2&~x3;
y1=~y2&~y3;
y2=w2&~y3;
y3=w2&x2;
z2=~z1&~z3
(w1+w2+w3)&
(~w1+~w2+~w3)&(~w1+x2+x3)&(~w2+~x2+~z3)&(z1+~x3+z3)&
(~w1+~w2)&(~w1+~w3)&(~w2+~w3)&
(~x2+~x3)&(~z1+~z3)&(~v3+~z1)
Clause (~w1+~w2) subsumes (~w1+~w2+~w3) giving us:
(w1+w2+w3)&
(~w1+x2+x3)&(~w2+~x2+~z3)&(z1+~x3+z3)&
(~w1+~w2)&(~w1+~w3)&(~w2+~w3)&
(~x2+~x3)&(~z1+~z3)&(~v3+~z1)
Clause literal ~w3 only appears in 2-clauses.
Resolving w3:
w3=~w1&~w2
(~w1+x2+x3)&(~w2+~x2+~z3)&(z1+~x3+z3)&
(~w1+~w2)&(~x2+~x3)&(~z1+~z3)&(~v3+~z1)
Clause literal ~w1 is pure:
~w1=T
(~w2+~x2+~z3)(z1+~x3+z3)
(~x2+~x3)(~z1+~z3)(~v3+~z1)
Clause literals ~w2 and ~x2 are pure:
~w2=T, ~x2=T
(z1+~x3+z3)(~z1+~z3)(~v3+~z1)
Clause literals ~x3 and ~v3 are pure:
~x3=T, ~v3=T
(~z1+~z3)
Finally, ~z1 and ~z3 are pure, completing
the assignment.
~w1,~w2,~x2,~x3,~v3,~z1,~z3=T
w3 = ~w1 & ~w2 = T
z2 = ~z1 & ~z3 = T
y3 = w2 & x2 = F
y2 = w2 & ~y3 = F
y1 = ~y2 & ~y3 = T
x1 = ~x2 & ~x3 = T
v3 = w1 & w2 = F
v2 = w1 & ~v3 = F
v1 = ~v2 & ~v3 = T
We only care about clause variables that are true:
v1,w3,x1,y1,z2=T
Mapping back to the originals clauses we get:
a,b,~c,e=T
(A+B+c)(~a+~b+~C)(A+~d+~e)(B+d+f)(~C+E+~f)
Russell
- 2 many 2 count |
|
