# 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) = 3-clause (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 n-bit 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 3-clause 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 2-clauses 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 2-clauses and 3-clauses).

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 3-clauses

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, k-1

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):