OKlibrary  0.2.1.6
VanderWaerdenProblems.mac
Go to the documentation of this file.
```00001 /* Oliver Kullmann, 20.9.2008 (Swansea) */
00002 /* Copyright 2008, 2009, 2010, 2011, 2012 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/Hypergraphs/Lisp/Generators/Generators.mac")\$
00023 oklib_include("OKlib/ComputerAlgebra/Satisfiability/Lisp/ClauseSets/BasicOperations.mac")\$
00024 oklib_include("OKlib/ComputerAlgebra/Hypergraphs/Lisp/Colouring.mac")\$
00025 oklib_include("OKlib/ComputerAlgebra/Satisfiability/Lisp/ClauseSets/Constructions.mac")\$
00026 oklib_include("OKlib/ComputerAlgebra/Hypergraphs/Lisp/Basics.mac")\$
00027 oklib_include("OKlib/ComputerAlgebra/Satisfiability/Lisp/Generators/NonBooleanTranslations.mac")\$
00028 oklib_include("OKlib/ComputerAlgebra/Satisfiability/Lisp/ClauseSets/NonBoolean.mac")\$
00029 oklib_include("OKlib/ComputerAlgebra/DataStructures/Lisp/Lists.mac")\$
00030
00031
00032 /* **************************************************
00033    * Arithmetic progressions in the natural numbers *
00034    **************************************************
00035 */
00036
00037 /* Boolean formal clause-sets, whose solutions are the partitionings of
00038    {1,...,n} into two parts such that none of them contains an arithmetic
00039    progression of size k.
00040    (We are using "trivially generalised partitionings" here, where the
00041     parts can be empty.)
00042    For the list-form the order of clauses is as given by arithprog_ohg, where
00043    the positive clauses are associated to the first block of the partition
00044    (the first "colour").
00045 */
00046 /* Prerequisites: k, n natural numbers >= 0. */
00047 vanderwaerden2_fcl(k,n) := tcol2sat_stdohg2stdfcl(arithprog_ohg(k,n))\$
00048 vanderwaerden2_fcs(k,n) := fcl2fcs(vanderwaerden2_fcl(k,n))\$
00049 /* The general non-diagonal form (the above case has k=k1=k2). */
00050 /* Prerequisites: k1, k2, n natural numbers >= 0. */
00051 vanderwaerden2nd_fcl(k1,k2,n) := block(
00052  [G1 : arithprog_ohg(k1,n), G2 : arithprog_ohg(k2,n)],
00053   [G1[1], append(G1[2], comp_cl(G2[2]))])\$
00054 vanderwaerden2nd_fcs(k1,k2,n) := fcl2fcs(vanderwaerden2nd_fcl(k1,k2,n))\$
00055
00056 /* The palindromic versions: */
00057 pd_vanderwaerden2nd_fcl(k1,k2,n) := block(
00058  [G1 : palindromise_vdw_ohg(arithprog_ohg(k1,n)),
00059   G2 : palindromise_vdw_ohg(arithprog_ohg(k2,n))],
00060   [G1[1], append(G1[2], comp_cl(G2[2]))])\$
00061 pd_vanderwaerden2nd_fcs(k1,k2,n) := block(
00062  [G1 : palindromise_vdw_hg(arithprog_hg(k1,n)),
00063   G2 : palindromise_vdw_hg(arithprog_hg(k2,n))],
00064   [G1[1], union(G1[2], comp_cs(G2[2]))])\$
00065 /*
00066  pd_vanderwaerden2nd_fcs(k1,k2,n) = fcl2fcs(pd_vanderwaerden2nd_fcl(k1,k2,n).
00067 */
00068
00069 /* Now the general form, where L is a vdW-parameter-tuple.
00070    Prerequisite: vanderwaerden_p(L) is true, n natural number >= 0
00071    (see ComputerAlgebra/RamseyTheory/Lisp/VanderWaerden/Numbers.mac).
00072 */
00073 /* TODO: needs update, and order needs specification! */
00074 vanderwaerden_nbfclud(L,n) :=
00075  if emptyp(L) then [create_list(i,i,1,n),[],[]] else
00076   gcol2sat_stdohg2stdnbfclud(
00077    map(lambda([k], arithprog_ohg(k,n)), L),
00078    create_list(i,i,1,length(L)))\$
00079 vanderwaerden_nbfcsud(L,n) := nbfclud2nbfcsud(vanderwaerden_nbfclud(L,n))\$
00080
00081
00082 /* ****************************************
00083    * Translation into boolean clause-sets *
00084    ****************************************
00085 */
00086
00087 /* Translating the general forms into boolean clause-sets via the
00088    (strong) standard translation: */
00089 vanderwaerden_aloamo_fcl(L,n) :=
00090   nbfclud2fcl_aloamo(vanderwaerden_nbfclud(L,n))\$
00091 vanderwaerden_aloamo_fcs(L,n) := fcl2fcs(vanderwaerden_aloamo_fcl(L,n))\$
00092
00093 /* Standardising these boolean clause-sets: */
00094 vanderwaerden_aloamo_stdfcl(L,n) := block([m : length(L)],
00095   [block([s : standardise_vanderwaerden_aloamo(L,n)],
00096      s(vanderwaerden_aloamo_fcl(L,n))),
00097    block([invs : invstandardise_vanderwaerden_aloamo(L,n)],
00098      create_list(invs(i), i,1,n*m))])\$
00099 /* We have vanderwaerden_aloamo_stdfcl(L,n) =
00100    standardise_fcl(vanderwaerden_aloamo_fcl(L,n)).
00101 */
00102 vanderwaerden_aloamo_stdfcs(L,n) := block(
00103  [FF : vanderwaerden_aloamo_stdfcl(L,n)],
00104   [fcl2fcs(FF[1]), FF[2]])\$
00105
00106 /* Computing translation functions for standardising resp. de-standardising
00107    terms resp. individual variables:
00108 */
00109 standardise_vanderwaerden_aloamo(L,n) := block([m : length(L)],
00110   buildq([m], lambda([t], ev(t, nbv(v,i):=(v-1)*m+i, nbv))))\$
00111 invstandardise_vanderwaerden_aloamo(L,n) := block([m : length(L)],
00112   buildq([m], lambda([i], block([d : divide(i-1,m)+1],
00113     nbv_var(d[1], d[2])))))\$
00114
00115
00116 /* Translating the general forms into boolean clause-sets via the
00117    (weak and strong) standard nested translation:
00118 */
00119 vanderwaerden_standnest_fcl(L,n) :=
00120 nbfclud2fcl_standnest(vanderwaerden_nbfclud(L,n))\$
00121 vanderwaerden_standnest_fcs(L,n) := fcl2fcs(vanderwaerden_standnest_fcl(L,n))\$
00122
00123 vanderwaerden_standnest_strong_fcl(L,n) :=
00124 nbfclud2fcl_standnest_strong(vanderwaerden_nbfclud(L,n))\$
00125 vanderwaerden_standnest_strong_fcs(L,n) := fcl2fcs(vanderwaerden_standnest_strong_fcl(L,n))\$
00126
00127
00128 /* Standardising these boolean clause-sets: */
00129 vanderwaerden_standnest_stdfcl(L,n) := block([m : length(L)],
00130   [block([s : standardise_vanderwaerden_standnest(L,n)],
00131      s(vanderwaerden_standnest_fcl(L,n))),
00132    block([invs : invstandardise_vanderwaerden_standnest(L,n)],
00133      create_list(invs(i), i,1,n*(m-1)))])\$
00134 /* We have vanderwaerden_standnest_stdfcl(L,n) =
00135    standardise_fcl(vanderwaerden_standnest_fcl(L,n)).
00136 */
00137 vanderwaerden_standnest_stdfcs(L,n) := block(
00138  [FF : vanderwaerden_standnest_stdfcl(L,n)],
00139   [fcl2fcs(FF[1]), FF[2]])\$
00140
00141 vanderwaerden_standnest_strong_stdfcl(L,n) := block([m : length(L)],
00142   [block([s : standardise_vanderwaerden_standnest(L,n)],
00143      s(vanderwaerden_standnest_strong_fcl(L,n))),
00144    block([invs : invstandardise_vanderwaerden_standnest(L,n)],
00145      create_list(invs(i), i,1,n*(m-1)))])\$
00146 /* We have vanderwaerden_standnest_strong_stdfcl(L,n) =
00147    standardise_fcl(vanderwaerden_standnest_strong_fcl(L,n)).
00148 */
00149 vanderwaerden_standnest_strong_stdfcs(L,n) := block(
00150  [FF : vanderwaerden_standnest_strong_stdfcl(L,n)],
00151   [fcl2fcs(FF[1]), FF[2]])\$
00152
00153
00154 /* Computing translation functions for standardising resp. de-standardising
00155    terms resp. individual variables:
00156 */
00157 standardise_vanderwaerden_standnest(L,n) := block([m : length(L)],
00158   buildq([m], lambda([t], ev(t, nbv(v,i):=(v-1)*(m-1)+i, nbv))))\$
00159 invstandardise_vanderwaerden_standnest(L,n) := block([m : length(L)],
00160   buildq([m], lambda([i], block([d : divide(i-1,m-1)+1],
00161     nbv_var(d[1], d[2])))))\$
00162
00163
00164 /* ************************
00165    * Statistics functions *
00166    ************************
00167 */
00168
00169 nvar_vanderwaerden2(k,n) := n\$
00170 nvar_vanderwaerden2nd(k1,k2,n) := n\$
00171 nvar_vanderwaerden(L,n) := n\$
00172 nvar_vanderwaerden_aloamo(L,n) := length(L)*n\$
00173 /* nvar_vanderwaerden_aloamo is also valid for the standardised forms. */
00174
00175 ncl_vanderwaerden2_cs(k,n) := if k=0 then nhyp_arithprog_hg(0,n)
00176  else 2 * nhyp_arithprog_hg(k,n)\$
00177 ncl_vanderwaerden2nd_cs(k1,k2,n) :=
00178  if k1=0 and k2=0 then nhyp_arithprog_hg(0,n)
00179  else nhyp_arithprog_hg(k1,n) + nhyp_arithprog_hg(k2,n)\$
00180 ncl_vanderwaerden_cl(L,n) := sum_l(create_list(nhyp_arithprog_hg(k,n),k,L))\$
00181 ncl_vanderwaerden_cs(L,n) := sum_l(create_list(nhyp_arithprog_hg(k,n),k,L))\$
00182 ncl_vanderwaerden_aloamo_cl(L,n) :=
00183   ncl_vanderwaerden_cl(L,n) + n + n*binomial(length(L),2)\$
00184 ncl_vanderwaerden_aloamo_cs(L,n) := block([l:length(L)],
00185   if l=0 then if n=0 then 0 else 1 else
00186   ncl_vanderwaerden_cl(L,n) + n + n*binomial(l,2))\$
00187 /* These two functions are also valid for the standardised forms. */
00188
00189
00190 /* ********************
00191    * Output functions *
00192    ********************
00193 */
00194
00195 output_vanderwaerden2(k,n,filename) :=
00196   output_fcl_v(
00197     sconcat("Van der Waerden problem: 2 parts, arithmetic progressions of size ", k, ", and ", n, " elements.", newline, "C Using the direct (strong) translation.", newline, "c Created by output_vanderwaerden2(", k, ",", n, ",\"", filename, "\").", newline, "c ", created_by_OKlib()),
00198     vanderwaerden2_fcl(k,n),
00199     filename, [])\$
00200 /* Providing a standard name: "VanDerWaerden_2-k-k_n.cnf": */
00201 output_vanderwaerden2_stdname(k,n) := output_vanderwaerden2(k,n,
00202   sconcat("VanDerWaerden_2-",k,"-",k,"_",n,".cnf"))\$
00203
00204 output_vanderwaerden2nd(k1,k2,n,filename) :=
00205   output_fcl_v(
00206     sconcat("Van der Waerden problem: 2 parts, arithmetic progressions of size ", k1, " and ", k2, ", and ", n, " elements.", newline, "C Using the direct (strong) translation.", newline, "c Created by output_vanderwaerden2nd(", k1, ",", k2, ",", n, ",\"", filename, "\").", newline, "c ", created_by_OKlib()),
00207     vanderwaerden2nd_fcl(k1,k2,n),
00208     filename, [])\$
00209 /* Providing a standard name: "VanDerWaerden_2-k1-k2_n.cnf": */
00210 output_vanderwaerden2nd_stdname(k1,k2,n) := output_vanderwaerden2nd(k1,k2,n,
00211   sconcat("VanDerWaerden_2-",k1,"-",k2,"_",n,".cnf"))\$
00212
00213 output_pd_vanderwaerden2nd(k1,k2,n,filename) :=
00214   output_fcl_v(
00215     sconcat("Palindromic van der Waerden problem: 2 parts, arithmetic progressions of size ", k1, " and ", k2, ", and ", n, " elements, yielding ", ceiling(n/2), " variables.", newline, "C Using the direct (strong) translation.", newline, "c Created by output_pd_vanderwaerden2nd(", k1, ",", k2, ",", n, ",\"", filename, "\").", newline, "c ", created_by_OKlib()),
00216     pd_vanderwaerden2nd_fcl(k1,k2,n),
00217     filename, [])\$
00218 /* Providing a standard name: "VanDerWaerden_pd_2-k1-k2_n.cnf": */
00219 output_pd_vanderwaerden2nd_stdname(k1,k2,n) := output_pd_vanderwaerden2nd(k1,k2,n,
00220   sconcat("VanDerWaerden_pd_2-",k1,"-",k2,"_",n,".cnf"))\$
00221
00222
00223 /* Standardising the variables according to lexicographical order
00224    nbv(1,1),...,nbv(1,m),nbv(2,1), ..., nbv(n,m):
00225 */
00226 output_vanderwaerden(L,n,filename) := block(
00227  [FF : vanderwaerden_aloamo_stdfcl(L,n)],
00228   output_fcl_v(
00229     sconcat("Van der Waerden problem: ", length(L), " parts with arithmetic progressions of sizes ", L, ", and ", n, " elements.", newline, "C Using the direct (strong) translation.", newline, "c Created by output_vanderwaerden(", L, ",", n, ",\"", filename, "\").", newline, "c ", created_by_OKlib()),
00230     FF[1],
00231     filename,
00232     FF[2]))\$
00233 output_vanderwaerden_stdname(L,n) := output_vanderwaerden(L,n,
00234   sconcat("VanDerWaerden_",length(L),apply(sconcat,map(sconcat,create_list("-",i,1,length(L)),L)),"_",n,".cnf"))\$
00235
00236 output_vanderwaerden_standnest(L,n,filename) := block(
00237  [FF : vanderwaerden_standnest_stdfcl(L,n)],
00238   output_fcl_v(
00239     sconcat("Van der Waerden problem: ", length(L), " parts with arithmetic progressions of sizes ", L, ", and ", n, " elements.
00240 c Using the weak standard nested translation.", newline, "c Created by output_vanderwaerden_standnest(", L, ",", n, ",\"", filename, "\").", newline, "c ", created_by_OKlib()),
00241     FF[1],
00242     filename,
00243     FF[2]))\$
00244 output_vanderwaerden_standnest_stdname(L,n) := output_vanderwaerden_standnest(L,n,
00245   sconcat("VanDerWaerden_N_",length(L),apply(sconcat,map(sconcat,create_list("-",i,1,length(L)),L)),"_",n,".cnf"))\$
00246
00247 output_vanderwaerden_standnest_strong(L,n,filename) := block(
00248  [FF : vanderwaerden_standnest_strong_stdfcl(L,n)],
00249   output_fcl_v(
00250     sconcat("Van der Waerden problem: ", length(L), " parts with arithmetic progressions of sizes ", L, ", and ", n, " elements.
00251 c Using the strong standard nested translation.", newline, "c Created by output_vanderwaerden_standnest_strong(", L, ",", n, ",\"", filename, "\").", newline, "c ", created_by_OKlib()),
00252     FF[1],
00253     filename,
00254     FF[2]))\$
00255 output_vanderwaerden_standnest_strong_stdname(L,n) := output_vanderwaerden_standnest_strong(L,n,
00256   sconcat("VanDerWaerden_SN_",length(L),apply(sconcat,map(sconcat,create_list("-",i,1,length(L)),L)),"_",n,".cnf"))\$
00257
00258
00259
```