3SAT  A Counting Solver 2
 From: Russell Easterly <logiclab@xxxxxxxxxxx>
 Date: Mon, 24 Nov 2008 11:22:54 0800 (PST)
Counting SAT Solver 2
I previously described this solver.
I have made improvements to how this
solver backtracks.
Notation:
A,B,C,D,E = 3SAT variables
a,b,c,d,e = 3SAT literals
~a = inverse of literal a
U,V,W,X,Y,Z = clauses
U0,U1,U2 = clause variables
u0,u1,u2 = clause literals
(a+b+c) = 3clause (A OR B OR C)
(a,b,c) = 1 in 3 clause (choose one of a, b, or c)
a&b = A AND B
Normally, we talk about the assignment
of variables. For example, A=True means
the variable A has been assigned the
Boolean value "True".
I will usually talk about assignment of
literals. ~a=True means the literal ~a
is True. This would mean the variable A
is assigned false. I will use literal
assignments throughout this post except
when I specifically state I am using
variable assignments.
The idea behind a counting solver is simple.
Assume we are given a Boolean expression
(3SAT instance) with n variables and m clauses.
Assume I assign each variable to a position
in an nbit binary number. I can then ask
what is the smallest binary number that
represents a satisfying assignment to the
3SAT instance?
The simplest counting solver just counts
up from 0. Luckily, there are faster ways
to find the smallest number that is a
satisfying assignment.
This particular solver uses clauses instead
of variables. Assume I assign 0, 1, or 2
to each literal inside a clause. If the 3SAT
instance is satisfied there is at least one
literal in each clause that is satisfied.
This means there is a lowest order literal
that is satisfied (literal 0, 1, or 2).
Now, I assign each clause to a position in
a base 3 number and ask what is the smallest
base 3 number that satisfies the 3SAT instance.
I show how to derive a set of DNF expressions
that solves the question of what is the smallest
base 3 number that satisfies the clauses.
I start by converting the 3SAT instance into
a form I have been studying.
Create a "1 in 3" clause for each 3clause in the
original 3SAT instance. I will create a "clause
variable" for each literal in each clause in the
original 3SAT instance. "1 in 3" means choose
exactly one of the three literals in the clause.
3SAT example:
(a+b+c)(~a+~b+~c)(~b+d+e)
(~b,c,~d)(~a+~c+~e)(~c+~d+e)
Assign a 1 in 3 clause to each 3SAT clause:
(a+b+c) = (u0,u1,u2)
(~a+~b+~c) = (v0,v1,v2)
(~b+d+e) = (w0,w1,w2)
(~b,c,~d) = (x0,x1,x2)
(~a+~c+~e) = (y0,y1,y2)
(~c+~d+e) = (z0,z1,z2)
Notice that if u0 (literal a in clause U)
is True then v0 (literal ~a in clause V)
can not be True. To prevent this, I create
a set of 2clauses for each literal and its
inverse in the original expression.
For this example, I would add the clause:
(~u0+~v0)
Converted expression:
(a+b+c)(~a+~b+~c)(~b+d+e)
(~b,c,~d)(~a+~c+~e)(~c+~d+e)
=
(u0,u1,u2)(v0,v1,v2)(w0,w1,w2)
(x0,x1,x2)(y0,y1,y2)(z0,z1,z2)
(~u0+~v0)(~u0+~y0)
(~u1+~v1)(~u1+~w0)(~u1+~x0)
(~u2+~v2)(~u2+~y1)(~u2+~z0)
(~v2+~x1)(~x1+~y1)(~x1+~z0)
(~w1+~x2)(~w1+~z1)
(~w2+~y2)(~y2+~z2)
Any satisfying assignment to the converted
expression is also a satisfying assignment
to the original 3SAT expression.
If there is a satisfying assignment of
clause variables where U0=True then
there is a satisfying assignment for
the original expression where literal
a in clause U is the lowest order
literal that is satisfied (A=True).
If U2=False is part of the satisfying
assignment then literal c in clause U
is not the lowest order literal
satisfied in clause U. This doesn't mean
C=False, but it does mean (a+b) is True.
Now I convert the expression to 2+SAT
(a combination of 2clauses and 3clauses).
I use this conversion:
(u0,u1,u2) = (u0+u1+u2)(~u0+~u1)(~u0+~u2)(~u1+~u2)
Fully converted expression:
(a+b+c)(~a+~b+~c)(~b+d+e)
(~b,c,~d)(~a+~c+~e)(~c+~d+e)
=
(u0+u1+u2)(v0+v1+v2)(w0+w1+w2)
(x0+x1=x2)(y0+y1+y2)(z0+z1+z2)
(~u0+~v0)(~u0+~y0)
(~u1+~v1)(~u1+~w0)(~u1+~x0)
(~u2+~v2)(~u2+~y1)(~u2+~z0)
(~v2+~x1)(~x1+~y1)(~x1+~z0)
(~w1+~x2)(~w1+~z1)
(~w2+~y2)(~y2+~z2)
(~u0+~u1)(~u0+~u2)(~u1+~u2)
(~v0+~v1)(~v0+~v2)(~v1+~v2)
(~w0+~w1)(~w0+~w2)(~w1+~w2)
(~x0+~x1)(~x0+~x2)(~x1+~x2)
(~y0+~y1)(~y0+~y2)(~y1+~y2)
(~z0+~z1)(~z0+~z2)(~z1+~z2)
I will simply throw away the 3clauses
leaving me with this 2SAT instance:
(~u0+~v0)(~u0+~y0)
(~u1+~v1)(~u1+~w0)(~u1+~x0)
(~u2+~v2)(~u2+~y1)(~u2+~z0)
(~v2+~x1)(~x1+~y1)(~x1+~z0)
(~w1+~x2)(~w1+~z1)
(~w2+~y2)(~y2+~z2)
(~u0+~u1)(~u0+~u2)(~u1+~u2)
(~v0+~v1)(~v0+~v2)(~v1+~v2)
(~w0+~w1)(~w0+~w2)(~w1+~w2)
(~x0+~x1)(~x0+~x2)(~x1+~x2)
(~y0+~y1)(~y0+~y2)(~y1+~y2)
(~z0+~z1)(~z0+~z2)(~z1+~z2)
This 2SAT instance is easily satisfied
by assuming all variables are False.
Is there a satisfying assignment
where exactly m clause variables
are True? If so, this is a solution
to the original 3SAT expression.
I use a trivial form of resolution
to derive a set of DNF expressions
that give solutions to the 2SAT instance.
The resolution is trivial because
all the literals are negated.
This means no "resolvent" clauses
will be generated. I will simply
remove clauses containing the
variable being resolved.
There are two ways I can do resolution.
We normally assume a variable
is False unless it must be True.
I write this as:
a=(b+c)
This means literal a is False
(and variable A is False) unless
literal b is True or literal c is True.
Or, I can assume a variable is True
unless it must be False.
I write this as:
~a=(b+c)
This means literal ~a is False
(and variable A is True) unless
literal b is True or literal c is True.
I will assume a clause variable is True
unless it must be False.
I resolve the clause variables in a
specific order. The reason I use this
ordering should become obvious.
Start with the lowest order
clause variable, U2.
The literal ~u2 must be True if
literal v2 is True because of the
clause (~u2+~v2).
The complete expression for ~u2:
~u2=z0+y1+v2+u1+u0
Remove all clauses with U2
and repeat the process for U1, U0, etc:
~u2=z0+y1+v2+u1+u0
~u1=x0+w0+v1+u0
~u0=y0+v0
~v2=x1+v1+v0
~v1=v0
~v0=?
~w2=y2+w1+w0
~w1=z1+x2+w0
~w0=?
~x2=x1+x0
~x1=z0+y1+x0
~x0=?
~y2=z2+y1+y0
~y1=y0
~y0=?
~z2=z1+z0
~z1=z0
~z0=?
Order the expressions the way
they will be evaluated:
~z0=?
~z1=z0
~z2=z1+z0
~y0=?
~y1=y0
~y2=z2+y1+y0
~x0=?
~x1=z0+y1+x0
~x2=x1+x0
~w0=?
~w1=z1+x2+w0
~w2=y2+w1+w0
~v0=?
~v1=v0
~v2=x1+v1+v0
~u0=y0+v0
~u1=x0+w0+v1+u0
~u2=z0+y1+v2+u1+u0
Notice clause variables Z0,Y0,
X0,W0, and V0 are "independent".
This means these clause variables
can have any assignment.
I will assume independent clause
variables are always True:
z0,y0,x0,w0,v0 = True
Once all the independent variables
are assigned we can compute the
assignments of all the other clause
variables:
z0,y0,x0,w0,v0 = True
>
z0~z1~z2y0~y1~y2x0~x1~x2w0~w1~w2v0~v1~v2~u0~u1~u2
Clause U is the highest order clause
not satisfied. Find the highest order
satisfied minterm in each DNF expression.
~u0=y0
~u1=x0
~u2=z0
The combination z0&y0&x0 causes clause U
to be unsatisfiable. I want to "increment"
the lowest order clause that causes the
contradiction. Clause X is the lowest order
clause causing the contradiction and
I want to guarantee ~x0 if z0 and y0 are True.
~x0=(z0&y0)
Adding this to our DNF expressions:
~z0=?
~z1=z0
~z2=z1+z0
~y0=?
~y1=y0
~y2=z2+y1+y0
~x0=(z0&y0)
~x1=z0+y1+x0
~x2=x1+x0
~w0=?
~w1=z1+x2+w0
~w2=y2+w1+w0
~v0=?
~v1=v0
~v2=x1+v1+v0
~u0=y0+v0
~u1=x0+w0+v1+u0
~u2=z0+y1+v2+u1+u0
X0 is no longer independent.
Now we have:
z0,y0,w0,v0 = True
>
z0~z1~z2y0~y1~y2~x0~x1x2w0~w1~w2v0~v1~v2~u0~u1~u2
Again, clause U is not satisfied.
~u0=y0
~u1=w0
~u2=z0
>
~w0=(z0&y0)
Adding this minterm:
~z0=?
~z1=z0
~z2=z1+z0
~y0=?
~y1=y0
~y2=z2+y1+y0
~x0=(z0&y0)
~x1=z0+y1+x0
~x2=x1+x0
~w0=(z0&y0)
~w1=z1+x2+w0
~w2=y2+w1+w0
~v0=?
~v1=v0
~v2=x1+v1+v0
~u0=y0+v0
~u1=x0+w0+v1+u0
~u2=z0+y1+v2+u1+u0
z0,y0,v0 = True
>
z0~z1~z2y0~y1~y2~x0~x1x2~w0~w1w2v0~v1~v2~u0u1~u2
This is a satisfying assignment to the original
3SAT instance.
z0,y0,x2,w2,v0,u1 = True
Mapping back to the original expression:
z0=~c, y0=~a, x2=~d,
w2=e, v0=~a, u1=b
~a,b,~c,~d,e = True
is a satisfying assignment for the
original 3SAT instance:
(a+B+c)(~A+~b+~c)(~b+d+E)
(~b,c,~D)(~A+~c+~e)(~C+~d+e)
There is one other rule I should include.
If the original 3SAT instance is
unsatisfiable, we will get something
like this:
~z0=?
~z1=z0
~z2=z1+z0
~y0=z0
~y1=z0+y0
~y2=z0+y1+y0
Clause Y is unsatisfiable if Z0=True.
Since Z0 can't depend on a higher
order variable, we must force it to False.
The DNF expressions become:
~z0=True
~z1=z0
~z2=z1+z0
~y0=z0
~y1=z0+y0
~y2=z0+y1+y0
I don't have to use backtracking to
derive the DNF expressions.
Consider the original formulas for
clause U:
~u0=y0+v0
~u1=x0+w0+v1+u0
~u2=z0+y1+v2+u1+u0
I can compute every combination
with one minterm from each expression.
For example, y0&x0&z0 will make clause
U unsatisfiable.
I can ignore combinations where there
are two literals from the same clause.
For example, I can ignore y0&x0&y1
because I know only one literal from
clause Y can be True.
I can also ignore combinations that
include literals from the clause I
am processing because of subsumption.
For example, y0&x0&u1 > ~u1=(y0&x0).
Adding this minterm to our existing
expression for ~u1:
~u1=(y0&x0)+x0+w0+v1+u0
We see that (y0&x0) is subsumed by x0.
Computing all the valid combinations
for clause U:
y0&x0&z0 > ~x0=(z0&y0)
y0&x0&v2 > ~v2=(y0&x0)
y0&w0&z0 > ~w0=(z0&y0)
y0&w0&v2 > ~v2=(y0&w0)
y0&v1&z0 > ~v1=(z0&y0)
v0&x0&z0 > ~v0=(z0&x0)
v0&x0&y1 > ~v0=(y1&x0)
v0&w0&z0 > ~v0=(z0&w0)
v0&w0&y1 > ~v0=(y1&w0)
Adding these new minterms:
~z0=?
~z1=z0
~z2=z1+z0
~y0=?
~y1=y0
~y2=z2+y1+y0
~x0=(z0&y0)
~x1=z0+y1+x0
~x2=x1+x0
~w0=(z0&y0)
~w1=z1+x2+w0
~w2=y2+w1+w0
~v0=(z0&x0)+(y1&x0)+(z0&w0)+(y1&w0)
~v1=(z0&y0)+v0
~v2=x1+(y0&x0)+(y0&w0)+v1+v0
~u0=y0+v0
~u1=x0+w0+v1+u0
~u2=z0+y1+v2+u1+u0
I can now repeat the process with clause V:
~v0=(z0&x0)+(y1&x0)+(z0&w0)+(y1&w0)
~v1=(z0&y0)+v0
~v2=x1+(y0&x0)+(y0&w0)+v1+v0
z0&x0&y0 > ~x0=(z0&y0)
z0&x0&y0&w0 > ~w0=(z0&y0&x0)
z0&x0&y0&v1 > ~v1=(z0&y0&x0)
z0&x0&v0y0 > ~v0=(z0&y0&x0)
z0&x0&v0&y0&w0 > ~v0=(z0&y0&x0&w0)
z0&w0&y0&x1 > ~w0=(z0&y0&x1)
z0&w0&y0&x0 > ~w0=(z0&y0&x0)
z0&w0&y0 > ~w0=(z0&y0)
It is easy to see this "brute force"
method generates a lot of minterms
that don't add any meaningful
information to the DNF expressions.
Not only are many of the minterms
redundant, many will be subsumed like:
~w0=(z0&y0) subsumes
(z0&y0&x0) and (z0&y0&x1).
Many of these minterms can never be True.
For example, ~v0=(z0&y0&x0) can never
be True because of ~x0=(z0&y0).
Clearly, the minterms generated by
backtracking is a subset of the minterms
generated by the brute force method.
It is easy to show that all we need
to solve the 3SAT instance is a polynomial
size subset of the DNF expressions:
These are all the minterms we need to find a solution:
z0,y0,x2,w2,v0,u1 = True
~z0=?
~z1=z0
~z2=z0
~y0=?
~y1=y0
~y2=y0
~x0=(z0&y0)
~x1=z0
~x2=?
~w0=(z0&y0)
~w1=x2
~w2=?
~v0=?
~v1=v0
~v2=v0
~u0=y0
~u1=?
~u2=u1
Only two of these minterms, ~x0=(z0&y0)
and ~w0=(z0&y0) were added by backtracking.
The rest of the terms were found during
resolution.
Resolution can never generate more than a
polynomial number of minterms. Each clause
variable only depends on clause variables
that are higher order.
The minterms generated by resolution
have only one variable. This means if
u3 is the kth highest order clause
variable then u3 has, at most, k1
minterms in its expression due to resolution.
I can prove NP=P if I can show no DNF
expression has more than a polynomial
number of minterms.
I can show certain clauses can never have
more than a polynomial number of minterms.
Consider the highest order clause, Z.
Clause Z will always be satisfied unless
the 3SAT instance is unsatisfiable.
This means clause Z can only fail to
be satisfied once during the search.
The second highest clause, Y, only depends
on clause variables in Z. This means
clause Y can only fail to be satisfied
three times, once for each Z clause variable.
Similar arguments show if clause U is
the kth highest order clause then U can
fail to be satisfied at most 3^k times.
This isn't much of a lower bound if there
are a lot of clauses, but it does show
the highest order clauses have, at most,
a polynomial number of minterms.
I can also show the lowest order clause, U,
has, at most, a polynomial number of minterms.
Since there are no lower order clauses
that can add terms to clause U, clause
U will only have the terms generated
during resolution. I have already shown
resolution only creates a polynomial
number of terms.
Russell
 2 many 2 count
.
 Prev by Date: Re: dictionary and anagrams
 Next by Date: Re: Problems in NP^(NP^NP) that are not in NP^NP?
 Previous by thread: Ryhmän sfnet.keskustelu.kieli.kaantaminen virallinen kuvaus
 Next by thread: Re: Problems in NP^(NP^NP) that are not in NP^NP?
 Index(es):
Relevant Pages
