3SAT - Partial Resolution in Parallel
RussellE
on creating SAT solvers that make use
of multiple processors.
I show how Partial Resolution can
partitioned among several processes
such that each process helps other
processes find a satisfying assignment.
This is accomplished by sharing
resolvent clauses. Resolvent clauses
are also called learning clauses.
Each process is randomly assigned
a resolution order and a parity.
Resolution order is just an ordering
of the variables. For simplicity,
this example will use lexographic order.
Parity determines if the process
assumes unassigned variables are True
or they are False.
For this example, I will use two
processes. The first will assume
unassigned variables are False
and the second process will assume
unassigned variables are True.
Each process has the following steps:
1) Assign the highest order unassigned
variable to False (True)
2) Record and propagate all unit clauses.
3) Resolve contradictions.
Assume I am given this 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)
Resolution order:
abcde
All processes start assuming all
variables are unassigned.
Start the first process.
Assign highest order unassigned variable to false:
~e
There are no unit clauses or contradictions.
Repeat step 1:
~e~d
Unit clauses:
(C+d+e)
(B+d+e)
Propagate these unit clauses:
~e~dcb
Unsatisfied clause:
(~b+~c+d)
I will use resolution to resolve
the contradiction.
Start with the clause (or clauses)
that cause the contradiction and
resolve that clause with the lowest
order unit clause.
(~b+~c+d) causes the contradiction.
The lowest order literal is ~b.
(b+d+e) forced b to be True.
Resolve (~b+~c+d) and (b+d+e).
(~b+~c+d)(b+d+e) resolves to (~c+d+e)
I want to keep resolving this clause
with the recorded unit clauses until
I have a resolvent clause where all
literals are positive (negative).
(~c+d+e)(c+d+e) resolves to (d+e)
Add resolvent clause (d+e) to our expression.
While the first process is finding the
resolvent clause (d+e), the second process
will be running.
Assign highest order variable true:
ed
Unit clauses:
(~C+~d+~e)
(C+~d+~e)
(~B+~d+~e)
(~c+~d+~e)(c+~d+~e) is a contradiction.
(~c+~d+~e)(c+~d+~e) resolves to (~d+~e)
Add resolvent clause (~d+~e).
Now, both processes have found a resolvent clause.
Adding both learning clauses to the 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)
(d+e)(~d+~e)
A common problem with SAT solvers
that use learning clauses is controlling
the number of learning clauses.
I can identify which resolvent clauses
are contributing to finding a solution
and I can remove resolvent clauses
that are no longer needed.
This method requires storing no more
than N times P resolvent clauses
at any one time. N is the number
of variables and P is the number
of processes.
A resolvent clause is retained if and
only if it is a unit clause in
some process.
We now restart both processes with
the new instance.
Assign highest order variable false:
~e
Unit clauses:
(D+e)*
* I will retain this resolvent clause
because it is a unit clause for this process.
~ed
(C+~d+e)
~edc
(B+~c+e)(~B+~c+~d)
These two clauses cause a contradiction.
(b+~c+e)(~b+~c+~d) resolves to (~c+~d+e)
(~c+~d+e)(c+~d+e) resolves to (~d+e)
(~d+e)(d+e) resolves to (e)
Add (e) as a resolvent clause.
The other process.
Assign highest order variable true:
e
Unit clauses:
(~D+~e)*
e~d
(~C+d+~e)
e~d~c
(~B+c+~e)
e~d~c~b
(A+b+c)(~A+b+c)
Resolve the contradiction:
(a+b+c)(~a+b+c) resolves to (b+c)
(b+c)(~b+c+~e) resolves to (c+~e)
(c+~e)(~c+d+~e) resolves to (d+~e)
(d+~e)(~d+~e) resolves to (~e)
We now have a certificate of unsatisfiabiliy,
a proof the empty clause is a resolvent clause:
(~b+~c+d)(b+d+e) -> (~c+d+e)
(~c+d+e)(c+d+e) -> (d+e)
(~c+~d+~e)(c+~d+~e) -> (~d+~e)
(b+~c+e)(~b+~c+~d) -> (~c+~d+e)
(~c+~d+e)(c+~d+e) -> (~d+e)
(~d+e)(d+e) -> (e)
(a+b+c)(~a+b+c) -> (b+c)
(b+c)(~b+c+~e) -> (c+~e)
(c+~e)(~c+d+~e) -> (d+~e)
(d+~e)(~d+~e) -> (~e)
(e)(~e) -> ()
Other processes would use different
resolution orders and parities.
Russell
- 2 many 2 count
MeAmI.org
P to solve on parallel computers [...] PCP, Probabilistically
Checkable Proof [...] .... proof, establishing that 3-SAT could be
reduced to 2SAT in O(n3) ...
http://groups.google.com/group/sci.logic/browse_thread/thread/b2ca736de875d27a/e1919ca15bef78f8