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 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/BasicOperations.mac")$
00024 oklib_include("OKlib/ComputerAlgebra/Satisfiability/Lisp/ClauseSets/Substitutions.mac")$
00025 oklib_include("OKlib/ComputerAlgebra/Hypergraphs/Lisp/SetSystems.mac")$
00026 
00027 kill(f)$
00028 
00029 
00030 /* **************************************************
00031    * Arithmetic progressions in the natural numbers *
00032    **************************************************
00033 */
00034 
00035 okltest_vanderwaerden2_fcl(f) := (
00036   assert(f(0,0) = [[],[{},{}]]),
00037   assert(f(0,1) = [[1],[{},{}]]),
00038   assert(f(1,0) = [[],[]]),
00039   assert(f(1,1) = [[1],[{1},{-1}]]),
00040   assert(f(3,5) = [[1,2,3,4,5], [{1,2,3},{2,3,4},{1,3,5},{3,4,5},{-1,-2,-3},{-2,-3,-4},{-1,-3,-5},{-3,-4,-5}]]),
00041   true)$
00042 
00043 okltest_vanderwaerden2_fcs(f) := (
00044   assert(f(0,0) = [{},{{}}]),
00045   assert(f(0,1) = [{1},{{}}]),
00046   assert(f(1,0) = [{},{}]),
00047   assert(f(1,1) = [{1},{{1},{-1}}]),
00048   assert(f(2,0) = [{},{}]),
00049   assert(f(2,1) = [{1},{}]),
00050   assert(f(2,2) = [{1,2},{{1,2},{-1,-2}}]),
00051   assert(f(2,3) = [{1,2,3},{{1,2},{1,3},{2,3},{-1,-2},{-1,-3},{-2,-3}}]),
00052   assert(f(3,0) = [{},{}]),
00053   assert(f(3,1) = [{1},{}]),
00054   assert(f(3,2) = [{1,2},{}]),
00055   assert(f(3,3) = [{1,2,3},{{1,2,3},{-1,-2,-3}}]),
00056   assert(f(3,4) = [{1,2,3,4},{{1,2,3},{2,3,4},{-1,-2,-3},{-2,-3,-4}}]),
00057   true)$
00058 
00059 okltest_vanderwaerden2nd_fcl(f) := block(
00060   assert(okltest_vanderwaerden2_fcl(buildq([f], lambda([k,n],f(k,k,n))))),
00061   assert(f(3,4,5) = [[1,2,3,4,5], [{1,2,3},{2,3,4},{1,3,5},{3,4,5},{-1,-2,-3,-4},{-2,-3,-4,-5}]]),
00062   true)$
00063 
00064 okltest_vanderwaerden2nd_fcs(f) := block(
00065   assert(okltest_vanderwaerden2_fcs(buildq([f], lambda([k,n],f(k,k,n))))),
00066   assert(f(3,4,4) = [{1,2,3,4},{{1,2,3},{2,3,4},{-1,-2,-3,-4}}]),
00067   true)$
00068 
00069 okltest_pd_vanderwaerden2nd_fcl(f) := (
00070   assert(f(3,4,6) = [[1,2,3],[{2,3},{-2,-3}]]),
00071   assert(f(3,4,9) = [[1,2,3,4,5],[{1,2,3},{2,4},{1,3,4},{1,5},{2,5},{3,5},{4,5},{-2,-4},{-1,-3,-5},{-3,-4,-5}]]),
00072   assert(okltest_pd_vanderwaerden2nd_fcs(buildq([f], lambda([k1,k2,n], fcl2fcs(f(k1,k2,n))))) = true),
00073   true)$
00074 
00075 okltest_pd_vanderwaerden2nd_fcs(f) := (
00076   assert(f(0,0,0) = [{},{{}}]),
00077   assert(f(0,0,1) = [{1},{{}}]),
00078   assert(f(0,1,0) = [{},{{}}]),
00079   assert(f(0,1,1) = [{1},{{},{-1}}]),
00080   assert(f(1,0,0) = [{},{{}}]),
00081   assert(f(1,0,1) = [{1},{{},{1}}]),
00082   assert(f(1,1,1) = [{1},{{1},{-1}}]),
00083   assert(f(3,4,7) = [{1,2,3,4}, {{1,3},{1,4},{2,4},{3,4},{-1,-3},{-2,-3,-4}}]),
00084   assert(f(3,4,8) = [{1,2,3,4}, {{1,2,3},{1,2,4},{3,4},{-3,-4}}]),
00085   true)$
00086 
00087 okltest_vanderwaerden_nbfclud(f) := (
00088   assert(f([],0) = [[],[],[]]),
00089   assert(f([1],3) = [[1,2,3], [{[1,1]},{[2,1]},{[3,1]}], [1]]),
00090   assert(f([2],3) = [[1,2,3], [{[1,1],[2,1]},{[1,1],[3,1]},{[2,1],[3,1]}], [1]]),
00091   assert(f([1,1,1],4) = [[1,2,3,4], [{[1,1]},{[2,1]},{[3,1]},{[4,1]},{[1,2]},{[2,2]},{[3,2]},{[4,2]},{[1,3]},{[2,3]},{[3,3]},{[4,3]}], [1,2,3]]),
00092   assert(f([1,2,3],3) = [[1,2,3], [{[1,1]},{[2,1]},{[3,1]},{[1,2],[2,2]},{[1,2],[3,2]},{[2,2],[3,2]},{[1,3],[2,3],[3,3]}], [1,2,3]]),
00093   assert(okltest_vanderwaerden_nbfcsud(buildq([f],lambda([L,n],fcl2fcs(f(L,n))))) = true),
00094   true)$
00095 
00096 okltest_vanderwaerden_nbfcsud(f) := block(
00097   assert(f([],0) = [{},{},{}]),
00098   assert(f([],1) = [{1},{},{}]),
00099   assert(f([],2) = [{1,2},{},{}]),
00100   assert(f([1],0) = [{},{},{1}]),
00101   assert(f([1],1) = [{1},{{[1,1]}},{1}]),
00102   assert(f([1],2) = [{1,2},{{[1,1]},{[2,1]}},{1}]),
00103   assert(f([1,1],0) = [{},{},{1,2}]),
00104   assert(f([1,1],1) = [{1},{{[1,1]},{[1,2]}},{1,2}]),
00105   assert(f([1,1],2) = [{1,2},{{[1,1]},{[1,2]},{[2,1]},{[2,2]}},{1,2}]),
00106   assert(f([2],0) = [{},{},{1}]),
00107   assert(f([2],1) = [{1},{},{1}]),
00108   assert(f([2],2) = [{1,2},{{[1,1],[2,1]}},{1}]),
00109   assert(f([1,2],0) = [{},{},{1,2}]),
00110   assert(f([1,2],1) = [{1},{{[1,1]}},{1,2}]),
00111   assert(f([1,2],2) = [{1,2},{{[1,1]},{[2,1]},{[1,2],[2,2]}},{1,2}]),
00112   assert(f([2,2],0) = [{},{},{1,2}]),
00113   assert(f([2,2],1) = [{1},{},{1,2}]),
00114   assert(f([2,2],2) = [{1,2},{{[1,1],[2,1]},{[1,2],[2,2]}},{1,2}]),
00115   assert(f([2,2],3) = [{1,2,3},{{[1,1],[2,1]},{[1,1],[3,1]},{[2,1],[3,1]},{[1,2],[2,2]},{[1,2],[3,2]},{[2,2],[3,2]}},{1,2}]),
00116   assert(f([2,3],0) = [{},{},{1,2}]),
00117   assert(f([2,3],1) = [{1},{},{1,2}]),
00118   assert(f([2,3],2) = [{1,2},{{[1,1],[2,1]}},{1,2}]),
00119   assert(f([2,3],3) = [{1,2,3},{{[1,1],[2,1]},{[1,1],[3,1]},{[2,1],[3,1]},{[1,2],[2,2],[3,2]}},{1,2}]),
00120   assert(f([3,3],0) = [{},{},{1,2}]),
00121   assert(f([3,3],1) = [{1},{},{1,2}]),
00122   assert(f([3,3],2) = [{1,2},{},{1,2}]),
00123   assert(f([3,3],3) = [{1,2,3},{{[1,1],[2,1],[3,1]},{[1,2],[2,2],[3,2]}},{1,2}]),
00124   assert(f([3,3],4) = [{1,2,3,4},{{[1,1],[2,1],[3,1]},{[1,2],[2,2],[3,2]},{[2,1],[3,1],[4,1]},{[2,2],[3,2],[4,2]}},{1,2}]),
00125   assert(f([3,3,3],0) = [{},{},{1,2,3}]),
00126   assert(f([3,3,3],1) = [{1},{},{1,2,3}]),
00127   assert(f([3,3,3],2) = [{1,2},{},{1,2,3}]),
00128   assert(f([3,3,3],3) = [{1,2,3},{{[1,1],[2,1],[3,1]},{[1,2],[2,2],[3,2]},{[1,3],[2,3],[3,3]}},{1,2,3}]),
00129   assert(f([1,3,3,3],3) = [{1,2,3},{{[1,1]},{[2,1]},{[3,1]},{[1,2],[2,2],[3,2]},{[1,3],[2,3],[3,3]},{[1,4],[2,4],[3,4]}},{1,2,3,4}]),
00130   true)$
00131 
00132 
00133 /* ****************************************
00134    * Translation into boolean clause-sets *
00135    ****************************************
00136 */
00137 
00138 okltest_vanderwaerden_aloamo_fcl(f) := block(
00139   assert(f([],0) = [[],[]]),
00140   for k : 0 thru 5 do
00141     assert(f([k],0) = [[], if k=0 then [{}] else []]),
00142   for n : 0 thru 5 do
00143     assert(f([],n) = [[], create_list({},i,1,n)]),
00144   assert(f([3,3],3) = [[nbv(1,1),nbv(1,2),nbv(2,1),nbv(2,2),nbv(3,1),nbv(3,2)], [{-nbv(1,1),-nbv(2,1),-nbv(3,1)},{-nbv(1,2),-nbv(2,2),-nbv(3,2)},{nbv(1,1),nbv(1,2)},{nbv(2,1),nbv(2,2)},{nbv(3,1),nbv(3,2)},{-nbv(1,1),-nbv(1,2)},{-nbv(2,1),-nbv(2,2)},{-nbv(3,1),-nbv(3,2)}]]),
00145   assert(okltest_vanderwaerden_aloamo_fcs(buildq([f],lambda([L,n],fcl2fcs(f(L,n))))) = true),
00146   assert(okltest_vanderwaerden_aloamo_stdfcl(buildq([f],lambda([L,n],standardise_fcl(f(L,n))))) = true),
00147   /* XXX */
00148   true)$
00149 
00150 okltest_vanderwaerden_aloamo_fcs(f) := (
00151   assert(f([],0) = [{},{}]),
00152   for k : 0 thru 5 do
00153     assert(f([k],0) = [{}, if k=0 then {{}} else {}]),
00154   for n : 0 thru 5 do
00155     assert(f([],n) = [{}, if n=0 then {} else {{}}]),
00156   assert(f([3,3],3) = [{nbv(1,1),nbv(1,2),nbv(2,1),nbv(2,2),nbv(3,1),nbv(3,2)}, {{-nbv(1,1),-nbv(2,1),-nbv(3,1)},{-nbv(1,2),-nbv(2,2),-nbv(3,2)},{nbv(1,1),nbv(1,2)},{nbv(2,1),nbv(2,2)},{nbv(3,1),nbv(3,2)},{-nbv(1,1),-nbv(1,2)},{-nbv(2,1),-nbv(2,2)},{-nbv(3,1),-nbv(3,2)}}]),
00157   /* XXX */
00158   true)$
00159 
00160 okltest_vanderwaerden_aloamo_stdfcl(f) := (
00161   assert(f([],0) = [[[],[]],[]]),
00162   for k : 0 thru 5 do
00163     assert(f([k],0) = [[[], if k=0 then [{}] else []], []]),
00164   for n : 0 thru 5 do
00165     assert(f([],n) = [[[], create_list({},i,1,n)],[]]),
00166   assert(f([2,3],4) = [[[1,2,3,4,5,6,7,8], [{-1,-3},{-1,-5},{-3,-5},{-1,-7},{-3,-7},{-5,-7},{-2,-4,-6},{-4,-6,-8},{1,2},{3,4},{5,6},{7,8},{-1,-2},{-3,-4},{-5,-6},{-7,-8}]], [nbv(1,1),nbv(1,2),nbv(2,1),nbv(2,2),nbv(3,1),nbv(3,2),nbv(4,1),nbv(4,2)]]),
00167   assert(okltest_vanderwaerden_aloamo_stdfcs(buildq([f],lambda([L,n],block([FF:f(L,n)], [fcl2fcs(FF[1]),FF[2]])))) = true),
00168   /* XXX */
00169   true)$
00170 
00171 okltest_vanderwaerden_aloamo_stdfcs(f) := (
00172   assert(f([],0) = [[{},{}],[]]),
00173   for k : 0 thru 5 do
00174     assert(f([k],0) = [[{}, if k=0 then {{}} else {}], []]),
00175   for n : 0 thru 5 do
00176     assert(f([],n) = [[{}, if n=0 then {} else {{}}], []]),
00177   /* XXX */
00178   true)$
00179 
00180 okltest_standardise_vanderwaerden_aloamo(f) := block([s],
00181   for k : 0 thru 5 do
00182     s : f([k],0),
00183   for n : 0 thru 5 do
00184     s : f([],n),
00185   for n : 0 thru 5 do (
00186     s : f([1],n),
00187     for i : 1 thru n do
00188       assert(s(nbv(i,1)) = i)
00189   ),
00190   for m : 0 thru 3 do
00191     for n : 0 thru 5 do (
00192       s : f(create_list(1,i,1,m),n),
00193       assert(s(create_list(nbv(i,j), i,1,n, j,1,m)) = create_list(i,i,1,m*n))
00194   ),
00195   true)$
00196 
00197 okltest_invstandardise_vanderwaerden_aloamo(f) := block([invs],
00198   for k : 0 thru 5 do
00199     invs : f([k],0),
00200   for n : 0 thru 5 do
00201     invs : f([],n),
00202   for n : 0 thru 5 do (
00203     invs : f([1],n),
00204     for i : 1 thru n do
00205       assert(invs(i) = nbv(i,1))
00206   ),
00207   /* XXX */
00208   true)$
00209 
00210 
00211 /* ************************
00212    * Statistics functions *
00213    ************************
00214 */
00215 
00216 okltest_nvar_vanderwaerden2(f) := (
00217   for k : 0 thru 3 do
00218     for n : 0 thru k+3 do
00219       assert(f(k,n) = length(vanderwaerden2_fcs(k,n)[1])),
00220   true)$
00221 
00222 okltest_nvar_vanderwaerden2nd(f) := (
00223   for k1 : 0 thru 3 do
00224     for k2 : 0 thru 3 do
00225     for n : 0 thru 5 do
00226       assert(f(k1,k2,n) = length(vanderwaerden2nd_fcs(k1,k2,n)[1])),
00227   true)$
00228 
00229 okltest_nvar_vanderwaerden(f) := block([K,N],
00230   if oklib_test_level = 0 then (K : 2, N : 3)
00231   else (K : 4, N : 5),
00232   for L in map(sort,all_transformations_l(setn(K))) do
00233     for n : 0 thru N do block([v : f(L,n)],
00234       assert(v = length(vanderwaerden_nbfclud(L,n)[1])),
00235       assert(v = length(vanderwaerden_nbfcsud(L,n)[1]))
00236   ),
00237   true)$
00238 
00239 okltest_nvar_vanderwaerden_aloamo(f) := block([K,N],
00240   if oklib_test_level = 0 then (K : 2, N : 3)
00241   else (K : 4, N : 5),
00242   for L in map(sort,all_transformations_l(setn(K))) do
00243     for n : 0 thru N do block([v : f(L,n)],
00244       assert(v = length(vanderwaerden_aloamo_fcl(L,n)[1])),
00245       assert(v = length(vanderwaerden_aloamo_fcs(L,n)[1])),
00246       assert(v = length(vanderwaerden_aloamo_stdfcl(L,n)[1][1])),
00247       assert(v = length(vanderwaerden_aloamo_stdfcs(L,n)[1][1]))
00248   ),
00249   true)$
00250 
00251 okltest_ncl_vanderwaerden2_cs(f) := (
00252   for k : 0 thru 3 do
00253     for n : 0 thru k+3 do
00254       assert(f(k,n) = length(vanderwaerden2_fcs(k,n)[2])),
00255   true)$
00256 
00257 okltest_ncl_vanderwaerden2nd_cs(f) := (
00258   for k1 : 0 thru 3 do
00259     for k2 : 0 thru 3 do
00260     for n : 0 thru 5 do
00261       assert(f(k1,k2,n) = length(vanderwaerden2nd_fcs(k1,k2,n)[2])),
00262   true)$
00263 
00264 okltest_ncl_vanderwaerden_cl(f) := block([K,N],
00265   if oklib_test_level = 0 then (K : 2, N : 3)
00266   else (K : 4, N : 5),
00267   for L in map(sort,all_transformations_l(setn(K))) do
00268     for n : 0 thru N do block([c : f(L,n)],
00269       assert(c = length(vanderwaerden_nbfclud(L,n)[2]))
00270   ),
00271   true)$
00272 
00273 okltest_ncl_vanderwaerden_cs(f) := block([K,N],
00274   if oklib_test_level = 0 then (K : 2, N : 3)
00275   else (K : 4, N : 5),
00276   for L in map(sort,all_transformations_l(setn(K))) do
00277     for n : 0 thru N do block([c : f(L,n)],
00278       assert(c = length(vanderwaerden_nbfcsud(L,n)[2]))
00279   ),
00280   true)$
00281 
00282 okltest_ncl_vanderwaerden_aloamo_cl(f) := block([K,N],
00283   if oklib_test_level = 0 then (K : 2, N : 3)
00284   else (K : 4, N : 5),
00285   for L in map(sort,all_transformations_l(setn(K))) do
00286     for n : 0 thru N do block([c : f(L,n)],
00287       assert(c = length(vanderwaerden_aloamo_fcl(L,n)[2])),
00288       assert(c = length(vanderwaerden_aloamo_stdfcl(L,n)[1][2]))
00289   ),
00290   true)$
00291 
00292 okltest_ncl_vanderwaerden_aloamo_cs(f) := block([K,N],
00293   if oklib_test_level = 0 then (K : 2, N : 3)
00294   else (K : 4, N : 5),
00295   for L in map(sort,all_transformations_l(setn(K))) do (
00296     for n : 0 thru N do block([c : f(L,n)],
00297       assert(c = length(vanderwaerden_aloamo_fcs(L,n)[2])),
00298       assert(c = length(vanderwaerden_aloamo_stdfcs(L,n)[1][2]))
00299   )),
00300   true)$
00301 
00302 
00303 /* ********************
00304    * Output functions *
00305    ********************
00306 */
00307 
00308