OKlibrary  0.2.1.6
HindmanProblems.mac
Go to the documentation of this file.
```00001 /* Oliver Kullmann, 12.7.2009 (Swansea) */
00002 /* Copyright 2009 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/Colouring.mac")\$
00023 oklib_include("OKlib/ComputerAlgebra/Satisfiability/Lisp/Generators/NonBooleanTranslations.mac")\$
00024 oklib_include("OKlib/ComputerAlgebra/Satisfiability/Lisp/ClauseSets/NonBoolean.mac")\$
00025 oklib_include("OKlib/ComputerAlgebra/Hypergraphs/Lisp/Generators/Hindman.mac")\$
00026
00027
00028 /* ********************
00029    * Hindman problems *
00030    ********************
00031 */
00032
00033 /* The non-boolean formal clause-set expressing the Hindman problem for k=2
00034    with r parts and n vertices.
00035    Reminder: The hyperedges are of the form {x,y,x+y,x*y} for x <> y.
00036    Prerequisites: r, n natural numbers, n, r >= 0.
00037 */
00038 hindmani_a1k2_nbfcsud(r,n) :=
00039  nbfclud2nbfcsud(col2sat_stdohg2stdnbfclud(hindmani_a1k2_ohg(n), create_list(i,i,1,r)))\$
00040
00041 /* Now allowing x = y: */
00042 hindman_a1k2_nbfcsud(r,n) :=
00043  nbfclud2nbfcsud(col2sat_stdohg2stdnbfclud(hindman_a1k2_ohg(n), create_list(i,i,1,r)))\$
00044
00045 /* Fixing r=2 (thus obtaining boolean clause-sets);
00046    again x <> y, but considering only x,y >= a: */
00047 hindmani_r2k2_ofcs(a,n) :=
00048  tcol2sat_stdohg2stdofcs(hindmani_k2_ohg(a,n))\$
00049
00050 /* The non-injective versions (allowing x = y): */
00051 hindman_r2k2_ofcs(a,n) :=
00052  tcol2sat_stdohg2stdofcs(hindman_k2_ohg(a,n))\$
00053
00054 /* Adding symmetry-breaking clauses (regarding the parts (colours), forcing
00055    vertex 1 to be in part 1); now we must have n >= 1: */
00056 hindmani_a1k2_sb_nbfcsud(r,n) := block([S : hindmani_a1k2_nbfcsud(r,n)],
00057  [S[1], union(setify(create_list({[1,i]},i,2,r)), S[2]), S[3]])\$
00058
00059
00060 /* Output facilities */
00061
00062 /* Output the boolean clause-set (standard translation) to a file: */
00063 output_hindmani_a1k2(r,n,filename) := block(
00064  [FF : standardise_fcs(nbfcsfd2fcs_aloamo(nbfcsud2nbfcsfd(hindmani_a1k2_nbfcsud(r,n))))],
00065   output_fcs_v(
00066     sconcat("Hindman problem (injective form) for k=2 with ", r, " parts and ", n, " elements."),
00067     FF[1],
00068     filename,
00069     FF[2]))\$
00070 /* Providing a standard name: "Hindmani_a1k2_r_n.cnf": */
00071 output_hindmani_a1k2_stdname(r,n) := output_hindmani_a1k2(r,n,
00072   sconcat("Hindmani_a1k2_",r,"_",n,".cnf"))\$
00073
00074 /* Allowing x=y: */
00075 output_hindman_a1k2(r,n,filename) := block(
00076  [FF : standardise_fcs(nbfcsfd2fcs_aloamo(nbfcsud2nbfcsfd(hindman_a1k2_nbfcsud(r,n))))],
00077   output_fcs_v(
00078     sconcat("Hindman problem for k=2 with ", r, " parts and ", n, " elements."),
00079     FF[1],
00080     filename,
00081     FF[2]))\$
00082 /* Providing a standard name: "Hindman_a1k2_r_n.cnf": */
00083 output_hindman_a1k2_stdname(r,n) := output_hindman_a1k2(r,n,
00084   sconcat("Hindman_a1k2_",r,"_",n,".cnf"))\$
00085
00086 /* With symmetry breaking: */
00087 output_hindmani_a1k2_sb(r,n,filename) := block(
00088  [FF : standardise_fcs(nbfcsfd2fcs_aloamo(nbfcsud2nbfcsfd(hindmani_a1k2_sb_nbfcsud(r,n))))],
00089   output_fcs_v(
00090     sconcat("Hindman problem (injective form) for k=2 with ", r, " parts and ", n, " elements; symmetry breaking by putting element 1 into part 1."),
00091     FF[1],
00092     filename,
00093     FF[2]))\$
00094 /* Providing a standard name: "Hindmani_a1k2_r_n.cnf": */
00095 output_hindmani_a1k2_sb_stdname(r,n) := output_hindmani_a1k2_sb(r,n,
00096   sconcat("Hindmani_a1k2_sb_",r,"_",n,".cnf"))\$
00097
00098
00099 /* Output the 2-colour cases (no translation needed) to a file: */
00100
00101 output_hindmani_r2k2(a,n,filename) := block(
00102  [FF :  hindmani_r2k2_ofcs(a,n)],
00103   output_fcs_v(
00104     sconcat("Hindman problem (injective form) for k=2 with 2 parts and ", n, " elements, starting with ", a, "."),
00105     FF,
00106     filename,[]))\$
00107 /* Providing a standard name: "Hindmani_r2k2_a_n.cnf": */
00108 output_hindmani_r2k2_stdname(a,n) := output_hindmani_r2k2(a,n,
00109   sconcat("Hindmani_r2k2_",a,"_",n,".cnf"))\$
00110
00111 output_hindman_r2k2(a,n,filename) := block(
00112  [FF :  hindman_r2k2_ofcs(a,n)],
00113   output_fcs_v(
00114     sconcat("Hindman problem for k=2 with 2 parts and ", n, " elements, starting with ", a, "."),
00115     FF,
00116     filename,[]))\$
00117 /* Providing a standard name: "Hindman_r2k2_a_n.cnf": */
00118 output_hindman_r2k2_stdname(a,n) := output_hindman_r2k2(a,n,
00119   sconcat("Hindman_r2k2_",a,"_",n,".cnf"))\$
00120
00121
```