Prev: 1.Asku algorithm
Next: Are there recommended books on computational geometry and polyhedral combinatoris?
From: RussellE on 21 Dec 2009 04:18
I describe a method for solving the
Boolean Satisfiabilty (SAT) problem
using a network of connected processes.

I previously posted a resolution
based backtracking algorithm for
parallel processors.
http://groups.google.com/group/comp.theory/browse_thread/thread/e01c2984cfced459/fa0966d4e3d70488

Now, I show how a large SAT instance
can be broken into smaller, more managable
partitions.

Assume we have a large SAT instance.
We don't want to send such a large amount
of data to every process. What if we
could have each process work on a
small piece of the SAT instance?

Well, we can.

Assume each variable in the instance
is assigned a position in a binary number.
Any satisfying assignment can be
represented as a binary number.
Any instance with a satisfying assignment
has a lowest numbered satisfying assignment.

Send each process a subset of the original problem.
The process finds the lowest numbered satisfying
assignment for the partition of clauses it has been given.

The lowest numbered assignment for the entire
SAT instance can't be lower than the lowest
assignment for any partition.

Each process tells a central process the
lowest satisfying assignment for its partition.
The partition with the highest number wins.
This is the new lower bound for the lowest
assignment of the entire instance.

Each process takes this new lower bound and searches
for a new lower bound for its partition that is
greater than or equal to the current best lower bound.
A satisfying assignment has been found if all
partitions are satisfied with the current lowest bound.
The instance is unsatisfiable if the lowest
bound is forced to be greater than all variables true.

I won't actually be passing large binary numbers around.
Instead, I will use "resolution equivalence".

Two SAT instances are resolution equivalent
if they have the same lowest numbered satisfying
assignment with respect to some variable ordering.

For example, the instance (a) is resolution equivalent
to instance (a+b+c)(~a+~b+~c) because ~c~ba is the
lowest numbered satisfying assignment for both instances.

If an instance with N variables has a satisfying assignment,
there exists a resolution equivalent instance with
N or fewer clauses.

The simplest example would be a set of unit clauses,
one for each true variable in the satisfying assignment.

I will send each process a set of no more than
one clause per variable to force a minimum assignment.

I call this set of resolution equivalent clauses
the "primary" clauses. A primary clause has all
positive literals. There can be no more than one
primary clause for each variable. The only time a
primary clause is replaced is if a clause with higher order
variables is derived for that variable by some process.

For example, if (a+b+c) is a primary clause
for variable a, it will only be replaced with
a clause having fewer or higher order variables
(and lowest order literal a). A clause like (a+e).

Since primary clauses can be resolvent clauses,
they can get rather large. Of course,
no clause will have more then N variables.


Assume I am given the following instance:

(a+b+c)(~a+c+~d)(~b+c+~e)(~b+~d+~e)
(b+d+e)(~c+~d+~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)(a+b+d)

I break this instance into two partitions.
It doesn't matter if partitions share clauses.
It is important for every clause in the
original instance to be in some partition.

Partition 1:
(a+b+c)(~a+c+~d)(~b+c+~e)(~b+~d+~e)
(b+d+e)(~c+~d+~e)(c+~d+~e)

Partition 2:
(c+d+e)(~b+~c+d)(b+c+~d)(c+~d+e)
(~b+~c+~d)(~a+b+c)(~c+d+~e)(a+b+d)

My initial list of primary clauses are the
clauses with all positive literals.

Initial Primary Clauses:
(a+b+c)(a+b+d)(b+d+e)(c+d+e)

We don't need more than one clause per lowest order variable.
(a+b+c) and (a+b+d) both have the same lowest order variable.
Always choose the clause with highest order variables.
In this example, keep (a+b+d) and eliminate (a+b+c).

Initial Primary Clauses:
(a+b+d)(b+d+e)(c+d+e)
Lowest satisfying assignment: ~e~dcb~a

Now, check if this lowest assignment for the
primary clauses is also the lowest assignment
for each partition.

Combine the partition with the primary clauses.

Combined Partition 1:
(a+b+d)(b+d+e)(c+d+e)
(a+b+c)(~a+c+~d)(~b+c+~e)(~b+~d+~e)
((b+d+e))(~c+~d+~e)(c+~d+~e)

Notice (b+d+e) is a primary clause and is in this partition.
A primary clause is always considered to be a primary clause,
even if it is in the current partition.

Steps to find the lowest numbered satisfying assignment.

1) Assume the highest ordered unassigned variable is false.
2) Mark and propagate all unit clauses.
3) Resolve any conflicts.

Repeat this process until a conflict is found
or all clauses are satisfied.

Partition 1:
(a+b+d)(b+d+e)(c+d+e)
(a+b+c)(~a+c+~d)(~b+c+~e)(~b+~d+~e)
((b+d+e))(~c+~d+~e)(c+~d+~e)

We start by assuming ~e. This doesn't create
a unit clause, so we repeat step (1).
Assuming ~e~d forces two primary clauses
into unit clauses: (b+d+e)(c+d+e)

We mark (b+d+e)(c+d+e) and propogate the assignment cb.
~e~dcb~a is the lowest satisfying assignment for partition 1.

All of the marked clauses are primary clauses.
The current lowest bound is consistent with partition 1.

Combine the primary clauses with partition 2.

Combined Partition 2:
(a+b+d)(b+d+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)((a+b+d))

Once again, we get the assignment ~e~dbc,
but clause (~b+~c+d) causes a contradiction.

Resolve the contradiction clause
with the marked clauses until
a clause of all positive literals
is derived.

Start with the lowest order negated
literal in the contradictory clause.

Contradictory clause: (~b+~c+d)
Marked clauses: (b+d+e)(c+d+e)

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

Return (d+e) as a new primary clause.

New Primary Clauses:
(a+b+d)(b+d+e)(c+d+e)(d+e)
lowest assignment: ~ed~c~b~a

Combine the new primary clauses with partition 1.

Partition 1:
(a+b+d)(b+d+e)(c+d+e)(d+e)
(a+b+c)(~a+c+~d)(~b+c+~e)(~b+~d+~e)
((b+d+e))(~c+~d+~e)(c+~d+~e)

~ed~cb~a is the lowest assignment.
Notice b is false in the primary lower bound.
We need a primary clause for variable b.

Marked clauses: (d+e)(~a+c+~d)(a+b+c).

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

Return (b+c+e) as a primary clause.

Partition 2:
(a+b+d)(b+d+e)(c+d+e)(d+e)
((c+d+e))(~b+~c+d)(b+c+~d)(c+~d+e)
(~b+~c+~d)(~a+b+c)(~c+d+~e)((a+b+d))

~edc~b~a is the lowest assignment.
Marked clauses: (d+e)(c+~d+e)(~b+~c+~d).

(c+~d+e) forces c to be true, so we need
a primary clause for variable c.
Start with the lowest negated literal in
(c+~d+e), ~d:

(c+~d+e)r(d+e) -> (c+e).
Return (c+e) as a new primary clause.

Primary clause (b+d+e) is not replaced by (b+c+e).
Primary clause (c+d+e) is replaced by (c+e).

New Primary Clauses:
(a+b+d)(b+d+e)(c+e)(d+e)
lowest assignment: ~edc~b~a

This set of primary clauses is
consistent with both partitions and
has the same lowest numbered satisfying
assignment as the original instance:

(a+b+C)(~A+C+~d)(~B+C+~E)(~B+~d+~E)
(b+D+e)(~c+~d+~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)(a+b+D)


Russell
- 2 many 2 count
 | 
Pages: 1
Prev: 1.Asku algorithm
Next: Are there recommended books on computational geometry and polyhedral combinatoris?