OKlibrary  0.2.1.6
HittingClauseSets.mac
Go to the documentation of this file.
00001 /* Oliver Kullmann, 12.2.2008 (Swansea) */
00002 /* Copyright 2008, 2009, 2010, 2011, 2012, 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/Generators/Generators.mac")$
00024 oklib_include("OKlib/ComputerAlgebra/Satisfiability/Lisp/MinimalUnsatisfiability/Deficiency2.mac")$
00025 oklib_include("OKlib/ComputerAlgebra/Satisfiability/Lisp/ClauseSets/BasicOperations.mac")$
00026 oklib_include("OKlib/ComputerAlgebra/Satisfiability/Lisp/ConflictCombinatorics/HittingClauseSets.mac")$
00027 oklib_include("OKlib/ComputerAlgebra/Hypergraphs/Lisp/SetSystems.mac")$
00028 oklib_include("OKlib/ComputerAlgebra/Satisfiability/Lisp/Symmetries/Symmetries.mac")$
00029 oklib_include("OKlib/ComputerAlgebra/DataStructures/Lisp/HashMaps.mac")$
00030 oklib_include("OKlib/ComputerAlgebra/Satisfiability/Lisp/Reductions/DP-Reductions.mac")$
00031 oklib_include("OKlib/ComputerAlgebra/Satisfiability/Lisp/ClauseSets/Statistics.mac")$
00032 oklib_include("OKlib/ComputerAlgebra/Satisfiability/Lisp/ClauseSets/Hypergraphs.mac")$
00033 oklib_include("OKlib/ComputerAlgebra/Satisfiability/Lisp/Symmetries/Symmetries.mac")$
00034 oklib_include("OKlib/ComputerAlgebra/Satisfiability/Lisp/ClauseSets/Substitutions.mac")$
00035 oklib_include("OKlib/ComputerAlgebra/Satisfiability/Lisp/MinimalUnsatisfiability/DeficiencyOne.mac")$
00036 oklib_include("OKlib/ComputerAlgebra/Satisfiability/Lisp/MinimalUnsatisfiability/Deficiency2.mac")$
00037 oklib_include("OKlib/ComputerAlgebra/Satisfiability/Lisp/Primality/PrimeImplicatesImplicants.mac")$
00038 oklib_include("OKlib/ComputerAlgebra/Satisfiability/Lisp/Reductions/Hardness.mac")$
00039 
00040 kill(f)$
00041 
00042 /* *******************
00043    * Representations *
00044    *******************
00045 */
00046 
00047 okltest_hitting_cls_rep_st(f) := block(
00048   assert(f([true]) = [{},{{}}]),
00049   assert(f([false]) = [{{}}, {}]),
00050   assert(f([1,[false],[false]]) = [{{1},{-1}},{}]),
00051   assert(f([1,[false],[true]]) = [{{1}},{{1}}]),
00052   assert(f([1,[true],[false]]) = [{{-1}},{{-1}}]),
00053   assert(f([1,[true],[true]]) = [{},{{-1},{1}}]),
00054   true)$
00055 
00056 
00057 /* **************
00058    * Generators *
00059    **************
00060 */
00061 
00062 okltest_uniform_usat_hitting_min(f) := (
00063   assert(f(0) = {{}}),
00064   assert(f(1) = {{trv([])},{-trv([])}}),
00065   assert(f(2) = {{trv([]),trv([1])},{trv([]),-trv([1])},{-trv([]),trv([2])},{-trv([]),-trv([2])}}),
00066   assert(f(3) = {{trv([]),trv([1]),trv([1,1])},{trv([]),trv([1]),-trv([1,1])},{trv([]),-trv([1]),trv([1,2])},{trv([]),-trv([1]),-trv([1,2])},{-trv([]),trv([2]),trv([2,1])},{-trv([]),trv([2]),-trv([2,1])},{-trv([]),-trv([2]),trv([2,2])},{-trv([]),-trv([2]),-trv([2,2])}}),
00067 
00068   true)$
00069 
00070 okltest_over_full_hitting_fcs(f) := (
00071   for m : 2 thru 5 do block([FF : f(m)],
00072     assert(FF[1] = setn(m+1)),
00073     assert(ncl_fcs(FF) = 2^m+2),
00074     assert(check_hitting_nsing_def(FF[2]) = [2^m-m+1]),
00075     assert(min_variable_degree_cs(FF[2]) = 2^m)
00076   ),
00077   true)$
00078 
00079 okltest_smusat_horn_cs(f) := (
00080   assert(f(0) = {{}}),
00081   assert(f(1) = {{-trv([])},{trv([])}}),
00082   assert(f(2) = {{-trv([]),-trv([2])},{-trv([]),trv([2])},{trv([])}}),
00083   assert(f(3) = {{-trv([]),-trv([2]),-trv([2,2])},{-trv([]),-trv([2]),trv([2,2])},{-trv([]),trv([2])},{trv([])}}),
00084   assert(okltest_smusat_horn_stdfcs(buildq([f], lambda([k], cs2fcs((ev(f(k), trv(L):=length(L)+1, trv)))))) = true),
00085   true)$
00086 
00087 okltest_smusat_horn_stdfcl(f) := (
00088   assert(f(0) = [[],[{}]]),
00089   assert(f(1) = [[1],[{1},{-1}]]),
00090   assert(f(2) = [[1,2],[{1},{-1,2},{-1,-2}]]),
00091   assert(f(3) = [[1,2,3],[{1},{-1,2},{-1,-2,3},{-1,-2,-3}]]),
00092   true)$
00093 
00094 okltest_smusat_horn_stdfcs(f) := (
00095   assert(f(0) = [{},{{}}]),
00096   assert(f(1) = [{1},{{1},{-1}}]),
00097   assert(f(2) = [{1,2},{{1},{-1,2},{-1,-2}}]),
00098   assert(f(3) = [{1,2,3},{{1},{-1,2},{-1,-2,3},{-1,-2,-3}}]),
00099   true)$
00100 
00101 okltest_nvar_smusat_horn(f) := (
00102   for k : 0 thru 5 do block([n : f(k)],
00103     assert(n = nvar_cs(smusat_horn_cs(k))),
00104     assert(n = nvar_fcl(smusat_horn_stdfcl(k)))
00105   ),
00106   true)$
00107 
00108 okltest_ncl_smusat_horn(f) := (
00109   for k : 0 thru 5 do block([c : f(k)],
00110     assert(c = ncl_cs(smusat_horn_cs(k))),
00111     assert(c = ncl_fcl(smusat_horn_stdfcl(k)))
00112   ),
00113   true)$
00114 
00115 okltest_ncl_list_smusat_horn(f) := (
00116   for k : 0 thru 5 do block([cl : f(k)],
00117     assert(cl = ncl_list_cs(smusat_horn_cs(k))),
00118     assert(cl = ncl_list_fcl(smusat_horn_stdfcl(k)))
00119   ),
00120   true)$
00121 
00122 okltest_nlitocc_smusat_horn(f) := (
00123   for k : 0 thru 5 do block([l : f(k)],
00124     assert(l = nlitocc_cs(smusat_horn_cs(k))),
00125     assert(l = nlitocc_fcl(smusat_horn_stdfcl(k)))
00126   ),
00127   true)$
00128 
00129 okltest_smusat_genhorn_cs(f) := block([x],
00130   assert(f(0,x) = {{}}),
00131   assert(f(x,0) = {{}}),
00132   assert(f(1,1) = {{trv([])},{-trv([])}}),
00133   assert(okltest_smusat_horn_cs(buildq([f], lambda([k], f(k,1)))) = true),
00134   assert(f(1,2) = {{trv([])},{-trv([])}}),
00135   assert(okltest_uniform_usat_hitting_min(buildq([f], lambda([k], f(k,k)))) = true),
00136   true)$
00137 
00138 okltest_sat_genhorn_cs(f) := (
00139   for k : 0 thru 3 do
00140    for l : 0 thru 3 do block([F : f(k,l), c, P],
00141      c : ncl_cs(F),
00142      assert(c = ncl_cs(smusat_genhorn_cs(k,l))),
00143      assert(deficiency_cs(F) = 1 - c),
00144      assert(hitting1rcsp(F) = true),
00145      if oklib_test_level > 0 then (
00146        P : min_resolution_closure_cs(F)[1],
00147        assert(ncl_cs(P) = 2^c-1),
00148        assert(hardness_wpi_cs(F,P) = min(k,l))
00149      )
00150   ),
00151   true)$
00152 
00153 okltest_ext1_sat_genhorn_cs(f) := (
00154   for l : 0 thru cokltl(3,5) do
00155     for n : 0 thru cokltl(4,7) do block([F : f(n,l)],
00156       assert(hitting1rcsp(F) = true),
00157       assert(sat_decision_hitting_cs(F) = false)
00158   ),
00159   true)$
00160 
00161 okltest_sasg2000(FF) := block([F : FF[2]],
00162   assert(FF[1] = {1,2,3,4}),
00163   assert(not treehittingcsp(F)),
00164   assert(literalregularcsp(F)),
00165   assert(min_literal_degree_cs(F) = 3),
00166   assert(max_variable_frequency_cs(F) = 3/4),
00167   assert(abd_parameters(F) = [4,3]),
00168   true)$
00169 
00170 okltest_brouwer1999(FF) := block([F : FF[2]],
00171   assert(FF[1] = setn(8)),
00172   assert(not treehittingcsp(F)),
00173   assert(literalregularcsp(F)),
00174   assert(min_literal_degree_cs(F) = 10),
00175   assert(max_variable_frequency_cs(F) = 5/8),
00176   assert(abd_parameters(F) = [8,5]),
00177   true)$
00178 
00179 okltest_max_var_hitting_def(f) := (
00180   for k : 2 thru 5 do ([FF : f(k)],
00181     assert(hittingcsp(FF[2]) = true),
00182     assert(sat_decision_hitting_cs(FF[2]) = false),
00183     assert(nonsingular_csp(FF[2]) = true),
00184     assert(deficiency_fcs(FF) = k),
00185     assert(nvar_f(FF) = 3 + (k-2) * 4)
00186   ),
00187   true)$
00188 
00189 okltest_nvar_max_var_hitting_def(f) := (
00190   assert(f(2) = 3),
00191   assert(f(3) = 7),
00192   for k : 2 thru 5 do ([FF : f(k)],
00193     assert(f(k) = nvar_f(max_var_hitting_def(k)))),
00194   true)$
00195 
00196 okltest_max_var_hittingdef2_cs(f) := (
00197   for h : 2 thru 5 do ([FF : f(h)],
00198     assert(hittingcsp(FF[2]) = true),
00199     assert(sat_decision_hitting_cs(FF[2]) = false),
00200     assert(nonsingular_csp(FF[2]) = true),
00201     assert(deficiency_fcs(FF) = def_max_var_hittingdef2_cs(h)),
00202     assert(nvar_f(FF) = nvar_max_var_hittingdef2_cs(h))
00203   ),
00204   true)$
00205 
00206 okltest_all_hitting_extensions_k_fcs(f) := block([X],
00207   assert(f(X,-1) = {}),
00208   assert(f(X,0) = X),
00209   assert(f({},1) = {}),
00210   assert(f({[{},{}]},1) = {}),
00211   assert(f({[{},{{}}]},1) = { [{1},{{-1},{1}}] }),
00212   assert(f({[{},{{}}]},2) = { [{1,2},{{-1,-2},{-1,2},{1}}], [{1,2},{{1,-2},{1,2},{-1}}], [{1,2},{{1,-2},{-1,-2},{2}}] }),
00213   for k : 0 thru if oklib_test_level=0 then 2 else 3 do 
00214    block([H : f({[{},{{}}]},k), S : all_smusat1_cs(k)],
00215     assert(map(fcs2cs,lunion(map(all_renamings_fcs,H))) = setify(S))
00216   ),
00217   true)$
00218 
00219 okltest_all_reps_hitting_extensions_k_fcs(f) := block([X],
00220   assert(f(X,-1) = {}),
00221   assert(f({},0) = {}),
00222   assert(f({[{},{}]},0) = {[{},{}]}),
00223   assert(f({ [{1},{{1},{-1}}], [{2},{{2},{-2}}] },0) = {[{1},{{1},{-1}}]}),
00224   assert(f({},1) = {}),
00225   assert(f({[{},{}]},1) = {}),
00226   assert(f({[{},{{}}]},1) = { [{1},{{-1},{1}}] }),
00227   assert(f({[{},{{}}]},2) = { [{1,2},{{-1,-2},{1,-2},{2}}] }),
00228   true)$
00229 
00230 
00231 /* *********
00232    * Tests *
00233    *********
00234 */
00235 
00236 okltest_sat_decision_hitting_cs(f) := (
00237   assert(f({}) = true),
00238   assert(f({{}}) = false),
00239   assert(f({{1}}) = true),
00240   for n : 0 thru 3 do
00241     assert(f(full_fcs(n)[2]) = false),
00242   true)$
00243 
00244 okltest_hittingcsp(f) := block(
00245   assert(f({}) = true),
00246   assert(f({{}}) = true),
00247   assert(f({{1}}) = true),
00248   assert(f({{},{1}}) = false),
00249   for n : 2 thru 4 do
00250     assert(f(musatd2_fcs(n)[2]) = if n <= 3 then true else false),
00251   assert(f({{1},{-1}}) = true),
00252   for n : 0 thru 4 do
00253     assert(f(uniform_usat_hitting_min(n))),
00254   for n : 0 thru 4 do
00255     assert(f(uniform_usat_hitting_max(n))),
00256   true)$
00257 
00258 okltest_hitting1rcsp(f) := block(
00259   assert(f({}) = true),
00260   assert(f({{}}) = true),
00261   assert(f({{1}}) = true),
00262   assert(f({{},{1}}) = false),
00263   for n : 2 thru 4 do
00264     assert(f(musatd2_fcs(n)[2]) = false),
00265   assert(f({{1},{-1}}) = true),
00266   for n : 0 thru 4 do
00267     assert(f(uniform_usat_hitting_min(n)) = true),
00268   for n : 0 thru 4 do
00269     assert(f(uniform_usat_hitting_max(n)) = if n<=1 then true else false),
00270   true)$
00271 
00272 okltest_treehittingcsp(f) := block(
00273   assert(f({}) = false),
00274   assert(f({{}}) = true),
00275   assert(f({{1}}) = false),
00276   assert(f({{},{1}}) = false),
00277   assert(f({{1},{-1}}) = true),
00278   for n : 2 thru 4 do
00279     assert(f(musatd2_fcs(n)[2]) = if n <= 2 then true else false),
00280   for n : 0 thru 4 do
00281     assert(f(uniform_usat_hitting_min(n))),
00282   for n : 0 thru 4 do
00283     assert(f(uniform_usat_hitting_max(n))),
00284   true)$
00285 
00286 okltest_check_hitting_nsing_def(f) := block(
00287   assert(f({{}}) = [1]),
00288   assert(f({}) = []),
00289   assert(f({{1},{-1}}) = []),
00290   assert(f(musatd2_fcs(2)[2]) = [2]),
00291   assert(f(musatd2_fcs(3)[2]) = [2]),
00292   assert(f(musatd2_fcs(4)[2]) = []),
00293   assert(f({{1,2,3},{-1,2,3},{1,-2,3},{-1,-2,3},{1,-3},{-1,-3}}) = [3]),
00294   assert(f({{1,2,3},{-1,2,3},{1,-2,4}, {-1,-2,4},{2,-3,5},{2,-3,-5},{-2,-4,5},{-2,-4,-5}}) = [3]),
00295   assert(f({{1,2,3},{1,-2,3},{1,2,-3},{1,-2,-3},{-1,4,5},{-1,-4,5},{-1,4,-5},{-1,-4,-5}}) = [3]),
00296   assert(f(full_fcs(3)[2]) = [5]),
00297   true)$
00298 
00299 
00300 /* **************************************************************
00301    * Necessary conditions for unsatisfiable hitting clause-sets *
00302    **************************************************************
00303 */
00304 
00305 okltest_all_cld_uhit(f) := block(
00306   assert(f(1,0,0) = {{[0,1]}}),
00307   assert(f(1,0,1) = {}),
00308   assert(f(1,0,2) = {}),
00309   assert(f(1,1,0) = {{[1,2]}}),
00310   assert(f(1,1,1) = {}),
00311   assert(f(1,1,2) = {}),
00312   assert(f(1,2,0) = {}),
00313   assert(f(1,2,1) = {{[1,1],[2,2]}}),
00314   assert(f(1,2,2) = {}),
00315   assert(f(1,2,3) = {}),
00316   assert(f(1,3,0) = {}),
00317   assert(f(1,3,1) = {}),
00318   true)$
00319 
00320 okltest_all_cld_uhit_minvd(f) := block(
00321   assert(f(6,4,9) = {{[2,2],[4,8]}}),
00322   assert(f(6,5,9) = {{[1,1],[3,1],[4,3],[5,6]},{[1,1],[3,2],[5,8]},{[1,1],[4,6],[5,4]},{[2,3],[5,8]}}),
00323   true)$
00324 
00325 okltest_all_cld_uhit_maxminvd(f) := block(
00326   assert(f(6,4) = {{[2,2],[4,8]}}),
00327   assert(f(6,5) = {{[1,1],[3,1],[4,3],[5,6]},{[1,1],[3,2],[5,8]},{[1,1],[4,6],[5,4]},{[2,3],[5,8]}}),
00328   true)$
00329 
00330 /* ****************************************************
00331    * Representing clause-sets via hitting clause-sets *
00332    ****************************************************
00333 */
00334 
00335 okltest_hitting_decomposition_m_cs(f) := block(
00336   assert(f({}) = []),
00337   assert(f({{}}) = [{{}}]),
00338   assert(f({{1}}) = [{{1}}]),
00339   assert(f({{1},{-1}}) = [{{1},{-1}}]),
00340   assert(setify(f({{1},{-1},{}})) = {{{1},{-1}},{{}}}),
00341   assert(setify(f({{-1},{1},{2},{-2},{3},{-3}})) = {{{-1},{1}},{{-2},{2}},{{-3},{3}}}),
00342   true)$
00343 
00344 
00345 /* ********************************************************************
00346    * Finding hitting clause-sets with given deficiency "sporadically" *
00347    ********************************************************************
00348 */
00349 
00350 okltest_all_hittinginstances_def(f) := block(
00351   assert(f({},0) = {{}}),
00352   assert(f({},1) = {}),
00353   assert(f({{}},0) = {}),
00354   assert(f({{}},1) = {{{}}}),
00355   assert(f({{1}},0) = {{},{{1}}}),
00356   assert(f({{1}},1) = {{{}}}),
00357   assert(f({{1}},2) = {}),
00358   assert(f({{1},{-1}},0) = {}),
00359   assert(f({{1},{-1}},1) = {{{}},{{1},{-1}}}),
00360   assert(f({{1},{-1}},2) = {}),
00361   assert(f({{1},{-1}},3) = {}),
00362   true)$
00363 
00364 okltest_all_hitting_DP_reductions_def(f) := block(
00365  [List : [
00366    [[{},0], {{}}], 
00367    [[{},1], {}], 
00368    [[{{}},0], {}],
00369    [[{{}},1], {{{}}}],
00370    [[{{1}},0], {{},{{1}}}],
00371    [[{{1}},1], {}],
00372    [[{{1}},2], {}],
00373    [[{{1},{-1}},0], {}],
00374    [[{{1},{-1}},1], {{{}},{{1},{-1}}}],
00375    [[{{1},{-1}},2], {}],
00376    [[full_fcs(2)[2],0], {}],
00377    [[full_fcs(2)[2],1], {{{}},{{1},{-1}},{{2},{-2}}}],
00378    [[full_fcs(2)[2],2], {full_fcs(2)[2]}],
00379    [[full_fcs(2)[2],3], {}]
00380   ]],
00381   for case in List do
00382     assert(apply(f,case[1]) = case[2]),
00383   for case in List do block(
00384    [presult, result],
00385     result : apply(f,endcons('presult,case[1])),
00386     assert(result = case[2]),
00387     assert(result = presult)
00388   ),
00389   for case in List do block(
00390    [presult, pc, result, n : nvar_cs(case[1][1])],
00391     result : apply(f,append(case[1],['presult,'pc])),
00392     assert(result = case[2]),
00393     assert(result = presult),
00394     assert(pc = if n = 0 then 0 else n!)
00395   ),
00396   for case in List do block(
00397    [presult, pc, result, n : nvar_cs(case[1][1])],
00398     pc : 0,
00399     result : apply(f,append(case[1],['presult,'pc])),
00400     assert(result = case[2]),
00401     assert(result = presult),
00402     assert(pc = if n = 0 then 0 else n!)
00403   ),
00404   for case in List do block(
00405    [presult, pc, result, F : case[1][1], k : case[1][2], n, def],
00406     n : nvar_cs(F),
00407     def : deficiency_cs(F),
00408     pc : n! + 1,
00409     result : apply(f,append(case[1],['presult,'pc])),
00410     assert(result = if def = k then {F} else {}),
00411     assert(result = presult),
00412     assert(pc = n!)
00413   ),
00414   true)$
00415 
00416 
00417 /* ********************************************************************
00418    * Finding hitting clause-sets with given deficiency systematically *
00419    ********************************************************************
00420 */
00421 
00422 okltest_derived_hitting_cs(f) := block([presult,result,F],
00423   result : f({},0,'presult), assert(result = {{}}), assert(presult = result),
00424   result : f({},1,'presult), assert(result = {}), assert(presult = result),
00425   result : f({{}},0,'presult), assert(result = {{{}}}), assert(presult = result),
00426   result : f({{}},1,'presult), assert(result = {}), assert(presult = result),
00427   result : f({{1}},0,'presult), assert(result = {{{1}}}), assert(presult = result),
00428   result : f({{1}},1,'presult), assert(result = {}), assert(presult = result),
00429   result : f({{1},{-1}},0,'presult), assert(result = {{{1},{-1}}}), assert(presult = result),
00430   result : f({{1},{-1}},1,'presult), assert(result = {}), assert(presult = result),
00431   result : f({{1},{-1}},2,'presult), assert(result = {}), assert(presult = result),
00432   F : full_fcs(2)[2],
00433   result : f(F,0,'presult),
00434   assert(result = {F}),
00435   assert(presult = result),
00436   result : f(F,1,'presult), assert(result = {{{1},{-1,2},{-1,-2}},{{-1},{1,2},{1,-2}},{{2},{-2,1},{-2,-1}},{{-2},{2,1},{2,-1}}}), assert(presult = result),
00437   result : f(F,2,'presult), assert(result = {}), assert(presult = result),
00438   true)$
00439 
00440 okltest_derived_hitting_cs_pred(f) := block([presult,result,P],
00441   okltest_derived_hitting_cs(buildq([f],lambda([F,k,r],
00442     f(F,k,r,buildq([F],lambda([G],is(nvar_cs(G) = nvar_cs(F)))))))),
00443   P : lambda([F], true),
00444   for n : 0 thru (if oklib_test_level = 0 then 2 else 3) do block(
00445    [F : full_fcs(n)[2]],
00446     result : f(F,2^n-1,'presult,P),
00447     assert(result = {{{}}}),
00448     assert(presult = result)
00449   ),
00450   true)$
00451 
00452 okltest_derived_hitting_cs_nsing(f) := block([presult,result,F],
00453   F : full_fcs(2)[2],
00454   result : f(F,0,'presult),
00455   assert(result = {F}),
00456   assert(presult = result),
00457   result : f(F,1,'presult),
00458   assert(result = {}),
00459   assert(presult = result),
00460   true)$
00461 
00462 okltest_all_derived_hitting_cs_nsing_isoelim(f) := block([repo,M:{},FF],
00463   repo : sm2hm({}),
00464   FF : [{},{}],
00465   assert(f(FF[2],repo) = 1),
00466   M : adjoin([fcs_identifier(FF), {FF}],M),
00467   assert(hm2sm(repo) = M),
00468   assert(f(FF[2],repo) = 0),
00469   assert(hm2sm(repo) = M),
00470   FF : [{},{{}}],
00471   assert(f(FF[2],repo) = 1),
00472   M : adjoin([fcs_identifier(FF), {FF}],M),
00473   assert(hm2sm(repo) = M),
00474   assert(f(FF[2],repo) = 0),
00475   assert(hm2sm(repo) = M),
00476   FF : full_fcs(2),
00477   assert(f(FF[2],repo) = 1),
00478   M : adjoin([fcs_identifier(FF), {FF}],M),
00479   assert(hm2sm(repo) = M),
00480   assert(f(FF[2],repo) = 0),
00481   assert(hm2sm(repo) = M),
00482   assert(length(M) = 3),
00483   repo : sm2hm({}),
00484   FF : full_fcs(3),
00485   assert(f(FF[2],repo) = 1 + 3 + 1 + 1),
00486   assert(analyse_isorepo_def(repo) = [[2,1],[3,3],[4,1],[5,1]]),
00487   true)$
00488 
00489 okltest_all_unsinghitting_def(f) := block([presult,result],
00490   result : f(0,0,'presult), assert(result = {}), assert(presult = result),
00491   result : f(0,1,'presult), assert(result = {}), assert(presult = result),
00492   result : f(1,0,'presult), assert(result = {{{}}}), assert(presult = result),
00493   result : f(2,0,'presult), assert(result = {}), assert(presult = result),
00494   result : f(2,1,'presult), assert(result = {}), assert(presult = result),
00495   result : f(2,2,'presult), assert(result = {full_fcs(2)[2]}), assert(presult = result),
00496   result : f(5,3,'presult), assert(result = {full_fcs(3)[2]}), assert(presult = result),
00497   result : f(2,3,'presult), 
00498   assert(length(result) = 1),
00499   assert(is_isomorphic_cs(single_element(result), musatd2_fcs(3)[2])),
00500   assert(subsetp(result,presult) = true),
00501   result : f(4,3,'presult),
00502   assert(length(result) = 1), assert(presult = result),
00503   assert(is_isomorphic_cs(single_element(result), {{-3,-2,-1},{-3,-2,1},{-3,-1,2},{-2,-1,3},{-2,1,3},{-1,2,3},{1,2}})),
00504   true)$
00505 
00506 
00507 /* ***********************************************************
00508    * Finding hitting clause-sets with given n systematically *
00509    ***********************************************************
00510 */
00511 
00512 okltest_all_unsinghitting(f) := block([hash],
00513   assert(f(2,'hash) = 1),
00514   assert(analyse_isorepo_def(hash) = [[2,1]]),
00515   assert(f(3,'hash) = 1 + 3 + 1 + 1),
00516   assert(analyse_isorepo_def(hash) = [[2,1],[3,3],[4,1],[5,1]]),
00517   true)$
00518 
00519 
00520 /* ***************************
00521    * Maximal min-var-degrees *
00522    ***************************
00523 */
00524 
00525 okltest_max_min_var_deg_uhit_def(f) := (
00526   assert(f(7) = 10),
00527   true)$
00528 
00529 /* *************************
00530    * Resolution complexity *
00531    *************************
00532 */
00533 
00534 okltest_min_nssplittree_isot(f) := (
00535   assert(f[[[1,0],1]] = 1),
00536   /* XXX */
00537   true)$
00538 
00539 okltest_min_nssplittree_def(f) := block(
00540   assert(f(1) = [1]),
00541   assert(f(2) = [2,2]),
00542   assert(f(3) = [2,2,2,2,3,2,2,2,3,2,2,2,3,4,2,3,3,3,3,3,3,3,4,3,3,3,4]),
00543   true)$
00544 
00545 
00546 /* ****************************
00547    * Primes and factorisation *
00548    ****************************
00549 */
00550 
00551 okltest_primeuhitting_p(f) := (
00552   assert(f({{}}) = true),
00553   assert(f({{1},{-1}}) = true),
00554   for n : 2 thru 5 do
00555     assert(f(full_cs(n)) = false),
00556   assert(f(musatd2_cs(2)) = false),
00557   assert(f(musatd2_cs(3)) = true),
00558   true)$
00559