OKlibrary  0.2.1.6
Pigeonhole.mac
Go to the documentation of this file.
00001 /* Matthew Gwynne, 26.8.2011 (Swansea) */
00002 /* Copyright 2011, 2012, 2013 Oliver Kullmann
00003 This file is part of the OKlibrary. OKlibrary is free software; you can redistribute
00004 it and/or modify it under the terms of the GNU General Public License as published by
00005 the Free Software Foundation and included in this library; either version 3 of the
00006 License, or any later version. */
00007 
00022 oklib_include("OKlib/ComputerAlgebra/DataStructures/Lisp/Lists.mac")$
00023 oklib_include("OKlib/ComputerAlgebra/DataStructures/Lisp/HashMaps.mac")$
00024 oklib_include("OKlib/ComputerAlgebra/Satisfiability/Lisp/ClauseSets/BasicOperations.mac")$
00025 oklib_include("OKlib/ComputerAlgebra/Satisfiability/Lisp/ClauseSets/Substitutions.mac")$
00026 
00027 
00028 
00029 /* ************************
00030    * Pigeon-hole formulas *
00031    ************************
00032 */
00033 
00034 /* TODO: The following needs to be updated, so that the list-forms
00035    are the basic forms, and the set-forms are derived. See todo
00036    "Update the php-functions" in the plans-file.
00037 */
00038 
00039 /* Encoding all injective maps from {1,...,m} to {1,...,n}
00040    (putting pigeon i in {1,...,m} into hole in {1,...,n}).
00041 */
00042 
00043 /* Variables are "php(i,j)", meaning that pigeon i is in hole j: */
00044 kill(php)$
00045 declare(php, noun)$
00046 declare(php, posfun)$
00047 php_var(i,j) := nounify(php)(i,j)$
00048 
00049 /* The set of variables for the pigeonhole formulas with m pigeons and
00050    n holes (order is lexicographical):
00051 */
00052 var_php_l(m,n) := create_list(php_var(i,j), i,1,m, j,1,n)$
00053 var_php(m,n) := setify(var_php_l(m,n))$
00054 
00055 /* In the following m denotes the number of pigeons, n the number of holes. */
00056 
00057 /* No two pigeons in the same hole (order is first holes k, then the two
00058    pigeons i, j lexicographically):
00059 */
00060 pigeons_different_holes_cl(m,n) :=
00061  create_list({-php_var(i,k), -php_var(j,k)}, k,1,n, i,1,m-1, j,i+1,m)$
00062 pigeons_different_holes_cs(m,n) := setify(pigeons_different_holes_cl(m,n))$
00063 
00064 /* Every pigeon in one hole (order by pigeons): */
00065 pigeons_in_holes_cl(m,n) :=
00066  create_list(setify(create_list(php_var(i,j), j,1,n)), i,1,m)$
00067 pigeons_in_holes_cs(m,n) := setify(pigeons_in_holes_cl(m,n))$
00068 
00069 /* The weak pigeon formula as formal clause-set: */
00070 weak_php_fcs(m,n) := [var_php(m,n),
00071  union(pigeons_different_holes_cs(m,n), pigeons_in_holes_cs(m,n))]$
00072 weak_php_cs(m,n) := fcs2cs(weak_php_fcs(m,n))$
00073 
00074 output_weak_php(m,n,filename) := block(
00075  [FF : standardise_fcs(weak_php_fcs(m,n))],
00076   output_fcs_v(
00077     sconcat("The pigeonhole principle (weak form): ", m, " pigeons, ", n, " holes."),
00078     FF[1], filename, FF[2]))$
00079 output_weak_php_stdname(m,n) := output_weak_php(m,n,
00080   sconcat("PHP_weak_",m,"_",n,".cnf"))$
00081 
00082 
00083 /* Additional clauses: */
00084 
00085 
00086 /* No pigeon in more than one hole: */
00087 pigeon_unique_hole(m,n) := setify(create_list({-php_var(i,k1), -php_var(i,k2)},
00088   i,1,m, k1,1,n-1, k2,k1+1,n))$
00089 
00090 /* Every hole carries a pigeon: */
00091 holes_occupied(m,n) :=
00092  setify(create_list(setify(create_list(php_var(i,j), i, 1, m)), j,1,n))$
00093 
00094 /* Remark: The clauses of pigeon_unique_hole(m,n) as well as of
00095    pigeon_unique_hole(m,n) are totally blocked for weak_php_cs(m,n) (except
00096    possibly for degenerations) *on their own*, but not together.
00097 */
00098 
00099 /* The "strong" pigeonhole formula as formal clause-set: */
00100 strong_php_fcs(m,n) := block([FF : weak_php_fcs(m,n)],
00101   [FF[1], union(FF[2], pigeon_unique_hole(m,n))])$
00102 strong_php_cs(m,n) := fcs2cs(strong_php_fcs(m,n))$
00103 /* Remark: "strong" comes from our general terminology regarding boolean
00104    translation of non-boolean clause-sets; especially for the PHP the
00105    term "functional" is used.
00106 */
00107 
00108 output_strong_php(m,n,filename) := block(
00109  [FF : standardise_fcs(strong_php_fcs(m,n))],
00110   output_fcs_v(
00111     sconcat("The pigeonhole principle (strong (i.e., functional) form): ", m, " pigeons, ", n, " holes."),
00112     FF[1], filename, FF[2]))$
00113 output_strong_php_stdname(m,n) := output_strong_php(m,n,
00114   sconcat("PHP_strong_",m,"_",n,".cnf"))$
00115 
00116 
00117 /* The "dual_strong" pigeonhole formula as formal clause-set: */
00118 dual_strong_php_fcs(m,n) := block([FF : weak_php_fcs(m,n)],
00119   [FF[1], union(FF[2], holes_occupied(m,n))])$
00120 dual_strong_php_cs(m,n) := fcs2cs(dual_strong_php_fcs(m,n))$
00121 /* Remark: "dual strong" comes from our general terminology regarding boolean
00122    translation of non-boolean clause-sets; especially for the PHP the
00123    term "onto" is used.
00124 */
00125 
00126 output_dual_strong_php(m,n,filename) := block(
00127  [FF : standardise_fcs(dual_strong_php_fcs(m,n))],
00128   output_fcs_v(
00129     sconcat("The pigeonhole principle (dual strong (i.e., onto-) form): ", m, " pigeons, ", n, " holes."),
00130     FF[1], filename, FF[2]))$
00131 output_dual_strong_php_stdname(m,n) := output_dual_strong_php(m,n,
00132   sconcat("PHP_dual_strong_",m,"_",n,".cnf"))$
00133 
00134 
00135 /* The "special" pigeonhole formula as formal clause-set: */
00136 special_php_fcs(m,n) := block([FF : weak_php_fcs(m,n)],
00137   [FF[1], union(FF[2], pigeon_unique_hole(m,n), holes_occupied(m,n))])$
00138 special_php_cs(m,n) := fcs2cs(special_php_fcs(m,n))$
00139 /* Remark: special_php_fcs(m,n) is satisfiable iff m=n.
00140    "Special" comes from our general terminology regarding boolean
00141    translation of non-boolean clause-sets; especially for the PHP the
00142    term "onto-functional" is used (in case m>n).
00143 */
00144 
00145 output_special_php(m,n,filename) := block(
00146  [FF : standardise_fcs(special_php_fcs(m,n))],
00147   output_fcs_v(
00148     sconcat("The pigeonhole principle (special (i.e., bijective) form): ", m, " pigeons, ", n, " holes."),
00149     FF[1], filename, FF[2]))$
00150 output_special_php_stdname(m,n) := output_special_php(m,n,
00151   sconcat("PHP_special_",m,"_",n,".cnf"))$
00152 
00153 
00154 /* Measures */
00155 
00156 nvar_php(m,n) := m * n$
00157 
00158 /* List of clause-counts for weak_php as with ncl_list_fcs: */
00159 ncl_list_weak_php(m,n) :=
00160   if m = 0 then []
00161   elseif n = 0 then [[0,1]]
00162   elseif m = 1 then [[n,m]]
00163   elseif n = 1 then [[n,m], [2,n*binomial(m,2)]]
00164   elseif n = 2 then [[2,n*binomial(m,2)+m]]
00165   else [[2,n*binomial(m,2)], [n,m]]$
00166 ncl_weak_php(m,n) := block([L : ncl_list_weak_php(m,n)],
00167  return(sum(L[i][2], i, 1, length(L))))$
00168 
00169 deficiency_weak_php(m,n) := ncl_weak_php(m,n) - nvar_php(m,n)$
00170 
00171 /* The probability that a random assignment is satisfiable: */
00172 satprob_weak_php(m,n) := sum(binomial(n,i) * stirling2(i,m) * m! ,i,m,n) / 2^nvar_php(m,n)$
00173 
00174 
00175 /* *********************************
00176    * Extended pigeon-hole formulas *
00177    *********************************
00178 */
00179 
00180 /* PHP formulas with additional clauses from the Extended Resolution
00181    refutation given in [A short proof of the pigeon hole principle using
00182    extended resolution"; Stephen Cook].
00183 
00184    Additional clauses, using new variables, allow polynomial size
00185    resolution proofs.
00186 */
00187 
00188 /* Variables are "php_ext(n,i,j)", meaning that pigeon i is in hole j in the
00189    map from {1,...,n} to {1,...,n-1}.  */
00190 kill(php_ext)$
00191 declare(php_ext, noun)$
00192 declare(php_ext, posfun)$
00193 php_ext_var(n,i,j) := nounify(php_ext)(n,i,j)$
00194 
00195 /* Clauses enforcing that if the variables
00196      php_ext_var(mp+1,i,j) for i in {1,...,mp+2}, j in {1,...,mp+1}
00197    represent an injective map phi : {1,...,mp+2} -> {1,...,mp+1} then variables
00198      php_ext_var(mp,i,j) for i in {1,...,mp+1}, j in {1,...,mp}
00199    represent the map phi_mp :  {1,...,mp+1} -> {1,...,mp}:
00200      phi_mp(i) = phi(i) if phi(i) # mp
00201                  phi(mp+2) if phi(i) = mp.
00202 */
00203 php_induction_step_cl(mp) :=
00204     lappend(create_list(
00205       [{php_ext_var(mp,i,j), -php_ext_var(mp+1,i,j)},
00206        {php_ext_var(mp,i,j), -php_ext_var(mp+1,i,mp+1), -php_ext_var(mp+1,mp+2,j)},
00207        {-php_ext_var(mp,i,j), php_ext_var(mp+1,i,j), php_ext_var(mp+1,i,mp+1)},
00208        {-php_ext_var(mp,i,j), php_ext_var(mp+1,i,j), php_ext_var(mp+1,mp+2,j)}],
00209       i,1,mp+1,j,1,mp))$
00210 /* Extended pigeon-hole induction clauses (using uniform variable names): */
00211 php_induction_uni_cl(m) :=
00212   lappend(
00213     create_list(php_induction_step_cl(mp), mp,1,m-1))$
00214 php_induction_cl(m) :=
00215   substitute_cl(php_induction_uni_cl(m),sm2hm(var_ephp2php_sm(m)))$
00216 
00217 /* For m >= 0, yields weak_php_fcs(m+1,m) with Extended Resolution clauses
00218    as given in
00219    [A short proof of the pigeon hole principle using extended resolution;
00220    Stephen Cook]: */
00221 weak_php_unsat_ext_fcs(m) := block([F : weak_php_unsat_ext_uni_fcs(m)],
00222   [listify(substitute_cs({F[1]},sm2hm(var_ephp2php_sm(m))))[1],
00223    substitute_cs(F[2],sm2hm(var_ephp2php_sm(m)))])$
00224 /* Using now php_ext_var(m+1,i,j) for php_var(i,j) for uniformity: */
00225 weak_php_unsat_ext_uni_fcs(m) := block([F : weak_php_fcs(m+1,m)],
00226   [setify(create_list(php_ext_var(mp,i,j), mp, 1, m, i, 1, mp+1, j, 1, mp)),
00227    union(setify(php_induction_uni_cl(m)),
00228      substitute_cs(F[2],sm2hm(var_php2ephp_sm(m))))])$
00229 
00230 /* Standardisation */
00231 
00232 standardise_weak_php_unsat_ext_uni(m) :=
00233  lambda([t], ev(t, php_ext(l,i,j):=l^3/3+i*l-4*l/3+j, php_ext))$
00234 /* We have that:
00235      1) php_ext(l,i,j) := sum((lp+1) * lp, lp, 1, l-1) + (i-1) * l + j,
00236         that is: php_ext(1,1,1) -> 1, php_ext(1,2,1) -> 2,
00237                  php_ext(2,1,1) -> 3, php_ext(2,1,2) -> 4,
00238                  php_ext(2,2,1) -> 5, etc;
00239      2) the standardisation is independent of m, and m is only taken
00240      for consistency with other standardisation functions.
00241 */
00242 
00243 invstandardise_weak_php_unsat_ext_uni(m) :=
00244  lambda([t], block([l: 1,i,j],
00245      while l^3 - l + 3 <= 3 * t do l : l +1,
00246      l : l -1,
00247      t : t - ((l^3 - 4*l)/3),
00248      i : ceiling(t / l) - 1,
00249      t : t - i * l,
00250      php_ext_var(l,i,t)))$
00251 
00252 weak_php_unsat_ext_stdfcs(m) :=
00253   standardise_weak_php_unsat_ext_uni(m)(weak_php_unsat_ext_uni_fcs(m))$
00254 
00255 /* Mapping the standard pigeon hole variables to their counter-parts in
00256    the extended-pigeon-hole clause-set weak_php_unsat_ext_uni_fcs(m): */
00257 var_php2ephp_sm(m) :=
00258   setify(lappend(
00259       create_list(
00260         if l = m then
00261           [[ php_var(i,j), php_ext_var(m,i,j)  ],
00262           [ -php_var(i,j), -php_ext_var(m,i,j) ]]
00263         else
00264           [[ php_ext(l,i,j), php_ext_var(l,i,j) ],
00265           [ -php_ext(l,i,j), -php_ext_var(l,i,j) ]],
00266         l, 1, m,i,1,l+1,j,1,l)))$
00267 /* Renaming the extended-pigeon-hole variables to their counter-parts in
00268    the original pigeon-hole clause-set: */
00269 var_ephp2php_sm(m) :=
00270     setify(lappend(
00271         create_list(
00272           if l = m then
00273             [[ php_ext_var(m,i,j), php_var(i,j)  ],
00274             [ -php_ext_var(m,i,j), -php_var(i,j) ]]
00275           else
00276             [[ php_ext(l,i,j), php_ext_var(l,i,j) ],
00277             [ -php_ext(l,i,j), -php_ext_var(l,i,j) ]],
00278           l, 1, m,i,1,l+1,j,1,l)))$
00279 
00280 /* Output */
00281 
00282 output_weak_php_unsat_ext(m, filename) := block(
00283   [FF : weak_php_unsat_ext_stdfcs(m)],
00284   output_fcs_v(
00285     sconcat("The extended pigeonhole formulas: ", m+1, " pigeons, ", m, " holes."),
00286     FF, filename,
00287     create_list(php_ext_var(mp,i,j), mp, 1, m, i, 1, mp+1, j, 1, mp)))$
00288 output_weak_php_unsat_ext_stdname(m) :=
00289   output_weak_php_unsat_ext(m, sconcat("EPHP_",m,".cnf"))$
00290 
00291 /* Measures */
00292 
00293 nvar_weak_php_unsat_ext(m) := m^3/3+m^2+2*m/3$
00294 /* This is: (m+1) * m + sum((l+1) * l, l, 1, m-1), simpsum, expand, simp; */
00295 ncl_weak_php_unsat_ext(m) := 11*m^3/6+m^2/2-m/3+1$
00296 /* This is: (m+1) + binomial(m+1,2) * m + sum(4*l*(l-1),l,1,m),
00297             simpsum, expand,simp; */
00298 
00299 
00300 
00301 
00302