3SAT - CloudSat 2
- From: RussellE <reasterly@xxxxxxxxx>
- Date: Mon, 18 Jan 2010 00:11:23 -0800 (PST)
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:
There are six combinations of three variables
that contain clauses:
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
We now have three Partial Variable Assignments (PVA).
Assume we have a push down stack.
Push these three PVA's onto the stack:
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
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
(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:
We find the variable combination "ab"
has no satisfying assignments:
The stack is now empty and we have
proven the original 3SAT instance
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.
- 2 many 2 count