OKlibrary  0.2.1.6
Pigeonhole.hpp File Reference

Plans for Maxima-generators of pigeonhole formulas. More...

Go to the source code of this file.


Detailed Description

Plans for Maxima-generators of pigeonhole formulas.

Todo:
Standard variable ordering for extended-pigeon-hole formulas
  • For the extended pigeon-hole 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, l-1) + (i-1) * 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
      l^3/3+1*l-4*l/3+1 <= m,
           
      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 closed-form equation
      (sqrt(243*t^2-486*t+239)/(2*3^(3/2))+(3*t-3)/2)^(1/3)
        +1/(3*(sqrt(243*t^2-486*t+239)/(2*3^(3/2))+(3*t-3)/2)^(1/3)))
           
      is then the real-valued solution from
      solve(l^3/3+l-4*l/3+1 = t, l).
           
  • A problem with the inversion is that:
    1. solve(l^3/3+l-4*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.
    2. The closed-form expression
      (sqrt(243*t^2-486*t+239)/(2*3^(3/2))+(3*t-3)/2)^(1/3)
        +1/(3*(sqrt(243*t^2-486*t+239)/(2*3^(3/2))+(3*t-3)/2)^(1/3)))
           
      is the real-valued solution to solve(l^3/3+l-4*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^2-486*t+239)/(2*3^(3/2))+(3*t-3)/2)^(1/3)
        +1/(3*(sqrt(243*t^2-486*t+239)/(2*3^(3/2))+(3*t-3)/2)^(1/3)))), t: 71);
       5
           
      Float is needed here to force the simplification of the term.
    3. 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.
    4. The current solution should be reconsidered, and a better method found.
Todo:
Update the php-functions
  • All functions need to be based on the list-forms ("fcl" etc.), not on the set-form (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 clause-set for the (weak) SAT translation of PHP is given by weak_php_fcs(m,n).
  • The clause-set 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:
      1. assume for the sake of contradiction we have an injective map from {1,...,n+1} to {1,...,n};
      2. we can then produce an injective map phi_n from {1,...,n} to {1,...,n-1} from phi;
      3. For a map phi : {1,...,n+1} -> {1,...,n}, the map phi_n : {1,...,n} -> {1,...,n-1} is defined as:
        phi_n(i) = phi(i) if phi(i) # n
                   phi(n+1) if phi(i) = n
               
      4. 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_(m-1), phi_(m-2), ..., 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,...,n-1}, i maps to j.
  • Clauses are then added to define phi_n for each n in {1,...,m-1}, based on phi_(n+1).
  • For each n in {1,...,m-1}, F_n is the union over i in {1,...,n-1} and j in {1,...,n-2} 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,...,m-1}.
  • The clause-set union(weak_php_fcs(m+1,m),F_S) then has a polynomial size resolution proof.
  • Construction of the resolution proof:
    1. First a representation of resolution proofs is needed. This is discussed in "Resolution proofs" in ComputerAlgebra/Satisfiability/Lisp/Resolution/plans/general.hpp.
    2. Labelled trees are a reasonable starting point, and are already there.
    3. Those trees which represent dag-like structures must have identical subtrees where clauses are "reused".
    4. The notions (and tools) for such presentations of resolution proofs of course go to module Resolution.
    5. A first tool is a correctness-checker.
    6. Once this has been established, the short resolution refutations of PHP have to be implemented.
    7. 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 pigeon-hole 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.