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