Plans for Maximagenerators of pigeonhole formulas.
More...
Go to the source code of this file.
Detailed Description
Plans for Maximagenerators of pigeonhole formulas.
 Todo:
 Standard variable ordering for extendedpigeonhole formulas

For the extended pigeonhole formulas with m holes, we have variables of the form php_ext(l,i,j) for 1 <= l <= m, 1 <= i <= l+1, 1 <= j <= l.

The natural ordering is the lexicographical order on NN x {1,...,l+1} x {1,...,l}. This has the nice property that the ordering doesn't depend on m.

The standardisation then simply maps php_ext(l,i,j) to sum((lp+1) * lp, lp, 1, l1) + (i1) * l + j.

Computing the inverse of
m = (l^3  4*l)/3 + i*l + j
where 1 <= l, 1 <= i <= l+1, 1 <= j <= l.

We first compute l, by computing the maximum integer l such that that is, substituting i < 1 and j < 1.

So we solve for l' in (l')^3/3+(l')4*(l')/3+1 = m and take the floor to get such a maximum l.

The closedform equation
(sqrt(243*t^2486*t+239)/(2*3^(3/2))+(3*t3)/2)^(1/3)
+1/(3*(sqrt(243*t^2486*t+239)/(2*3^(3/2))+(3*t3)/2)^(1/3)))
is then the realvalued solution from solve(l^3/3+l4*l/3+1 = t, l).

A problem with the inversion is that:

solve(l^3/3+l4*l/3+1 = t, l) computes the correct value for l if we substitute a particular value for t. However, it also computes imaginary solutions, and it isn't clear from the Maxima documentation how to reliably extract only the real solution.

The closedform expression
(sqrt(243*t^2486*t+239)/(2*3^(3/2))+(3*t3)/2)^(1/3)
+1/(3*(sqrt(243*t^2486*t+239)/(2*3^(3/2))+(3*t3)/2)^(1/3)))
is the realvalued solution to solve(l^3/3+l4*l/3+1 = t, l), but when t = 71, rounding errors mean we get l = 5 instead of l = 6: ev(float(floor((sqrt(243*t^2486*t+239)/(2*3^(3/2))+(3*t3)/2)^(1/3)
+1/(3*(sqrt(243*t^2486*t+239)/(2*3^(3/2))+(3*t3)/2)^(1/3)))), t: 71);
5
Float is needed here to force the simplification of the term.

The current solution, in invstandardise_weak_php_unsat_ext_uni, is to iteratively search for l from l = 1. This is then linear complexity in l.

The current solution should be reconsidered, and a better method found.
 Todo:
 Update the phpfunctions

All functions need to be based on the listforms ("fcl" etc.), not on the setform (this is then derived).

At the same time, we should add tests for all these functions (we don't have tests for weak_php_fcs etc).
 Todo:
 Extended Resolution clauses for the Pigeon Hole Principle

See [A short proof of the pigeon hole principle using Extended Resolution; Stephen Cook].

See weak_php_fcs in ComputerAlgebra/Satisfiability/Lisp/Generators/Generators.mac.

Consider positive integers m and n, and Pigeon Hole Principle (PHP) for m pigeons and n holes.

That is, consider the decision problem: is there an injective map from {1,...,m} to {1,...,n}?

The clauseset for the (weak) SAT translation of PHP is given by weak_php_fcs(m,n).

The clauseset weak_php_fcs(m+1,m) has only exponential size resolution proofs. Investigations started with [The intractability of resolution; Armin Haken].

In [A short proof of the pigeon hole principle using Extended Resolution; Stephen Cook], Cook shows that there is a polynomial size Extended Resolution proof of weak_php_fcs(m+1,m).

That is, Cook defines a set of new variables V_S and a set of clauses F_S which when added to weak_php_fcs(m,n), has a polynomial size resolution proof.

The fact that there is no injective map from {1,...,m+1} into {1,...,m} can be proven by induction:

Base case: there is no map from {1} into {}, as there are no maps into {}.

Induction hypothesis: for all n' < n, there is no map from {1,...,n'+1} into {1,...,n'}.

Induction Step:

assume for the sake of contradiction we have an injective map from {1,...,n+1} to {1,...,n};

we can then produce an injective map phi_n from {1,...,n} to {1,...,n1} from phi;

For a map phi : {1,...,n+1} > {1,...,n}, the map phi_n : {1,...,n} > {1,...,n1} is defined as:
phi_n(i) = phi(i) if phi(i) # n
phi(n+1) if phi(i) = n

by the induction hypothesis, this is a contradiction.

If one could find such a phi then expanding the induction steps of the proof, one would get a series of maps: phi, phi_m, phi_(m1), phi_(m2), ..., phi_2, phi_1, each defined in terms of the last.

Cook encodes the induction proof as an Extended Resolution proof by introducing new variables php_ext(n,i,j) for n, j in {1,...,m} and i in {1,...,m+1}.

php_ext(n,i,j) encodes that in the map phi_n : {1,...,n} > {1,...,n1}, i maps to j.

Clauses are then added to define phi_n for each n in {1,...,m1}, based on phi_(n+1).

For each n in {1,...,m1}, F_n is the union over i in {1,...,n1} and j in {1,...,n2} of the set of prime implicates of the relation php_ext(n,i,j) <=> (php_ext(n+1, i,j) or (php_ext(n+1,i,n) and php_ext(n+1,n+1,j))). </li

In the case where n = m  1, we have php_ext(n+1,i,j) = php(i,j) for all i and j.

F_S is then the union of F_n for all n in {1,...,m1}.

The clauseset union(weak_php_fcs(m+1,m),F_S) then has a polynomial size resolution proof.

Construction of the resolution proof:

First a representation of resolution proofs is needed. This is discussed in "Resolution proofs" in ComputerAlgebra/Satisfiability/Lisp/Resolution/plans/general.hpp.

Labelled trees are a reasonable starting point, and are already there.

Those trees which represent daglike structures must have identical subtrees where clauses are "reused".

The notions (and tools) for such presentations of resolution proofs of course go to module Resolution.

A first tool is a correctnesschecker.

Once this has been established, the short resolution refutations of PHP have to be implemented.

This is the only way that we can check correctness of the ER clauses!

See weak_php_unsat_ext_fcs in ComputerAlgebra/Satisfiability/Lisp/Generators/Generators.mac for the generator of the weak pigeonhole principle with the extended resolution clauses.

See also "Hardness of boolean function representations" in Experimentation/Investigations/BooleanFunctions/plans/general.hpp.
 Todo:
 DONE Add tests for weak_php_ext_fcs

DONE Tests are needed for:

DONE weak_php_unsat_ext_fcs;

DONE php_induction_cl;

DONE php_induction_step_cl.
Definition in file Pigeonhole.hpp.