OKlibrary  0.2.1.6
GreenTaoProblems.mac
Go to the documentation of this file.
00001 /* Oliver Kullmann, 30.12.2009 (Swansea) */
00002 /* Copyright 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/Substitutions.mac")$
00024 
00025 kill(f)$
00026 
00027 /* *****************************************
00028    * Arithmetic progressions in the primes *
00029    *****************************************
00030 */
00031 
00032 okltest_greentao2_fcl(f) := (
00033   assert(f(0,0) = [[],[{},{}]]),
00034   assert(f(0,1) = [[2],[{},{}]]),
00035   assert(f(1,0) = [[],[]]),
00036   assert(f(2,4) = [[2,3,5,7], [{2,3},{2,5},{3,5},{2,7},{3,7},{5,7},{-2,-3},{-2,-5},{-3,-5},{-2,-7},{-3,-7},{-5,-7}]]),
00037   assert(f(3,5) = [[2,3,5,7,11],[{3,5,7},{3,7,11},{-3,-5,-7},{-3,-7,-11}]]),
00038   assert(okltest_greentao2_fcs(buildq([f],lambda([k,n],fcl2fcs(f(k,n))))) = true),
00039   true)$
00040 
00041 okltest_greentao2_fcs(f) := (
00042   assert(f(0,0) = [{},{{}}]),
00043   assertf((0,1) = [{2},{{}}]),
00044   assert(f(1,0) = [{},{}]),
00045   assert(f(1,1) = [{2},{{2},{-2}}]),
00046   assert(f(2,0) = [{},{}]),
00047   assert(f(2,1) = [{2},{}]),
00048   assert(f(2,2) = [{2,3},{{2,3},{-2,-3}}]),
00049   assert(f(2,3) = [{2,3,5},{{2,3},{2,5},{3,5},{-2,-3},{-2,-5},{-3,-5}}]),
00050   assert(f(3,0) = [{},{}]),
00051   assert(f(3,1) = [{2},{}]),
00052   assert(f(3,2) = [{2,3},{}]),
00053   assert(f(3,3) = [{2,3,5},{}]),
00054   assert(f(3,4) = [{2,3,5,7},{{3,5,7},{-3,-5,-7}}]),
00055   true)$
00056 
00057 okltest_greentao2nd_fcl(f) := (
00058   assert(f(0,0,0) = [[],[{},{}]]),
00059   assert(f(0,1,2) = [[2,3],[{},{-2},{-3}]]),
00060   assert(okltest_greentao2nd_fcs(buildq([f],lambda([k1,k2,n],fcl2fcs(f(k1,k2,n))))) = true),
00061   assert(okltest_greentao2_fcl(buildq([f],lambda([k,n],f(k,k,n)))) = true),
00062   true)$
00063 
00064 okltest_greentao2nd_fcs(f) := (
00065   okltest_greentao2_fcs(buildq([f], lambda([k,n], f(k,k,n)))),
00066   assert(okltest_greentao2_fcs(buildq([f],lambda([k,n],f(k,k,n)))) = true),
00067   assert(f(3,4,5) = [{2,3,5,7,11}, {{3,5,7},{3,7,11}}]),
00068   assert(f(3,4,9) = [{2,3,5,7,11,13,17,19,23}, {{3,5,7},{3,7,11},{3,11,19},{3,13,23},{5,11,17},{7,13,19},{11,17,23},{-5,-11,-17,-23}}]),
00069   true)$
00070 
00071 okltest_greentao_nbfclud(f) := (
00072   assert(f([],0) = [[],[],[]]),
00073   assert(f([],1) = [[2],[],[]]),
00074   assert(f([],2) = [[2,3],[],[]]),
00075   assert(f([0],0) = [[],[{}],[1]]),
00076   assert(f([0,0],0) = [[],[{},{}],[1,2]]),
00077   assert(f([0,0,0,1],1) = [[2],[{},{},{},{[2,4]}],[1,2,3,4]]),
00078   assert(f([2,3],5) = [[2,3,5,7,11], [{[2,1],[3,1]},{[2,1],[5,1]},{[3,1],[5,1]},{[2,1],[7,1]},{[3,1],[7,1]},{[5,1],[7,1]},{[2,1],[11,1]},{[3,1],[11,1]},{[5,1],[11,1]},{[7,1],[11,1]},{[3,2],[5,2],[7,2]},{[3,2],[7,2],[11,2]}],[1,2]]),
00079   assert(okltest_greentao_nbfcsud(buildq([f],lambda([L,n], nbfclud2nbfcsud(f(L,n))))) = true),
00080   true)$
00081 
00082 okltest_greentao_nbfcsud(f) := (
00083   assert(f([],0) = [{},{},{}]),
00084   assert(f([],1) = [{2},{},{}]),
00085   assert(f([],2) = [{2,3},{},{}]),
00086   assert(f([1],0) = [{},{},{1}]),
00087   assert(f([1],1) = [{2},{{[2,1]}},{1}]),
00088   assert(f([1],2) = [{2,3},{{[2,1]},{[3,1]}},{1}]),
00089   assert(f([1,1],0) = [{},{},{1,2}]),
00090   assert(f([1,1],1) = [{2},{{[2,1]},{[2,2]}},{1,2}]),
00091   assert(f([1,1],2) = [{2,3},{{[2,1]},{[2,2]},{[3,1]},{[3,2]}},{1,2}]),
00092   assert(f([2],0) = [{},{},{1}]),
00093   assert(f([2],1) = [{2},{},{1}]),
00094   assert(f([2],2) = [{2,3},{{[2,1],[3,1]}},{1}]),
00095   assert(f([1,2,3],3) = [{2,3,5}, {
00096    {[2,1]},{[3,1]},{[5,1]},
00097    {[2,2],[3,2]},{[2,2],[5,2]},{[3,2],[5,2]}}, {1,2,3}]),
00098   assert(f([1,1,2,2,3,3],4) = [{2,3,5,7}, {
00099    {[2,1]},{[3,1]},{[5,1]},{[7,1]},
00100    {[2,2]},{[3,2]},{[5,2]},{[7,2]},
00101    {[2,3],[3,3]},{[2,3],[5,3]},{[2,3],[7,3]},{[3,3],[5,3]},{[3,3],[7,3]},{[5,3],[7,3]},
00102    {[2,4],[3,4]},{[2,4],[5,4]},{[2,4],[7,4]},{[3,4],[5,4]},{[3,4],[7,4]},{[5,4],[7,4]},
00103    {[3,5],[5,5],[7,5]},
00104    {[3,6],[5,6],[7,6]}
00105   }, {1,2,3,4,5,6}]),
00106   /* XXX */
00107   true)$
00108 
00109 okltest_greentaod_nbfclud(f) := (
00110   assert(f(0,0,0) = [[],[],[]]),
00111   assert(f(0,2,2) = [[2,3],[],[]]),
00112   assert(f(3,3,4) = [[2,3,5,7],[{[3,1],[5,1],[7,1]},{[3,2],[5,2],[7,2]},{[3,3],[5,3],[7,3]}],[1,2,3]]),
00113   assert(okltest_greentaod_nbfcsud(buildq([f],lambda([m,k,n],nbfclud2nbfcsud(f(m,k,n))))) = true),
00114   true)$
00115 
00116 okltest_greentaod_nbfcsud(f) := (
00117   assert(f(0,0,0) = [{},{},{}]),
00118   assert(f(0,1,2) = [{2,3},{},{}]),
00119   assert(f(1,2,3) = [{2,3,5},{{[2,1],[3,1]},{[2,1],[5,1]},{[3,1],[5,1]}},{1}]),
00120   assert(f(2,3,5) = [{2,3,5,7,11},{{[3,1],[5,1],[7,1]},{[3,1],[7,1],[11,1]},{[3,2],[5,2],[7,2]},{[3,2],[7,2],[11,2]}},{1,2}]),
00121   /* XXX */
00122   true)$
00123 
00124 
00125 /* ****************************************
00126    * Translation into boolean clause-sets *
00127    ****************************************
00128 */
00129 
00130 okltest_greentao_aloamo_fcl(f) := (
00131   assert(f([],0) = [[],[]]),
00132   assert(f([],1) = [[],[{}]]),
00133   assert(f([1],0) = [[],[]]),
00134   assert(f([1],1) = [[nbv(2,1)],[{-nbv(2,1)},{nbv(2,1)}]]),
00135   assert(f([1],2) = [[nbv(2,1),nbv(3,1)],[{-nbv(2,1)},{-nbv(3,1)},{nbv(2,1)},{nbv(3,1)}]]),
00136   assert(f([2,3],3) = [[nbv(2,1),nbv(2,2),nbv(3,1),nbv(3,2),nbv(5,1),nbv(5,2)],[{-nbv(2,1),-nbv(3,1)},{-nbv(2,1),-nbv(5,1)},{-nbv(3,1),-nbv(5,1)},{nbv(2,1),nbv(2,2)},{nbv(3,1),nbv(3,2)},{nbv(5,1),nbv(5,2)},{-nbv(2,1),-nbv(2,2)},{-nbv(3,1),-nbv(3,2)},{-nbv(5,1),-nbv(5,2)}]]),
00137   true)$
00138 
00139 okltest_greentao_aloamo_fcs(f) := (
00140   /* XXX */
00141   true)$
00142 
00143 okltest_greentao_standnest_fcl(f) := (
00144   assert(f([1],0) = [[],[]]),
00145   assert(f([1],1) = [[],[{}]]),
00146   assert(f([1],2) = [[],[{},{}]]),
00147   assert(f([2,3],3) = [[nbv(2,1),nbv(3,1),nbv(5,1)],[{nbv(2,1),nbv(3,1)},{nbv(2,1),nbv(5,1)},{nbv(3,1),nbv(5,1)}]]),
00148   assert(f([2,3],4) = [[nbv(2,1),nbv(3,1),nbv(5,1),nbv(7,1)],[{nbv(2,1),nbv(3,1)},{nbv(2,1),nbv(5,1)},{nbv(3,1),nbv(5,1)},{nbv(2,1),nbv(7,1)},{nbv(3,1),nbv(7,1)},{nbv(5,1),nbv(7,1)},{-nbv(3,1),-nbv(5,1),-nbv(7,1)}]]),
00149   true)$
00150 
00151 okltest_greentao_standnest_fcs(f) := (
00152   /* XXX */
00153   true)$
00154 
00155 okltest_greentao_standnest_strong_fcl(f) := (
00156 
00157   true)$
00158 
00159 okltest_greentao_standnest_strong_fcs(f) := (
00160 
00161   true)$
00162 
00163 okltest_greentao_logarithmic_fcl(f) := (
00164   assert(f([0],0) = [[],[{}]]),
00165   assert(f([0,0],0) = [[],[{},{}]]),
00166   assert(f([1],0) = [[],[]]),
00167   assert(f([1],1) = [[],[{}]]),
00168   assert(f([1],2) = [[],[{},{}]]),
00169   assert(f([0,1],0) = [[],[{}]]),
00170   assert(f([0,1],1) = [[nbv(2,1)],[{},{nbv(2,1)}]]),
00171   assert(f([0,1],2) = [[nbv(2,1),nbv(3,1)],[{},{nbv(2,1)},{nbv(3,1)}]]),
00172   assert(f([1,1],0) = [[],[]]),
00173   assert(f([1,1],1) = [[nbv(2,1)],[{-nbv(2,1)},{nbv(2,1)}]]),
00174   assert(f([1,1],2) = [[nbv(2,1),nbv(3,1)],[{-nbv(2,1)},{-nbv(3,1)},{nbv(2,1)},{nbv(3,1)}]]),
00175   assert(f([2],0) = [[],[]]),
00176   assert(f([2],1) = [[],[]]),
00177   assert(f([2],2) = [[],[{}]]),
00178   assert(f([2],3) = [[],[{},{},{}]]),
00179   assert(f([2,3],0) = [[],[]]),
00180   assert(f([2,3],1) = [[nbv(2,1)],[]]),
00181   assert(f([2,3],2) = [[nbv(2,1),nbv(3,1)],[{-nbv(2,1),-nbv(3,1)}]]),
00182   assert(f([2,3],3) = [[nbv(2,1),nbv(3,1),nbv(5,1)],[{-nbv(2,1),-nbv(3,1)},{-nbv(2,1),-nbv(5,1)},{-nbv(3,1),-nbv(5,1)}]]),
00183   assert(f([2,3],4) = [[nbv(2,1),nbv(3,1),nbv(5,1),nbv(7,1)],[{-nbv(2,1),-nbv(3,1)},{-nbv(2,1),-nbv(5,1)},{-nbv(3,1),-nbv(5,1)},{-nbv(2,1),-nbv(7,1)},{-nbv(3,1),-nbv(7,1)},{-nbv(5,1),-nbv(7,1)},{nbv(3,1),nbv(5,1),nbv(7,1)}]]),
00184   /* XXX */
00185   true)$
00186 
00187 okltest_greentao_logarithmic_fcs(f) := (
00188 
00189   true)$
00190 
00191 okltest_greentao_reduced_fcl(f) := (
00192   /* XXX */
00193   true)$
00194 
00195 okltest_greentao_reduced_fcs(f) := (
00196   /* XXX */
00197   true)$
00198 
00199 okltest_greentao_reduced_strong_fcl(f) := (
00200 
00201   true)$
00202 
00203 okltest_greentao_reduced_strong_fcs(f) := (
00204 
00205   true)$
00206 
00207 
00208 /* *********************
00209    * Symmetry breaking *
00210    *********************
00211 */
00212 
00213 okltest_greentao2_sb_fcs(f) := (
00214   /* XXX */
00215   true)$
00216 
00217 okltest_greentao_sb_aloamo_fcs(f) := (
00218   assert(f([],2) = [{},{{}}]),
00219   assert(f([],3) = [{},{{}}]),
00220   assert(f([1],2) = [{nbv(2,1),nbv(3,1)},{{-nbv(2,1)},{-nbv(3,1)},{nbv(2,1)},{nbv(3,1)}}]),
00221   assert(f([1,1],2) = [
00222  {nbv(2,1),nbv(3,1),nbv(2,2),nbv(3,2)},
00223  {{-nbv(2,1)},{-nbv(3,1)}, {-nbv(2,2)},{-nbv(3,2)},
00224   {nbv(2,1),nbv(2,2)},{nbv(3,1),nbv(3,2)},
00225   {-nbv(2,1),-nbv(2,2)},{-nbv(3,1),-nbv(3,2)}, 
00226   {nbv(3,1)}}]),
00227   assert(f([1,1,2,2],2) = [
00228  {nbv(2,1),nbv(3,1),nbv(2,2),nbv(3,2),nbv(2,3),nbv(3,3),nbv(2,4),nbv(3,4)},
00229  {{-nbv(2,1)},{-nbv(3,1)}, {-nbv(2,2)},{-nbv(3,2)},
00230   {-nbv(2,3),-nbv(3,3)}, {-nbv(2,4),-nbv(3,4)},
00231   {nbv(2,1),nbv(2,2),nbv(2,3),nbv(2,4)},{nbv(3,1),nbv(3,2),nbv(3,3),nbv(3,4)},
00232  {-nbv(2,1),-nbv(2,2)},{-nbv(2,1),-nbv(2,3)},{-nbv(2,1),-nbv(2,4)},{-nbv(2,2),-nbv(2,3)},{-nbv(2,2),-nbv(2,4)},{-nbv(2,3),-nbv(2,4)},
00233  {-nbv(3,1),-nbv(3,2)},{-nbv(3,1),-nbv(3,3)},{-nbv(3,1),-nbv(3,4)},{-nbv(3,2),-nbv(3,3)},{-nbv(3,2),-nbv(3,4)},{-nbv(3,3),-nbv(3,4)},
00234  {nbv(3,1),nbv(3,3)}}]),
00235   /* XXX */
00236   true)$
00237 
00238 okltest_greentaod_sb_nbfcsud(f) := (
00239   /* XXX */
00240   true)$
00241 
00242 
00243 /* ************************
00244    * Statistics functions *
00245    ************************
00246 */
00247 
00248 
00249 /* *******************
00250    * Standardisation *
00251    *******************
00252 */
00253 
00254 testcases_empty_greentao_std : [
00255  [[],0], [[],1], [[],2]
00256 ]$
00257 testcases_nonempty_greentao_std : [
00258  [[0],0], [[0],1], [[0],2],
00259  [[0,0],0], [[0,0],1], [[0,0],2],
00260  [[0,1],0], [[0,1],1], [[0,1],2],
00261  [[0,0,1],0], [[0,0,1],1], [[0,0,1],2],
00262  [[1],0], [[1],1], [[1],2],
00263  [[0,1,2],0], [[0,1,2],1], [[0,1,2],2], [[0,1,2],3],
00264  [[2,2],0], [[2,2],1], [[2,2],2], [[2,2],3], [[2,2],4],
00265  [[2,3],0], [[2,3],1], [[2,3],2], [[2,3],3], [[2,3],4],
00266  [[2,3,4],0], [[2,3,4],1], [[2,3,4],2], [[2,3,4],3], [[2,3,4],4], [[2,3,4],5], [[2,3,4],6], [[2,3,4],7], [[2,3,4],8], [[2,3,4],9], [[2,3,4],10]
00267 ]$
00268 
00269 okltest_greentao_aloamo_stdfcl(f) := (
00270   assert(f([],0) = [[[],[]],[]]),
00271   for T in 
00272       append(testcases_empty_greentao_std,testcases_nonempty_greentao_std) do
00273     assert(apply(f,T) = standardise_fcl(apply(greentao_aloamo_fcl,T))),
00274   true)$
00275 
00276 okltest_greentao_standnest_stdfcl(f) := (
00277   assert(f([],0) = [[[],[]],[]]),
00278   for T in testcases_nonempty_greentao_std do
00279     assert(apply(f,T) = standardise_fcl(apply(greentao_standnest_fcl,T))),
00280   true)$
00281 
00282 okltest_greentao_standnest_strong_stdfcl(f) := (
00283   assert(f([],0) = [[[],[]],[]]),
00284   for T in testcases_nonempty_greentao_std do
00285     assert(apply(f,T) = standardise_fcl(apply(greentao_standnest_strong_fcl,T))),
00286   true)$
00287 
00288 okltest_greentao_logarithmic_stdfcl(f) := (
00289   assert(f([],0) = [[[],[]],[]]),
00290   for T in testcases_nonempty_greentao_std do
00291     assert(apply(f,T) = standardise_fcl(apply(greentao_logarithmic_fcl,T))),
00292   true)$
00293 
00294 okltest_greentao_reduced_stdfcl(f) := (
00295   assert(f([],0) = [[[],[]],[]]),
00296   for T in testcases_nonempty_greentao_std do
00297     assert(apply(f,T) = standardise_fcl(apply(greentao_reduced_fcl,T))),
00298   true)$
00299 
00300 okltest_greentao_reduced_strong_stdfcl(f) := (
00301   assert(f([],0) = [[[],[]],[]]),
00302   for T in testcases_nonempty_greentao_std do
00303     assert(apply(f,T) = standardise_fcl(apply(greentao_reduced_strong_fcl,T))),
00304   true)$
00305 
00306 
00307 /* ********************
00308    * Output functions *
00309    ********************
00310 */
00311 
00312