3SAT - A Counting Solver

I describe a new back-tracking SAT solver.
I described a similar SAT solver several years ago.
I think I called the earlier one the Simple SAT solver.
The Simple SAT solver was very slow, but this
one should be much faster.

The basic idea is simple.
Assume we have a 3SAT instance with n variables.
Assume each variable in the expression is assigned
to a bit position in an n-bit binary number.
What is the smallest binary number that is
a satisfying assignment?

I can start by trying 0.
If 0 is not a satisfying assignment,
then I can try 1, 2, 3, etc.
Luckily, there is a much faster way.

First, I will count with clauses instead
of variables.

Assume each literal in the clauses is numbered
with 0, 1, or 2 and I have ordered the clauses
from least significant to most significant.

Now, a base 3 number represents a potential
satisfying assignment to the clauses.
Each "trigit" describes which literal is true
in the clause associated with that trigit's position.

There may be more than one literal in the clause
that is true, but I am only interested in the
lowest numbered one.

I start by assigning "clause" variables to
each clause in the 3SAT instance.

(a+b+c)(~a+~b+~c)(~b+d+e)(~a+~c+~e)(~c+~d+e)

(a+b+c) = (v0,v1,v2)
(~a+~b+~c) = (w0,w1,w2)
(~b+d+e) = (x0,x1,x2)
(~a+~c+~e) = (y0,y1,y2)
(~c+~d+e) = (z0,z1,z2)

(v0,v1,v2) means choose exactly one of v0,v1, or v2.

Notice that if v0 (=a) is true then w0(=~a)
can't be true. To prevent this, I create
the clause (~v0+~w0). I need to do this
for every literal and its inverse in the original
expression.

(a+b+c)(~a+~b+~c)(~b+d+e)(~a+~c+~e)(~c+~d+e)
=
(v0,v1,v2)(w0,w1,w2)(x0,x1,x2)(y0,y1,y2)(z0,z1,z2)
(~v0+~w0)(~v0+~y0) (clause like a+~a)
(~v1+~w1)(~v1+~x0) (clause like b+~b)
(~v2+~w2)(~v2+~y1)(~v2+~z0) (like c+~c)
(~x1+~z1) (clauses like d+~d)
(~x2+~y2)(~y2+~z2) (clauses like e+~e)

I will "fix" one contradiction at a time.
A "contradiction" will be a 2-clause that
can't be satisfied with the current clause
assignment. I want to fix the contradiction
between the two highest order clauses.

To facilitate this, I will sort the 2-clauses
in reverse lexigraphical order. I assume each
clause has the lower order literal first and
the higher order literal second.

(a+b+c)(~a+~b+~c)(~b+d+e)(~a+~c+~e)(~c+~d+e)
=
(v0,v1,v2)(w0,w1,w2)(x0,x1,x2)(y0,y1,y2)(z0,z1,z2)
(~y2+~z2)
(~x2+~y2)
(~x1+~z1)
(~v2+~z0)
(~v2+~y1)
(~v2+~w2)
(~v1+~x0)
(~v1+~w1)
(~v0+~y0)
(~v0+~w0)

I will always check for contradictions in the order
given above. This will guarantee that I am fixing
the contradiction between the highest order clauses.

There are three rules for "fixing" a contradiction.
The first rule is fairly simple.

The Addition Rule:
When there is contradiction between two clauses,
increment the lower order clause.

Start by assuming the 0'th element of every clause
is true:

z0,y0,x0,w0,v0 = True

The first contradiction in the list is (~v0+~y0).
Since v0 is lower order, I increment v0 to v1.
I want to remember why I set v1 when I backtrack,
so I add the conditional: y0->v1.

z0,y0,x0,w0,v1 = True; y0->v1

The first contradiction for this new assignment:
(~v1+~x0)
Increment v1 to v2 and add (x0&y0)->v2.

z0,y0,x0,w0,v2 = True; y0->v1, (x0&y0)->v2
(~v2+~z0)

The assignment (x0&y0&z0) -> contradiction.
I can no longer use the Addition rule
because I can't increment v2.

Now I must backtrack with the "Carry" rule.

The Carry Rule:
If the lower order clause can't be incremented,
then find the lowest order clause variable that
implicates the contradiction and increment it.

Remove all conditionals that rely on the
incremented clause literal. Add a conditional
for the other two clause variables and
the new increment clause variable.

In the example, (x0&y0&z0) causes the contradiction.
The carry rule says to increment x0 to x1 and remove
all conditionals that depend on x0.
(x0&y0)->v2 is removed, but y0->v1 is not.

Now I add the conditional: (y0&z0)->x1.

z0,y0,x1,w0,v1 = True; y0->v1, (y0&z0)->x1

There are no more contradictions and this is
a satisfying clause assignment.

z0 = ~c
y0 = ~a
x1 = d
w0 = ~a
v1 = b

~a,b,~c,d = True

(a+B+c)(~A+~b+~c)(~b+D+e)(~A+~c+~e)(~C+~d+e)

I have to add a "Double Carry" rule.
Astute observers will notice that the Carry rule
can never increment the two highest order clauses.

The Double Carry Rule
If the lower order literal in the contradiction
can't be incremented, and the lowest order literal
that implies the contradiction can't be incremented,
then increment the lowest order implying literal that
can be incremented. Remove all dependent implications
and add an implication with all literals that weren't
incremented.

If none of the implicating literals can be incremented
the instance is unsolvable.

For example, assume:

z0,y0,x2,w0,v2 = True; y0->v1, (x2&y0)->v2, z0->x1, (y0&z0)->x2

If I have a contradiction like (~y0+~v2) then
I get the contradiction (x2&y0&z0)-> carry.
But, I can't increment x2, so, I must increment
y0 to y1 and add the implication z0->y1.

The double carry rule is the only way clauses Y and Z
can be incremented. Increments to the Z clause are
unconditional. A backtrack can never decrement Z.
Other clauses might be decremented when conditionals
are removed.



Russell
- 2 many 2 count

I made a mistake. Several, in fact.

I won't correct the errors in the example.
You should try working the problem out
yourself to find those mistakes.

But, I do need to extend the Double Carry rule.

With this method, it is very important that I
don't "skip" possible satisfying clause assignments.

When there is a contradiction, I must increment
the lowest order clause that will remove the
contradiction.

The Double Carry rule is correct for the
example I gave, but there are situations
where it can increment the wrong clause.

Assume I have the clause V,W,X,Y, and Z.
The current clause assignment and conditionals are:

z0,y0,x0,w2,v2 = T
w2->v1, (w2&z0)->v2, z0->w1, (x0&z0)->w2

Assume the instance has the clause (~y0+~v2).
This means (w2&y0&z0) -> contradiction.

We can't increment w2.
The old Double Carry rule says to increment y0.

Look at the conditional (x0&z0)->w2.

I can fix the contradiction (w2&y0&z0) by
incrementing x0. Since x0 is lower order
than y0, I increment x0.
I remove all the conditionals for x0 and w2
and add the conditional (y0&z0)->x1

z0,y0,x1,w1,v2 = T
z0->w1, (y0&z0)->x1


Russell
- 2 many 2 count

On Aug 14, 8:22*pm, reaste...@gmail.com wrote:

> Assume I have the clause V,W,X,Y, and Z.
> The current clause assignment and conditionals are:
>
> z0,y0,x0,w2,v2 = T
> w2->v1, (w2&z0)->v2, z0->w1, (x0&z0)->w2
>
> Assume the instance has the clause (~y0+~v2).
> This means (w2&y0&z0) -> contradiction.
>
> We can't increment w2.
> The old Double Carry rule says to increment y0.
>
> Look at the conditional (x0&z0)->w2.
>
> I can fix the contradiction (w2&y0&z0) by
> incrementing x0. Since x0 is lower order
> than y0, I increment x0.
> I remove all the conditionals for x0 and w2
> and add the conditional (y0&z0)->x1

> z0,y0,x1,w1,v2 = T
> z0->w1, (y0&z0)->x1

z0,y0,x1,w1,v0 = T
z0->w1, (y0&z0)->x1