Prev: Last CFP - Applied Computing 2010: 3 September 2010
Next: Pole Balancing Applet
From: RussellE on 8 Aug 2010 20:17
A partitioning solver can produce shorter
refutations of the pigeonhole problem than
resolution based solvers.

Partitioning solvers repeatedly partition
SAT instances until a solution is found
or all partitions are exhausted.
A refutation consists of a list of
partitions containing contradictions.

Simple Partitioning Solver:

1) Choose the lowest order 2-clause
2) Push possible assignments on stack
3) Pop partition from stack
4) Propogate partition assignment
5) If Contradiction go to 3
6) go to 1

The process ends if a satisfying
assignment is found or all partitions
are removed from the stack.

This is a pigeonhole problem with
four pigeons and three holes:

(a+b+c)(d+e+f)(g+h+i)(j+k+l)
(~a+~d)(~a+~g)(~a+~j)(~d+~g)(~d+~j)(~g+~j)
(~b+~e)(~b+~h)(~b+~k)(~e+~h)(~e+~k)(~h+~k)
(~c+~f)(~c+~i)(~c+~l)(~f+~i)(~f+~l)(~i+~l)

Choose the lowest order 2-clause:
(~a+~d)

The partition of variables, [A,B], has three
possible satisfying assignments. Push these
partition assignments on the partition stack:

Partition Stack:
~a~d, ~ad, a~d

Pop an assignment from the stack and
propogate the assignment.

a~d ->
(e+f)(h+i)(k+l)
(~g)(~j)
(~b+~e)(~b+~h)(~b+~k)(~e+~h)(~e+~k)(~h+~k)
(~c+~f)(~c+~i)(~c+~l)(~f+~i)(~f+~l)(~i+~l)

Choose lowest order 2-clause:
(~b+~e)

Push the three possible assignments on the stack.

Partition Stack:
~a~d, ~ad, a~b~d~e, a~b~de, ab~d~e

Pop ab~d~e from the stack.
ab~d~e -> () contradiction

Pop a~b~de from the stack.
a~b~de -> () contradiction

Pop a~b~d~e from the stack.
a~b~d~e -> () contradiction

Partition Stack:
~a~d, ~ad

~ad ->
(b+c)(h+i)(k+l)
(~g)(~j)
(~b+~e)(~b+~h)(~b+~k)(~e+~h)(~e+~k)(~h+~k)
(~c+~f)(~c+~i)(~c+~l)(~f+~i)(~f+~l)(~i+~l)

Choose lowest order 2-clause:
(b+c)

Partition Stack:
~a~d, ~abcd, ~a~bcd, ~ab~cd

Once again, the last three assignments
on the stack lead to contradiction.
The only partition left is ~a~d which
also leads to contradiction when combined
with (b+c).

We now have a short refutation proof:

Refutation:

(~a+~d) a~d, (~b+~e) b~e -> ()
(~a+~d) a~d, (~b+~e) ~be -> ()
(~a+~d) a~d, (~b+~e) ~b~e -> ()
(~a+~d) ~ad, (b+c) bc -> ()
(~a+~d) ~ad, (b+c) ~bc -> ()
(~a+~d) ~ad, (b+c) b~c -> ()
(~a+~d) ~a~d, (b+c) bc -> ()
(~a+~d) ~a~d, (b+c) ~bc -> ()
(~a+~d) ~a~d, (b+c) b~c -> ()

The format of this refutation is a list of
assignments that lead to contradiction.
The size of the list is reduced by including
partition clauses. Partition clauses restrain
the number of possible assignments.

The validity of this refutation can be checked
in a polynomial number of steps.


Russell
- 2 many 2 count
 | 
Pages: 1
Prev: Last CFP - Applied Computing 2010: 3 September 2010
Next: Pole Balancing Applet