OKlibrary  0.2.1.6
DP-Reductions.mac
Go to the documentation of this file.
00001 /* Oliver Kullmann, 25.4.2008 (Guangzhou) */
00002 /* Copyright 2008, 2009, 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/Generators/Pigeonhole.mac")$
00025 oklib_include("OKlib/ComputerAlgebra/Satisfiability/Lisp/MinimalUnsatisfiability/DeficiencyOne.mac")$
00026 oklib_include("OKlib/ComputerAlgebra/Satisfiability/Lisp/ConflictCombinatorics/HittingClauseSets.mac")$
00027 oklib_include("OKlib/ComputerAlgebra/Satisfiability/Lisp/ClauseSets/Statistics.mac")$
00028 oklib_include("OKlib/ComputerAlgebra/Hypergraphs/Lisp/SetSystems.mac")$
00029 
00030 
00031 kill(f)$
00032 
00033 
00034 /* *************************
00035    * Singular DP-reduction *
00036    *************************
00037 */
00038 
00039 okltest_sdp_reduction_cs(f) := (
00040   assert(f({}) = {}),
00041   assert(f({{}}) = {{}}),
00042   assert(f({{1,2},{2,3},{-2,3},{-2,-3},{2},{-3}}) = {{1,2},{2,3},{-2,3},{-2,-3},{2},{-3}}),
00043   assert(f({{1,2},{1,-2},{2},{-2}}) = {{1,2},{1,-2},{2},{-2}}),
00044   for n : 0 thru 3 do block([F : full_fcs(n)[2]],
00045     assert(f(F) = if n <= 1 then {{}} else F)),
00046   for k : 0 thru 3 do block([F : marginal_musat1(k)],
00047     assert(f(F) = {{}})),
00048   for k : 0 thru 3 do block([F : uniform_usat_hitting_min(k)],
00049     assert(f(F) = {{}})),
00050   for k : 0 thru 3 do block([F : smusat_horn_cs(k)],
00051     assert(f(F) = {{}})),
00052   assert(nvar_cs(f(weak_php_cs(3,2))) = 3),
00053   true)$
00054 
00055 okltest_onesdp_reduction_cs(f) := (
00056   assert(f({}) = {}),
00057   assert(f({{}}) = {{}}),
00058   assert(f({{1,2},{2,3},{-2,3},{-2,-3},{2},{-3}}) = {{1,2},{2,3},{-2,3},{-2,-3},{2},{-3}}),
00059   assert(f({{1,2},{1,-2},{2},{-2}}) = {{1,2},{1,-2},{2},{-2}}),
00060   for n : 0 thru 3 do block([F : full_fcs(n)[2]],
00061     assert(f(F) = if n <= 1 then {{}} else F)),
00062   for k : 0 thru 3 do block([F : marginal_musat1(k)],
00063     assert(f(F) = {{}})),
00064   for k : 0 thru 3 do block([F : uniform_usat_hitting_min(k)],
00065     assert(f(F) = {{}})),
00066   for k : 0 thru 3 do block([F : smusat_horn_cs(k)],
00067     assert(f(F) = {{}})),
00068   assert(nvar_cs(f(weak_php_cs(3,2))) = 6),
00069   assert(f({{1,2,8},{-1,3,9},{-2,4},{-2,5},{-3,6},{-3,7}}) = {{2,3,8,9},{-2,4},{-2,5},{-3,6},{-3,7}}),
00070   true)$
00071 
00072 okltest_nononesingulartuple_cs(f) := (
00073   assert(f({}) = []),
00074   assert(f({{}}) = []),
00075   assert(f({{1}}) = []),
00076   assert(f({{1},{-1}}) = []),
00077   assert(f({{1},{-1,2},{-1,-2}}) = [1]),
00078   assert(f({{1,2},{2,3},{-2,3},{-2,-3},{2},{-3}}) = []),
00079   assert(f({{1,2,8},{-1,3,9},{-2,4},{-2,5},{-3,6},{-3,7}}) = [2,1]),
00080   true)$
00081 
00082 okltest_sdp_set_cs_bydef(f) := block(
00083   assert(f({}) = {{}}),
00084   assert(f({{}}) = {{{}}}),
00085   for k : 0 thru if oklib_test_level=0 then 2 else 3 do
00086    block([F : marginal_musat1(k)],
00087     assert(f(F) = {{{}}})),
00088   assert(f({{1,2},{-1,3},{-1,-3},{-2,3},{-2,-3}}) = {{{2,3},{-2,3},{2,-3},{-2,-3}}, {{1,3},{1,-3},{-1,3},{-1,-3}}}),
00089   assert(f({{5,6,1},{-5,2},{-5,6,-2},{6,-1,2},{6,-1,-2},{-6,3,4},{-6,3,-4},{-6,-3,4},{-6,-3,-4}}) = { {{6,1,2},{6,1,-2},{6,-1,2}, {6,-1,-2},{-6,3,4},{-6,3,-4},{-6,-3,4},{-6,-3,-4}}, {{-6,-4,-3},{-6,-4,3},{-6,-3,4},{-6,3,4},{-5,-2,6},{-5,2},{-2,5,6},{2,5,6}}}),
00090   if oklib_test_level=0 then return(true),
00091   assert(f({{1,2},{-1,3,5},{-1,4,6},{-2,3,5},{-2,4,6},{-3,5},{-4,6},{-5,-6}}) = { {{2,6},{-2,6},{2,-6},{-2,-6}}, {{1,6},{-1,6},{1,-6},{-1,-6}}, {{2,5},{-2,5},{2,-5},{-2,-5}}, {{1,5},{-1,5},{1,-5},{-1,-5}} }),
00092   assert(f({{1,2},{-1,3},{-2,4},{-2,5},{-3,6},{-3,7}}) = { {{3,4},{3,5},{-3,6},{-3,7}}, {{2,6},{2,7},{-2,4},{-2,5}}, {{1,4},{1,5},{-1,6},{-1,7}} }),
00093   assert(f({{1,2,8},{-1,3,9},{-2,4},{-2,5},{-3,6},{-3,7}}) = { {{3,4,8,9},{3,5,8,9},{-3,6},{-3,7}}, {{2,6,8,9},{2,7,8,9},{-2,4},{-2,5}}, {{1,4,8},{1,5,8},{-1,6,9},{-1,7,9}} }),
00094   true)$
00095 
00096 okltest_singulartuple_degrees_cs(f) := block([F],
00097   assert(f([],F) = []),
00098   assert(f([],{}) = []),
00099   assert(f([],{{}}) = []),
00100   assert(f([1],{}) = []),
00101   assert(f([1],{{}}) = []),
00102   assert(f([1],{{1}}) = []),
00103   assert(f([1],{{1},{-1}}) = [1]),
00104   assert(f([1],{{1},{-1,2},{-1,-2}}) = [2]),
00105   assert(f([1,2],{{1},{-1,2},{-1,-2}}) = [2,1]),
00106   assert(f([2,1],{{1},{-1,2},{-1,-2}}) = [1,1]),
00107   assert(f([2,1,3],{{1},{-1,2},{-1,-2}}) = [1,1]),
00108   assert(f([3,2,1],{{1},{-1,2},{-1,-2}}) = []),
00109   assert(f([1,2,3,4],{{1,2},{-1,3},{-1,4},{-2},{-3},{-4}}) = [2,2,1,1]),
00110   assert(f([2,1,3,4],{{1,2},{-1,3},{-1,4},{-2},{-3},{-4}}) = [1,2,1,1]),
00111   assert(f([2,3,4,1],{{1,2},{-1,3},{-1,4},{-2},{-3},{-4}}) = [1,1,1,1]),
00112   assert(f([1,2],{{1,2},{-1,3,4},{-1,-3,4},{-1,3,-4},{-1,-3,-4},{-2}}) = [4,4]),
00113   assert(f([2,1],{{1,2},{-1,3,4},{-1,-3,4},{-1,3,-4},{-1,-3,-4},{-2}}) = [1,4]),
00114   assert(f([1,2],{{1,2},{-1,2},{-2,3,4},{-2,-3,4},{-2,3,-4},{-2,-3,-4}}) = [1,4]),
00115   assert(f([2,1],{{1,2},{-1,2},{-2,3,4},{-2,-3,4},{-2,3,-4},{-2,-3,-4}}) = []),
00116   true)$
00117 
00118 okltest_singulartuple_csp(f) := block([F],
00119   assert(f([],F) = true),
00120   assert(f([],{}) = true),
00121   assert(f([],{{}}) = true),
00122   assert(f([1],{}) = false),
00123   assert(f([1],{{}}) = false),
00124   assert(f([1],{{1}}) = false),
00125   assert(f([1],{{1},{-1}}) = true),
00126   assert(f([1],{{1},{-1,2},{-1,-2}}) = true),
00127   assert(f([1,2],{{1},{-1,2},{-1,-2}}) = true),
00128   assert(f([2,1],{{1},{-1,2},{-1,-2}}) = true),
00129   assert(f([2,1,3],{{1},{-1,2},{-1,-2}}) = false),
00130   assert(f([3,2,1],{{1},{-1,2},{-1,-2}}) = false),
00131   F : {{1,2},{-1,3},{-1,4},{-2},{-3},{-4}},
00132   for v in permutations([1,2,3,4]) do
00133     assert(f(v,F) = true),
00134   true)$
00135 
00136 okltest_onesingulartuple_csp(f) := block([F],
00137   assert(f([],F) = true),
00138   assert(f([],{}) = true),
00139   assert(f([],{{}}) = true),
00140   assert(f([1],{{1}}) = true),
00141   assert(f([1],{{1},{-1}}) = true),
00142   assert(f([1],{{1},{-1,2},{-1,-2}}) = false),
00143   assert(f([2,1],{{1},{-1,2},{-1,-2}}) = true),
00144   true)$
00145 
00146 okltest_nononesingulartuple_csp(f) := (
00147   assert(f([],F) = true),
00148   assert(f([],{}) = true),
00149   assert(f([],{{}}) = true),
00150   assert(f([1],{{1}}) = true),
00151   assert(f([1],{{1},{-1}}) = false),
00152   assert(f([1],{{1},{-1,2},{-1,-2}}) = true),
00153   assert(f([2,1],{{1},{-1,2},{-1,-2}}) = false),
00154   assert(f([1,2],{{1},{-1,2},{-1,-2}}) = false),
00155   assert(f([1,2],{{1},{-1,2},{-1,-2},{2,3}}) = true),
00156   assert(f([1,2,3],{{1},{-1,2},{-1,-2},{2,3}}) = true),
00157   true)$
00158 
00159 okltest_totally_singulartuple_csp_bydef(f) := (
00160   assert(f([],F) = true),
00161   assert(f([],{}) = true),
00162   assert(f([],{{}}) = true),
00163   assert(f([1],{{1}}) = false),
00164   assert(f([1],{{1},{-1}}) = true),
00165   assert(f([1],{{1},{-1,2},{-1,-2}}) = true),
00166   assert(f([2,1],{{1},{-1,2},{-1,-2}}) = true),
00167   assert(f([1,2],{{1},{-1,2},{-1,-2}}) = true),
00168   assert(f([1,2],{{1},{-1,2},{-1,-2},{2,3}}) = true),
00169   assert(f([1,2,3],{{1},{-1,2},{-1,-2},{2,3}}) = false),
00170   assert(f([1,2],{{2,1},{2,-1},{-2,3},{-2,-3}}) = false),
00171   true)$
00172 
00173 okltest_sdpss_cs_bydef(f) := (
00174   assert(f({}) = {{}}),
00175   assert(f({{}}) = {{}}),
00176   assert(f({{1}}) = {{}}),
00177   assert(f({{1},{-1}}) = {{},{1}}),
00178   assert(f({{1},{-1,2},{-1,-2}}) = {{},{1},{2},{1,2}}),
00179   assert(f({{1,2,8},{-1,3,9},{-2,4},{-2,5},{-3,6},{-3,7}}) = {{},{1},{2},{3},{1,2},{1,3},{2,3}}),
00180   assert(f({{1,2},{-1,3},{-2,4},{-2,-4},{-3,4},{-3,-4}}) = {{},{1},{2},{3},{1,2},{1,3},{2,3}}),
00181   assert(f({{1,2},{-1,2},{-2,3,4},{-2,-3,4},{-2,3,-4},{-2,-3,-4}}) = {{},{1},{1,2}}),
00182   assert(okltest_sdp_count_cs_bydef(buildq([f], lambda([F], length(max_elements(f(F)))))) = true),
00183   true)$
00184 
00185 okltest_onesdpss_cs_bydef(f) := (
00186   assert(f({}) = {{}}),
00187   assert(f({{}}) = {{}}),
00188   assert(f({{1}}) = {{}}),
00189   assert(f({{1},{-1}}) = {{},{1}}),
00190   assert(f({{1},{-1,2},{-1,-2}}) = {{},{2},{1,2}}),
00191   assert(f({{1,2,8},{-1,3,9},{-2,4},{-2,5},{-3,6},{-3,7}}) = {{},{1}}),
00192   assert(f({{1,2},{-1,3},{-2,4},{-2,-4},{-3,4},{-3,-4}}) = {{},{1}}),
00193   assert(f({{1,4},{-1,4},{2,3,-4},{-2,3,-4},{-3,-4}}) = {{},{1},{1,2},{1,2,3},{2},{2,3},{1,2,3,4}}),
00194   true)$
00195 
00196 okltest_maxnononesdpst_cs_bydef(f) := (
00197   assert(f({}) = {[]}),
00198   assert(f({{}}) = {[]}),
00199   assert(f({{1}}) = {[]}),
00200   assert(f({{1},{-1}}) = {[]}),
00201   assert(f({{1},{-1,2},{-1,-2}}) = {[1]}),
00202   assert(f({{1},{-1,2},{-1,-2},{2,3}}) = {[1,2],[2,1]}),
00203   assert(f({{1},{-1,2},{-1,-2},{2,3},{-3,4},{-3,-4}}) = permutations([1,2,3])),
00204   assert(f({{1,2},{-1,3},{-1,4},{-2,5},{-2,6}}) = {[1],[2]}),
00205   assert(f({{1,2,8},{-1,3,9},{-2,4},{-2,5},{-3,6},{-3,7}}) = {[2,1],[3,1],[2,3],[3,2]}),
00206   true)$
00207 
00208 okltest_sdp_count_cs_bydef(f) := block(
00209   assert(f({}) = 1),
00210   assert(f({{}}) = 1),
00211   assert(f({{1,2,8},{-1,3,9},{-2,4},{-2,5},{-3,6},{-3,7}}) = 3),
00212   assert(f({{2,3,8,9},{-2,4},{-2,5},{-3,6},{-3,7}}) = 2),
00213   assert(f({{1,2},{-1,3},{-2,4},{-2,-4},{-3,4},{-3,-4}}) = 3),
00214   assert(f({{2,3},{-2,4},{-2,-4},{-3,4},{-3,-4}}) = 2),
00215   if oklib_test_level=0 then return(true),
00216   assert(f({{2,5,3,6},{-2,4},{-2,-4},{-3,4},{-3,-4},{-5,7,8},{-5,-7,8},{-5,7,-8},{-5,-7,-8},{-6,9,10},{-6,-9,10},{-6,9,-10},{-6,-9,-10}}) = 4),
00217   assert(okltest_cfsdp_csp_bydef(buildq([f], lambda([F], is(f(F)=1)))) = true),
00218   true)$
00219 
00220 okltest_cfsdp_csp_bydef(f) := (
00221   assert(f({}) = true),
00222   assert(f({{}}) = true),
00223   for k : 0 thru if oklib_test_level=0 then 2 else 3 do
00224    block([F : marginal_musat1(k)],
00225     assert(f(F) = true)),
00226   assert(f({{1,2},{-1,3},{-1,-3},{-2,3},{-2,-3}}) = false),
00227   true)$
00228 
00229 okltest_cfisdp_count_cs_bydef(f) := block(
00230   assert(f({}) = 1),
00231   assert(f({{}}) = 1),
00232   assert(f({{1,2,8},{-1,3,9},{-2,4},{-2,5},{-3,6},{-3,7}}) = 2),
00233   assert(f({{2,3,8,9},{-2,4},{-2,5},{-3,6},{-3,7}}) = 1),
00234   assert(f({{1,2},{-1,3},{-2,4},{-2,-4},{-3,4},{-3,-4}}) = 1),
00235   if oklib_test_level=0 then return(true),
00236   assert(f({{1,2,5},{-1,3,6},{-2,4},{-2,-4},{-3,4},{-3,-4}}) = 2),
00237   assert(f({{2,5,3,6},{-2,4},{-2,-4},{-3,4},{-3,-4}}) = 1),
00238   assert(f({{1,2,5},{-1,3,6},{-2,4},{-2,-4},{-3,4},{-3,-4},{-5,7,8},{-5,-7,8},{-5,7,-8},{-5,-7,-8},{-6,9,10},{-6,-9,10},{-6,9,-10},{-6,-9,-10}}) = 5),
00239   assert(f({{2,5,3,6},{-2,4},{-2,-4},{-3,4},{-3,-4},{-5,7,8},{-5,-7,8},{-5,7,-8},{-5,-7,-8},{-6,9,10},{-6,-9,10},{-6,9,-10},{-6,-9,-10}}) = 2),
00240   assert(f({{1,2,5},{-1,3,6},{-2,4,5},{-2,-4,6},{-3,4},{-3,-4},{-5,7,8},{-5,-7,8},{-5,7,-8},{-5,-7,-8},{-6,9,10},{-6,-9,10},{-6,9,-10},{-6,-9,-10}}) = 3),
00241   assert(f({{2,5,3,6},{-2,4,5},{-2,-4,6},{-3,4},{-3,-4},{-5,7,8},{-5,-7,8},{-5,7,-8},{-5,-7,-8},{-6,9,10},{-6,-9,10},{-6,9,-10},{-6,-9,-10}}) = 2),
00242   assert(f({{-10,-9,-6},{-10,-6,9},{-9,-6,10},{-8,-7,-5},{-8,-5,7},{-7,-5,8},{-6,9,10},{-5,7,8},{-4,-3},{-4,-2,6},{-3,4},{-2,4,5},{2,3,5,6}}) = 2),
00243   assert(f({{1,2},{-1,3,5},{-1,4,6},{-2,3,5},{-2,4,6},{-3,5},{-4,6},{-5,-6}}) = 1),
00244   true)$
00245 
00246 okltest_cfisdp_csp_bydef(f) := (
00247   assert(f({}) = true),
00248   assert(f({{}}) = true),
00249   assert(f({{1,2},{-1,3},{-1,-3},{-2,3},{-2,-3}}) = true),
00250   assert(f({{1,2,8},{-1,3,9},{-2,4},{-2,5},{-3,6},{-3,7}}) = false),
00251   true)$
00252 
00253 okltest_nonsingular_csp(f) := (
00254   assert(f({}) = true),
00255   assert(f({{}}) = true),
00256   assert(f({{1}}) = true),
00257   assert(f({{-1}}) = true),
00258   assert(f({{1},{-1}}) = false),
00259   assert(f({{1,2}}) = true),
00260   assert(f({{1,2},{-1,2}}) = false),
00261   assert(f({{1,2},{-1,2},{-2,1}}) = false),
00262   assert(f({{1,2},{-1,2},{-2,1},{-1,-2}}) = true),
00263   assert(f({{-3,-2,-1},{-3,1},{-2,3},{-1,2},{1,2,3}}) = true),
00264   assert(f(weak_php_cs(3,2)) = false),
00265   true)$
00266 
00267 okltest_nononesingular_csp(f) := (
00268   assert(f({}) = true),
00269   assert(f({{}}) = true),
00270   assert(f({{1}}) = true),
00271   assert(f({{-1}}) = true),
00272   assert(f({{1},{-1}}) = false),
00273   assert(f({{1,2}}) = true),
00274   assert(f({{1,2},{-1,2}}) = false),
00275   assert(f({{1,2},{-1,2},{-2,1}}) = true),
00276   assert(f({{1,2},{-1,2},{-2,1},{-1,-2}}) = true),
00277   assert(f({{-3,-2,-1},{-3,1},{-2,3},{-1,2},{1,2,3}}) = true),
00278   assert(f(weak_php_cs(3,2)) = true),
00279   true)$
00280 
00281