OKlibrary  0.2.1.6
SchurProblems.mac
Go to the documentation of this file.
00001 /* Oliver Kullmann, 19.4.2009 (Swansea) */
00002 /* Copyright 2009, 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/TestSystem/Lisp/Asserts.mac")$
00023 oklib_include("OKlib/ComputerAlgebra/Satisfiability/Lisp/ClauseSets/Statistics.mac")$
00024 oklib_include("OKlib/ComputerAlgebra/Satisfiability/Lisp/Generators/RamseyTheory/SchurProblems.mac")$
00025 
00026 
00027 kill(f)$
00028 
00029 /* *****************
00030    * Schur triples *
00031    *****************
00032 */
00033 
00034 okltest_schur_nbfcsud(f) := (
00035   assert(f(0,0) = [{},{},{}]),
00036   assert(f(0,1) = [{1},{},{}]),
00037   assert(f(0,2) = [{1,2},{},{}]),
00038   assert(f(0,3) = [{1,2,3},{},{}]),
00039   assert(f(1,0) = [{},{},{1}]),
00040   assert(f(1,1) = [{1},{},{1}]),
00041   assert(f(1,2) = [{1,2},{{[1,1],[2,1]}},{1}]),
00042   assert(f(1,3) = [{1,2,3},{{[1,1],[2,1]},{[1,1],[2,1]}},{1}]),
00043   assert(f(2,0) = [{},{},{1,2}]),
00044   assert(f(2,1) = [{1},{},{1,2}]),
00045   assert(f(2,2) = [{1,2},{{[1,1],[2,1]},{[1,2],[2,2]}},{1,2}]),
00046   assert(f(2,3) = [{1,2,3},{{[1,1],[2,1]},{[1,2],[2,2]}},{1,2}]),
00047   assert(f(3,0) = [{},{},{1,2,3}]),
00048   assert(f(3,1) = [{1},{},{1,2,3}]),
00049   assert(f(3,2) = [{1,2},{{[1,1],[2,1]},{[1,2],[2,2]},{[1,3],[2,3]}},{1,2,3}]),
00050   assert(f(3,3) = [{1,2,3},{{[1,1],[2,1]},{[1,2],[2,2]},{[1,3],[2,3]}},{1,2,3}]),
00051   true)$
00052 
00053 okltest_nvar_schur_nbfcsud(f) := (
00054   for r : 0 thru cokltl(6,10) do
00055    for n : 0 thru cokltl(6,10) do block([F : schur_nbfcsud(r,n)],
00056     assert(f(r,n) = length(F[1]))
00057   ),
00058   true)$
00059 
00060 okltest_nval_schur_nbfcsud(f) := (
00061   for r : 0 thru cokltl(6,10) do
00062    for n : 0 thru cokltl(6,10) do block([F : schur_nbfcsud(r,n)],
00063     assert(f(r,n) = length(F[3]))
00064   ),
00065   true)$
00066 
00067 okltest_ncl_list_schur_nbfcsud(f) := (
00068   for r : 0 thru cokltl(6,10) do
00069    for n : 0 thru cokltl(6,10) do block([F : schur_nbfcsud(r,n)],
00070     assert(f(r,n) = ncl_list_fcs(F))
00071   ),
00072   true)$
00073 
00074 okltest_ncl_schur_nbfcsud(f) := (
00075   for r : 0 thru cokltl(6,10) do
00076    for n : 0 thru cokltl(6,10) do block([F : schur_nbfcsud(r,n)],
00077     assert(f(r,n) = ncl_fcs(F))
00078   ),
00079   true)$
00080 
00081 okltest_nvar_pd_schur_nbfcsud(f) := (
00082   for r : 0 thru cokltl(6,10) do
00083    for n : 0 thru cokltl(6,10) do block([F : pd_schur_nbfcsud(r,n)],
00084     assert(f(r,n) = length(F[1]))
00085   ),
00086   true)$
00087 
00088 okltest_nvar_pd_wschur_nbfcsud(f) := (
00089   for r : 0 thru cokltl(6,10) do
00090    for n : 0 thru cokltl(6,10) do block([F : pd_wschur_nbfcsud(r,n)],
00091     assert(f(r,n) = length(F[1]))
00092   ),
00093   true)$
00094 
00095 
00096 /* *********************
00097    * Symmetry breaking *
00098    *********************
00099 */
00100 
00101 okltest_schur_sb_nbfcsud(f) := (
00102   assert(f(0,1) = [{1},{},{}]),
00103   assert(f(0,2) = [{1,2},{},{}]),
00104   assert(f(0,3) = [{1,2,3},{},{}]),
00105   assert(f(1,1) = [{1},{},{1}]),
00106   assert(f(1,2) = [{1,2},{{[1,1],[2,1]}},{1}]),
00107   assert(f(1,3) = [{1,2,3},{{[1,1],[2,1]},{[1,1],[2,1]}},{1}]),
00108   assert(f(2,1) = [{1},{{[1,2]}},{1,2}]),
00109   assert(f(2,2) = [{1,2},{{[1,2]},{[1,1],[2,1]},{[1,2],[2,2]}},{1,2}]),
00110   assert(f(2,3) = [{1,2,3},{{[1,2]},{[1,1],[2,1]},{[1,2],[2,2]}},{1,2}]),
00111   assert(f(3,1) = [{1},{{[1,2]},{[1,3]}},{1,2,3}]),
00112   assert(f(3,2) = [{1,2},{{[1,2]},{[1,3]},{[1,1],[2,1]},{[1,2],[2,2]},{[1,3],[2,3]}},{1,2,3}]),
00113   assert(f(3,3) = [{1,2,3},{{[1,2]},{[1,3]},{[1,1],[2,1]},{[1,2],[2,2]},{[1,3],[2,3]}},{1,2,3}]),
00114   /* XXX */
00115   true)$
00116 
00117 
00118 /* ****************************
00119    * Heuristical restrictions *
00120    ****************************
00121 */
00122 
00123 okltest_schur_fullsb_nbcl(f) := (
00124   assert(f(0,inf) = []),
00125   assert(f(1,inf) = []),
00126   assert(f(2,inf) = [{[1,2]},{[2,1]}]),
00127   assert(f(3,inf) = [{[1,2]},{[1,3]},{[2,1]},{[2,3]},{[5,1]},{[5,2]}]),
00128   assert(f(4,inf) = [{[1,2]},{[1,3]},{[1,4]},{[2,1]},{[2,3]},{[2,4]},{[5,1]},{[5,2]},{[5,4]},{[14,1]},{[14,2]},{[14,3]}]),
00129   assert(f(4,14) = [{[1,2]},{[1,3]},{[1,4]},{[2,1]},{[2,3]},{[2,4]},{[5,1]},{[5,2]},{[5,4]},{[14,1]},{[14,2]},{[14,3]}]),
00130   assert(f(4,13) = [{[1,2]},{[1,3]},{[1,4]},{[2,1]},{[2,3]},{[2,4]},{[5,1]},{[5,2]},{[5,4]}]),
00131   true)$
00132 
00133 okltest_wschur_fullsb_nbcl(f) := (
00134   assert(f(0,inf) = []),
00135   assert(f(1,inf) = []),
00136   assert(f(2,inf) = [{[1,2]},{[3,1]}]),
00137   assert(f(3,inf) = [{[1,2]},{[1,3]},{[3,1]},{[3,3]},{[9,1]},{[9,2]}]),
00138   assert(f(4,inf) = [{[1,2]},{[1,3]},{[1,4]},{[3,1]},{[3,3]},{[3,4]},{[9,1]},{[9,2]},{[9,4]},{[24,1]},{[24,2]},{[24,3]}]),
00139   assert(f(4,24) = [{[1,2]},{[1,3]},{[1,4]},{[3,1]},{[3,3]},{[3,4]},{[9,1]},{[9,2]},{[9,4]},{[24,1]},{[24,2]},{[24,3]}]),
00140   assert(f(4,23) = [{[1,2]},{[1,3]},{[1,4]},{[3,1]},{[3,3]},{[3,4]},{[9,1]},{[9,2]},{[9,4]}]),
00141   true)$
00142 
00143 okltest_schur_rm_nbfclud(f) := (
00144   assert(f(1,1,0) = [[1],[],[1]]),
00145   assert(f(1,1,1) = [[1],[{[1,1]}],[1]]),
00146   assert(f(1,2,0) = [[1,2],[{[1,1],[2,1]}],[1]]),
00147   assert(f(1,2,1) = [[1,2],[{[1,1]},{[1,1],[2,1]}],[1]]),
00148   assert(f(1,2,2) = [[1,2],[{[1,1]},{[2,1]},{[1,1],[2,1]}],[1]]),
00149   /* XXX */
00150   true)$
00151 
00152 
00153 /* ****************************************
00154    * Translation into boolean clause-sets *
00155    ****************************************
00156 */
00157 
00158 okltest_schur_aloamo_fcl(f) := (
00159   assert(f(0,0) = [[],[]]),
00160   for n : 0 thru 4 do
00161     assert(f(0,n) = [[],create_list({},i,1,n)]),
00162   for n : 0 thru 1 do
00163     assert(f(1,n) = [create_list(nbv(i,1),i,1,n),create_list({nbv(i,1)},i,1,n)]),
00164   /* XXX */
00165   true)$
00166 
00167 okltest_nvar_schur_aloamo_fcl(f) := (
00168   for r : 0 thru 6 do
00169    for n : 0 thru 6 do
00170     assert(f(r,n) = nvar_fcl(schur_aloamo_fcl(r,n))),
00171   true)$
00172 
00173 okltest_nvar_schur_aloamo_fcs(f) := (
00174   for r : 0 thru 6 do
00175    for n : 0 thru 6 do
00176     assert(f(r,n) = nvar_fcs(schur_aloamo_fcs(r,n))),
00177   true)$
00178 
00179 okltest_ncl_list_schur_aloamo_fcl(f) := (
00180   for r : 0 thru 6 do
00181    for n : 0 thru 6 do
00182     assert(f(r,n) = ncl_list_fcl(schur_aloamo_fcl(r,n))),
00183   true)$
00184 
00185 okltest_ncl_list_schur_aloamo_fcs(f) := (
00186   for r : 0 thru 6 do
00187    for n : 0 thru 6 do
00188     assert(f(r,n) = ncl_list_fcs(schur_aloamo_fcs(r,n))),
00189   true)$
00190 
00191 
00192 /* *******************
00193    * Standardisation *
00194    *******************
00195 */
00196 
00197 okltest_schur_aloamo_stdfcl(f) := (
00198   assert(f(0,0) = [[[],[]],[]]),
00199   for n : 0 thru cokltl(4,10) do
00200     assert(f(0,n) = [[[],create_list({},i,1,n)],[]]),
00201   for n : 0 thru 1 do
00202     assert(f(1,n) = [[create_list(i,i,1,n),create_list({i},i,1,n)],create_list(nbv(i,1),i,1,n)]),
00203   for r : 0 thru cokltl(4,10) do
00204    for n : 0 thru cokltl(4,10) do
00205     assert(f(r,n) = standardise_fcl(schur_aloamo_fcl(r,n))),
00206   true)$
00207 
00208 okltest_pd_schur_aloamo_stdfcl(f) := (
00209   assert(f(0,0) = [[[],[]],[]]),
00210   assert(f(0,1) = [[[],[{}]],[]]),
00211   assert(f(0,2) = [[[],[{},{}]],[]]),
00212   for n : 0 thru 1 do
00213     assert(f(1,n) = [[create_list(i,i,1,n),create_list({i},i,1,n)],create_list(nbv(i,1),i,1,n)]),
00214   for r : 0 thru cokltl(4,10) do
00215    for n : 0 thru cokltl(4,10) do
00216     assert(f(r,n) = standardise_fcl(pd_schur_aloamo_fcl(r,n))),
00217   true)$
00218 
00219 okltest_mschur_aloamo_stdfcl(f) := (
00220   for r : 0 thru cokltl(4,10) do
00221    for n : 0 thru cokltl(4,10) do
00222     assert(f(r,n) = standardise_fcl(mschur_aloamo_fcl(r,n))),
00223   true)$
00224 
00225 okltest_wmschur_aloamo_stdfcl(f) := (
00226   for r : 0 thru cokltl(4,10) do
00227    for n : 0 thru cokltl(4,10) do
00228     assert(f(r,n) = standardise_fcl(wmschur_aloamo_fcl(r,n))),
00229   true)$
00230 
00231 okltest_symmetrictriples_aloamo_stdfcl(f) := (
00232   for r : 0 thru cokltl(4,10) do
00233    for n : 0 thru cokltl(4,5) do
00234     assert(f(r,n) = standardise_fcl(symmetrictriples_aloamo_fcl(r,n))),
00235   true)$
00236 
00237 okltest_wsymmetrictriples_aloamo_stdfcl(f) := (
00238   for r : 0 thru cokltl(4,10) do
00239    for n : 0 thru cokltl(4,5) do
00240     assert(f(r,n) = standardise_fcl(wsymmetrictriples_aloamo_fcl(r,n))),
00241   true)$
00242 
00243 okltest_pd_schur_fullsb_aloamo_stdfcl(f) := (
00244   assert(f(0,0) = [[[],[]],[]]),
00245   /* XXX */
00246   for r : 0 thru cokltl(4,10) do
00247    for n : 0 thru cokltl(4,10) do
00248     assert(f(r,n) = standardise_fcl(pd_schur_fullsb_aloamo_fcl(r,n))),
00249   true)$
00250 
00251 okltest_pd_wschur_fullsb_aloamo_stdfcl(f) := (
00252   assert(f(0,0) = [[[],[]],[]]),
00253   /* XXX */
00254   for r : 0 thru cokltl(4,10) do
00255    for n : 0 thru cokltl(4,10) do
00256     assert(f(r,n) = standardise_fcl(pd_wschur_fullsb_aloamo_fcl(r,n))),
00257   true)$
00258 
00259 okltest_schur_rm_aloamo_stdfcl(f) := (
00260   assert(f(0,0,0) = [[[],[]],[]]),
00261   /* XXX */
00262   for r : 1 thru cokltl(4,10) do
00263    for n : 0 thru cokltl(4,10) do
00264     for k : 0 thru n do
00265      assert(f(r,n,k) = standardise_fcl(schur_rm_aloamo_fcl(r,n,k))),
00266   true)$
00267 
00268 okltest_pd_schur_rm_aloamo_stdfcl(f) := (
00269   assert(f(0,0,0) = [[[],[]],[]]),
00270   /* XXX */
00271   for r : 1 thru cokltl(4,10) do
00272    for n : 0 thru cokltl(4,10) do
00273     for k : 0 thru ceiling(n/2) do
00274      assert(f(r,n,k) = standardise_fcl(pd_schur_rm_aloamo_fcl(r,n,k))),
00275   true)$
00276 
00277 okltest_pd_schur_fullsb_rm_aloamo_stdfcl(f) := (
00278   assert(f(0,0,0) = [[[],[]],[]]),
00279   /* XXX */
00280   for r : 1 thru cokltl(4,10) do
00281    for n : 0 thru cokltl(4,10) do
00282     for k : 0 thru ceiling(n/2) do
00283      assert(f(r,n,k) = standardise_fcl(pd_schur_fullsb_rm_aloamo_fcl(r,n,k))),
00284   true)$
00285 
00286 okltest_schur_standnest_stdfcl(f) := (
00287   for n : 0 thru 1 do
00288     assert(f(1,n) = [[[],[]],[]]),
00289   for r : 0 thru cokltl(4,10) do
00290    for n : 0 thru cokltl(4,10) do
00291     assert(f(r,n) = standardise_fcl(schur_standnest_fcl(r,n))),
00292   true)$
00293