# 3SAT - CloudSat 2

*From*: RussellE <reasterly@xxxxxxxxx>*Date*: Mon, 18 Jan 2010 00:11:23 -0800 (PST)

CloudSat 2

I describe a method of repeatedly partioning

a 3SAT instance until a satisfying assignment

is found or all partitions are searched.

A simple way to partition a 3SAT instance

is to choose a variable, A, and create one

partition where A is assumed to be true and

another partition where A is assumed false.

We can create more partitions by branching

on more than one variable. Branching on

two variables creates four partitions,

branching on three variables creates

eight paritions, etc.

We can reduce the number of partitions

we create by choosing the right variables

to branch on.

This method branches on sets of three

variables at a time. We will be choosing

sets of three variables that appear

together in clauses.

Assume we have the following 3SAT instance:

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

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

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

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

There are six combinations of three variables

that contain clauses:

abc: (a+b+c)(~a+b+c)

acd: (~a+c+~d)

bce: (~b+c+~e)(b+~c+e)

bde: (~b+~d+~e)(b+d+e)

cde: (~c+~d+~e)(c+~d+~e)(c+d+e)(c+~d+e)(~c+d+~e)

bcd: (~b+~c+d)(b+c+~d)(~b+~c+~d)

We want the combination with the fewest number

of satisfying assignments. Each clause removes

one of the eight possble assignments.

The combination "cde" has five clauses or

2^3 - 5 = 3 satisfying assingments:

Satisfying assignments for

(~c+~d+~e)(c+~d+~e)(c+d+e)(c+~d+e)(~c+d+~e)

cde: c~d~e,cd~e,~c~de

We now have three Partial Variable Assignments (PVA).

Assume we have a push down stack.

Push these three PVA's onto the stack:

c~d~e

cd~e

~c~de

These are the basic operations of the partition solver:

1) Pop the top PVA from the stack.

2) If the stack is empty and this is not

the first pass, the original 3SAT instance

is unsatisfiable.

3) Reduce the original 3SAT instance

using the PVA.

4) Propagate all unit clauses.

5) If a contradiction is found go to step 1.

6) Find the three variable combination with

the fewest number of satisfying assignments.

7) Find all satisfying assignments for the

clauses containing only these three variables.

8) Push these (up to 7) PVA's (including propogated

variable assignments) onto the stack.

9) Go to step 1

Applying this procedure to the example,

we first pop the PVA c~d~e from the stack.

Reducing the original expression with

this variable assignment, we quickly find

a contradiction:

(c)(~d)(~e)(b+d+e)(~b+~c+d) -> (b)(~b)

We pop the next PVA: cd~e

This PVA also causes a contradiction.

(c)(d)(~e)(b+~c+e)(~b+~c+~d) -> (b)(~b)

The last PVA on the stack is ~c~de:

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

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

We find the variable combination "ab"

has no satisfying assignments:

ab: (a+b)(~b)(~a+b)

The stack is now empty and we have

proven the original 3SAT instance

is unsatisfiable.

Notice, we only needed to evaluate

three partial variable assignments.

This method would be impractical if the

size of the stack grew exponentially.

Analysis shows the stack will grow

to a maximum size and then remain

relatively constant. The maximum

size of the stack is linearly

proportional to the number of variables.

Assume worse case: each process finds

seven new partial assignments.

We initially push 7 PVA's of 3 variables

onto the stack. We pop one of these

3-variable PVA's from the stack and

push 7 more PVA with 6 variables.

Each iteration adds at least three

more variables to the assignment.

This iteration process must end when

all variables are assigned. There

can be, at most, N/3 iterations

(where N is the number of variables).

We now have 6 PVA's of 3 variables,

6 PVA's of 6 variables, etc.

At this point there are no more than

6*N/3 = 2N PVA's on the stack.

When all the variables are assigned,

we will either find a satisfying assignment,

and we are are done, or we find a contradiction.

Each contradiction removes one PVA from the stack.

Assume we find all (N-3) variable PVA's

are contradictary. We then pop a (N-6)

variable PVA and generate 7 new (N-3) PVA's.

This shows the stack size will remain

relatively constant until a solution is found

or all PVA's are removed from the stack.

In a multi-processor environment we can assume

each simultaneous process will add 2N PVA's

to the stack. The maximum stack size will be

on the order of 2*P*N where P is the number

of processors and N is the number of variables.

We can easily branch on more than three

variables at a time. For example, we can

take the eight most common unassigned

variables, create the set of all clauses

containing only these eight variables,

then try all 256 possible assignments.

Each new satisfying PVA is pushed on

the stack. Branching on more variables

will increase the maximum size of the

stack, but the maximum size will still

be linear with respect to number of variables.

Russell

- 2 many 2 count

.

- Prev by Date:
**Re: How did the Internet come about?** - Next by Date:
**Re: Help: sanity-review regex equivalence.** - Previous by thread:
**NOW Watch ***y Star Aishwarya rai <***> Bathing Videos In All Angles .** - Next by thread:
**Formalism** - Index(es):