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