OKlibrary  0.2.1.6
MinVarDegrees.mac
Go to the documentation of this file.
00001 /* Oliver Kullmann, 16.4.2011 (Guangzhou) */
00002 /* Copyright 2011, 2013 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/MinimalUnsatisfiability/MinVarDegrees.mac")$
00024 
00025 
00026 kill(f)$
00027 
00028 
00029 /* **************************
00030    * Number of full clauses *
00031    **************************
00032 */
00033 
00034 okltest_fullclauses_dmu_lb1(f) := (
00035   assert(f[1] = 2),
00036   assert(f[2] = 4),
00037   assert(f[3] = 4),
00038   true)$
00039 
00040 okltest_index_Sma_S2_rec(f) := block([N],
00041   N : cokltl(100,1000),
00042   assert(create_list(2*(k+1-f(k)),k,2,N) = rest(Sma_S2_list(N+1),2)),
00043   true)$
00044 
00045 okltest_Sma_S2_replica(f) := (
00046   for k : 0 thru cokltl(100,1000) do
00047     assert(f(k) = Sma_S2_list(k)),
00048   true)$
00049 
00050 okltest_fullclauses_dmu_lb1_gen(f) := block([N],
00051   for k : 1 thru cokltl(100,1000) do
00052     assert(f[k,2] = fullclauses_dmu_lb1[k]),
00053   N : cokltl(100,1000),
00054   for d : 2 thru cokltl(10,30) do
00055     assert(create_list(f[k,d],k,1,N) = rest(Sma_list(N+1,d))),
00056   true)$
00057 
00058 okltest_Sma_S2_list(f) := (
00059   assert(f(0) = []),
00060   assert(f(21) = [0,2,4,4,6,8,8,8,10,12,12,14,16,16,16,16,18,20,20,22,24]),
00061   true)$
00062 
00063 okltest_Sma_bydef(f) := (
00064   for k: 0 thru 20 do
00065     assert(f(k,1) = 0),
00066   for d : 2 thru cokltl(40,1000) do (
00067     assert(f(0,d) = 0),
00068     if primep(d) then
00069       assert(f(1,d) = d)
00070     else block([L : ifactors(d), res],
00071       res : lmax(create_list(f(p[2],p[1]), p,L)),
00072       assert(f(1,d) = res)
00073     )
00074   ),
00075   assert(create_list(f(k,2),k,0,20) = [0,2,4,4,6,8,8,8,10,12,12,14,16,16,16,16,18,20,20,22,24]),
00076   assert(create_list(f(k,3),k,0,20) = [0,3,6,9,9,12,15,18,18,21,24,27,27,27,30,33,36,36,39,42,45]),
00077   assert(create_list(f(k,5),k,0,20) = [0,5,10,15,20,25,25,30,35,40,45,50,50,55,60,65,70,75,75,80,85]),
00078   true)$
00079 
00080 okltest_Sma_start(f) := (
00081   for d : 2 thru cokltl(100,1000) do
00082     assert(Sma_bydef(1,d) = f(d)),
00083   true)$
00084 
00085 okltest_Sma_list(f) := block([D,N],
00086   for k : 0 thru cokltl(100,500) do
00087     assert(f(k,2) = Sma_S2_list(k)),
00088   D : cokltl(15,40,100),
00089   N : cokltl(2,4)*D,
00090   for d : 2 thru D do
00091     if primep(d) then
00092       assert(f(N,d) = create_list(Sma_bydef(k,d), k, 0,N-1)),
00093   true)$
00094 
00095 okltest_Sma_replica(f) := block([D,N],
00096   D : cokltl(20,100),
00097   N : cokltl(100,1000),
00098   for d : 2 thru D do
00099     assert(f(N,d) = Sma_list(N,d)),
00100   true)$
00101 
00102 
00103 /* ***************************
00104    * Maximal min-var-degrees *
00105    ***************************
00106 */
00107 
00108 okltest_order_deficiency(f) := (
00109   assert(map(f,create_list(i,i,1,13)) = [0,2,3,3,3,4,4,4,4,4,4,4,5]),
00110   for n : 2 thru 10 do
00111     assert(f(2^n-n) = n),
00112   true)$
00113 
00114 /* **************************************
00115    * (Generalised) non-Mersenne numbers *
00116    **************************************
00117 */
00118 
00119 okltest_nonmersenne_rec(f) := (
00120   assert(f[1] = 2),
00121   assert(f[2] = 4),
00122   assert(f[3] = 5),
00123   assert(f[4] = 6),
00124   assert(f[5] = 8),
00125   assert(f[6] = 9),
00126   assert(f[7] = 10),
00127   assert(f[8] = 11),
00128   assert(f[9] = 12),
00129   assert(f[10] = 13),
00130   assert(f[11] = 14),
00131   assert(f[12] = 16),
00132   for n : 1 thru 6 do
00133     assert(f[2^n-n] = 2^n),
00134   true)$
00135 
00136 okltest_nonmersenne_law(f) := (
00137   for k : 1 thru cokltl(30,100,200) do
00138     assert(f(k) = nonmersenne_rec[k]),
00139   true)$
00140 
00141 okltest_nonmersenne_lb(f) := (
00142   assert(f(1) = 2),
00143   assert(f(2) = 3),
00144   assert(f(3) = 5),
00145   assert(f(4) = 6),
00146   true)$
00147 
00148 okltest_nonmersenne_ub(f) := (
00149   assert(f(1) = 2),
00150   assert(f(2) = 4),
00151   assert(f(3) = 5),
00152   assert(f(4) = 7),
00153   true)$
00154 
00155 okltest_nonmersenne_dary_jump0(f) := (
00156   for k : 1 thru 100 do
00157     assert(f(k,1) = k),
00158   for k : 1 thru 100 do
00159     assert(f(k,2) = nonmersenne(k)),
00160   assert(create_list(f(k,3),k,1,22) = [3,4,5,6,9,10,11,12,13,14,15,16,17,18,19,20,21,22,23,24,27,28]),
00161   true)$
00162 
00163 okltest_nonmersenne_dary_rec(f) := (
00164   for k : 1 thru 200 do
00165     assert(f[k,2] = nonmersenne(k)),
00166   for d : 3 thru cokltl(5,12) do
00167     for k : 1 thru cokltl(5,50) * d do
00168       assert(f[k,d] = nonmersenne_dary_jump_bydef(k,d)),
00169   true)$
00170 
00171 okltest_analyse_nonmersenne_rec(f) := (
00172   assert(f(1) = []),
00173   assert(f(2) = [[2,1,"ab"]]),
00174   assert(f(3) = [[3,1,"b"]]),
00175   assert(f(4) = [[3,"a"],[4,1,"b"]]),
00176   assert(f(5) = [[4,2,"ab"]]),
00177   true)$
00178 
00179 okltest_index_nonmersenne_rec(f) := (
00180   assert(f(2) = 2),
00181   assert(f(3) = 3),
00182   assert(f(4) = 4),
00183   assert(f(5) = 4),
00184   true)$
00185 
00186 okltest_step_nonmersenne_rec(f) := (
00187   assert(f(2) = [1,0,1,0]),
00188   assert(f(3) = [1,0,1,1]),
00189   assert(f(4) = [2,2,0,2]),
00190   true)$
00191 
00192 okltest_possible_degree_pairs_nm(f) := (
00193   assert(f(2,4) = [[[2,2],[1,4,1,4]]]),
00194   assert(f(3,4) = [[[2,2],[2,6,2,6]]]),
00195   assert(f(3,5) = [[[2,3],[2,6,1,5]]]),
00196   assert(f(4,4) = [[[2,2],[3,7,3,7]]]),
00197   assert(f(4,5) = [[[2,3],[3,7,2,7]]]),
00198   assert(f(4,6) = [[[2,4],[3,7,1,6]],[[3,3],[2,7,2,7]]]),
00199   assert(f(6,9) = [[[4,5],[3,9,2,9]]]),
00200   for k : 2 thru cokltl(30,200) do block(
00201    [i : index_nonmersenne_rec(k)],
00202     assert(elementp([nonmersenne(k-i+1),i], setify(map(first,f(k,nonmersenne(k))))) = true),
00203     assert(f(k,nonmersenne(k)+1) = [])
00204   ),
00205   true)$
00206 
00207 okltest_possible_degree_pairs_gen(f) := (
00208   assert(okltest_possible_degree_pairs_nm(buildq([f], lambda([k,m], f(k,m,nonmersenne)))) = true),
00209   /* XXX */
00210   true)$
00211 
00212 okltest_nonmersenne_op(f) := (
00213   assert(okltest_nonmersenne_law(buildq([f], lambda([k], f[k,[2]]))) = true),
00214   /* XXX */
00215   true)$
00216 
00217 okltest_nonmersenne_gen_rec(f) := (
00218   assert(okltest_nonmersenne_law(buildq([f], lambda([k], f[k,0]))) = true),
00219   assert(f[6,1] = 8),
00220   assert(f[13,1] = 16),
00221   assert(f[28,1] = 32),
00222   assert(f[59,1] = 64),
00223   assert(f[14,2] = 17),
00224   assert(f[29,2] = 33),
00225   assert(f[60,2] = 65),
00226   true)$
00227 
00228 okltest_epoche_nonmersenne_gen(f) := (
00229   assert(map(f,create_list(i,i,1,14)) = [-1,0,0,0,0,1,1,1,1,1,1,1,1,2]),
00230   true)$
00231 
00232 okltest_nonmersenne_inf_rec(f) := (
00233   for k : 1 thru 60 do
00234     assert(f(k) = nonmersenne_gen_rec[k,k]),
00235   true)$
00236 
00237 okltest_nonmersenne_level(f) := (
00238   assert(map(f,create_list(i,i,1,12)) = [1,2,2,2,3,3,3,3,3,3,3,4]),
00239   true)$
00240 
00241