Investigations regarding extended resolution for pigeonhole clausesets.
More...
Go to the source code of this file.
Detailed Description
Investigations regarding extended resolution for pigeonhole clausesets.
 Todo:
 Sat solvers on xxtended PHP clausesets

The standardised extended clauseset is weak_php_unsat_ext_stdfcs(N), which is output by output_weak_php_unsat_ext_stdname(n).

Performance of SAT solvers (n is the number of holes):

First impression with cryptominisat (csltok with 2.0 GHz):
n=10
18.65s
n=11
38.64s
n=12
249.72s
n=13
886.28s
n=14
13187.05s
# with n=14 worse than PHP itself

The other solvers seem to perform worse (and also not better than their PHPperformance). Though one needs to see complete data.

So apparently no solver can make use of the extension. This seems understandable, given the complicated nature of the resolution proof for the extension  all clauses have to be used, in a special order.
 Todo:
 Hardness

The hardness of weak_php_fcs(m,m1) vs weak_php_unsat_ext_fcs(m):
maxima> for m : 1 while true do
print([hardness_wpi_cs(weak_php_fcs(m,m1)[2],{{}}),
hardness_wpi_cs(weak_php_unsat_ext_fcs(m)[2],{{}})])$
[0,0]
[1,1]
[2,2]
[3,3]
[4,4]

weak_php_unsat_ext_fcs(m) has a polynomial size resolution proof. However, what is the complexity of the smallest tree resolution proof?
 Todo:
 Analysis of blocking structure

Computing the number of blocked 2clauses which can be removed:
experiment(n) := for i : 0 thru n do block([P:weak_php_cs(i+1,i),E:weak_php_unsat_ext_fcs(i)[2],R,R2], R:elim_blocked_cs(E), R2:elim_blockedk_cs(E,2), print(i, length(P), length(E), length(R), length(R2), length(E)length(R2)));
experiment(7);
0 1 1 1 1 0
1 3 3 3 3 0
2 9 17 9 15 2
3 22 54 22 49 5
4 45 125 45 116 9
5 81 241 81 227 14
6 133 413 133 393 20
7 204 652 204 625 27

So it seems the number of removable blocked 2clauses is n*(n+1)/21.

The question is whether after removal of the blocked 2clauses still an exponential resolution lowerbound can be shown?!

One needs to determine which clauses are removed.

For this the generator in ComputerAlgebra/Satisfiability/Lisp/Generators/Pigeonhole.mac needs to be given more structure (and better documentation).

Perhaps the extension should be standardised in the sense that only extension via {v,a,b},{v,a},{v,b} is used? Perhaps then removal of blocked 2clauses becomes more powerful?
Definition in file ExtendedResolution.hpp.