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 2clause 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 2clause: (~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 2clause: (~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 2clause: (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 