OKlibrary  0.2.1.6
Cores.mac
Go to the documentation of this file.
00001 /* Oliver Kullmann, 8.4.2008 (Swansea) */
00002 /* Copyright 2008, 2009, 2012 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/Backtracking/DLL_solvers.mac")$
00024 oklib_include("OKlib/ComputerAlgebra/Satisfiability/Lisp/Generators/Generators.mac")$
00025 oklib_include("OKlib/ComputerAlgebra/Hypergraphs/Lisp/Basics.mac")$
00026 oklib_include("OKlib/ComputerAlgebra/Hypergraphs/Lisp/Transversals/Minimal/RecursiveSplitting.mac")$
00027 oklib_include("OKlib/ComputerAlgebra/Satisfiability/Lisp/ClauseSets/BasicOperations.mac")$
00028 
00029 
00030 kill(f)$
00031 
00032 
00033 /* *************************************************
00034    * Minimally unsatisfiable cores of minimum size *
00035    *************************************************
00036 */
00037 
00038 okltest_min_size_mus(f) := block([S : dll_simplest_trivial1],
00039   assert(f({{}},S) = 1),
00040   assert(f({{1},{-1}},S) = 2),
00041   assert(f({{1},{-1},{2},{-2}},S) = 2),
00042   assert(f({{1},{-1},{}},S) = 1),
00043   assert(f({{1,2},{-2,3},{-1,3},{1,-2},{2,3}},S) = inf),
00044   assert(f({{1,2},{-2,-3},{-1,3},{1,-2},{2,-3}},S) = 5),
00045   assert(f({{1,2},{-2,-3},{-1,3},{1,-2},{2,-3},{2,3}},S) = 5),
00046   true)$
00047 
00048 okltest_contains_us(f) := block([S : dll_simplest_trivial1],
00049   assert(f({},0,S) = false),
00050   assert(f({},1,S) = false),
00051   assert(f({},inf,S) = false),
00052   assert(f({{}},0,S) = false),
00053   assert(f({{}},1,S) = true),
00054   assert(f({{}},2,S) = true),
00055   assert(f({{-1},{1}},0,S) = false),
00056   assert(f({{-1},{1}},1,S) = false),
00057   assert(f({{-1},{1}},2,S) = true),
00058   assert(f({{-1},{1}},inf,S) = true),
00059   true)$
00060 
00061 
00062 /* ***********************************
00063    * Computing all irredundant cores *
00064    ***********************************
00065 */
00066 
00067 okltest_all_irr_cores(f) := block([S : dll_simplest_trivial1],
00068   assert(f([{},{}],S) = {{}}),
00069   assert(f([{},{{}}],S) = {{{}}}),
00070   assert(f([{1},{{1}}],S) = {{{1}}}),
00071   assert(f([{1},{{1},{}}],S) = {{{}}}),
00072   assert(f([{1},{{1},{-1}}],S) = {{{1},{-1}}}),
00073   assert(f([{1},{{1},{-1},{}}],S) = {{{1},{-1}},{{}}}),
00074   assert(f([{1,2},{{1,2},{-1,2}}],S) = {{{1,2},{-1,2}}}),
00075   assert(f([{1,2,3},{{1,2},{1,-2},{1},{3}}],S) = {{{1},{3}}, {{1,2},{1,-2},{3}}}),
00076   assert(f([{1,2},{{-1},{1},{2},{-2}}],S) = {{{-1},{1}},{{-2},{2}}}),
00077   assert(f([{1,2,3,4},{{1,2},{-1,2},{-2},{3},{4},{-3,-4}}],S) = {{{1,2},{-1,2},{-2}}, {{3},{4},{-3,-4}}}),
00078   if oklib_test_level = 0 then return(true),
00079   block([oklib_test_level : oklib_test_level - 1],
00080     okltest_all_min_usat_cores_bydef(buildq([f],lambda([F,S],f(F,S))))),
00081   true)$
00082 
00083 okltest_all_min_usat_cores(f) := block([S : dll_simplest_trivial1],
00084   assert(f([{},{{}}],S) = {{{}}}),
00085   assert(f([{1},{{}}],S) = {{{}}}),
00086   assert(f([{1},{{1},{-1}}],S) = {{{1},{-1}}}),
00087   assert(f([{1,2},{{1},{-1},{1,2}}],S) = {{{1},{-1}}}),
00088   assert(f([{1},{{1},{-1},{}}],S) = {{{1},{-1}},{{}}}),
00089   assert(f([{1,2},{{1},{-1},{2},{-2}}],S) = {{{1},{-1}},{{2},{-2}}}),
00090   assert(f([{1,2},{{1},{-1},{2},{-2},{1,2}}],S) = {{{1},{-1}},{{2},{-2}},{{1,2},{-1},{-2}}}),
00091   true);
00092 
00093 okltest_all_forced_irr_cores(f) := block(
00094  [S : dll_simplest_trivial1,
00095   nf : buildq([f,S],lambda([F,P], block (
00096    [counter_irr : 0, potentially_unusable_clauses : not emptyp(F)],
00097     f(F,P,S))))],
00098   assert(nf({},{}) = {{}}),
00099   assert(nf({},{{}}) = {{{}}}),
00100   assert(nf({},{{1}}) = {{{1}}}),
00101   assert(nf({{1}},{}) = {{{1}}}),
00102   assert(nf({{1}},{{1,2}}) = {{{1}}}),
00103   assert(nf({{1,2}},{{-1,2}}) = {{{1,2},{-1,2}}}),
00104   assert(nf({{1}},{{2},{-2}}) = {}),
00105   assert(nf({{1}},{{-1},{2},{-2}}) = {{{1},{-1}}}),
00106   true)$
00107 
00108 /* *************************************************
00109    * Heuristical search for some irredundant cores *
00110    *************************************************
00111 */
00112 
00113 /* Generic test function for testing whether f on input an unsatisfiable
00114    clause-set F returns some minimally unsatisfiable core of F:
00115 */
00116 okltest_some_mus_cs(f) := (
00117   /* Cases where F has exactly one minimally unsatisfiable subset */
00118   assert(f({{}}) = {{}}),
00119   assert(f({{1},{-1}}) = {{1},{-1}}),
00120   assert(f({{1},{-1},{2}}) = {{1},{-1}}),
00121   assert(f({{1,2},{-1,2},{-2,3},{-2,-3},{1,3}}) = {{1,2},{-1,2},{-2,3},{-2,-3}}),
00122   /* XXX */
00123   true)$
00124 
00125 
00126 okltest_first_mus_fcs(f) := block([S : dll_simplest_trivial1],
00127   assert(f([{},{{}}],S) = [{},{{}}]),
00128   assert(f([{1},{{},{1}}],S) = [{1},{{}}]),
00129   assert(f([{1},{{1},{-1}}],S) = [{1},{{1},{-1}}]),
00130   assert(f([{1,2},{{1},{-1},{1,2}}],S) = [{1,2},{{1},{-1}}]),
00131   for n : 0 thru 3 do block([FF : full_fcs(n)],
00132     assert(f(FF,S) = FF)),
00133   assert(okltest_some_mus_cs(buildq([f,S], lambda([F], fcs2cs(f(cs2fcs(F),S))))) = true),
00134   true)$
00135 
00136 /* Generic test function for testing whether f on input a clause-set F
00137    returns some irredundant core of F:
00138 */
00139 okltest_some_irr_cs(f) := (
00140   /* Cases where F has exactly one irredundant core */
00141   assert(f({}) = {}),
00142   assert(f({{1}}) = {{1}}),
00143   assert(f({{-1}}) = {{-1}}),
00144   assert(f({{1},{1,2}}) = {{1}}),
00145   assert(f({{1,2},{-1,2},{1,-2}}) = {{1,2},{-1,2},{1,-2}}),
00146   assert(f({{1,2},{-2,3},{1,3}}) = {{1,2},{-2,3}}),
00147   /* XXX */
00148   assert(okltest_some_mus_cs(f) = true),
00149   true)$
00150 
00151 okltest_first_irr_fcs(f) := block([S : dll_simplest_trivial1],
00152   assert(f([{},{}],S) = [{},{}]),
00153   assert(f([{1},{{1}}],S) = [{1},{{1}}]),
00154   assert(f([{1,2},{{1,2},{-1,2}}],S) = [{1,2},{{1,2},{-1,2}}]),
00155   assert(f([{1,2},{{1},{1,2}}],S) = [{1,2},{{1}}]),
00156   assert(okltest_some_irr_cs(buildq([f,S], lambda([F], fcs2cs(f(cs2fcs(F),S))))) = true),
00157   if oklib_test_level = 0 then return(true),
00158   block([oklib_test_level : oklib_test_level-1],
00159     okltest_first_mus_fcs(f)),
00160   true)$
00161 
00162 
00163 /* *********************************
00164    * Sampling of irredundant cores *
00165    *********************************
00166 */
00167 
00168 okltest_sample_irr_cores(f) := block([Sol,x],
00169   assert(f([{},{}],Sol,0,x,0) = {}),
00170   assert(f([{},{{}}],Sol,0,x,0) = {}),
00171   Sol : dll_simplest_trivial1,
00172   assert(f([{},{{}}],Sol,1,0,0) = {{{}}}),
00173   for n : 0 thru 2 do block([FF : full_fcs(n)],
00174     assert(f(FF,Sol,inf,0,0) = {FF[2]}),
00175     assert(f(FF,Sol,inf,0,1) = {FF[2]}),
00176     assert(f(FF,Sol,inf,1,0) = {FF[2]}),
00177     assert(f(FF,Sol,inf,1,1) = {FF[2]}),
00178     assert(f(FF,Sol,1,1,2) = {FF[2]})),
00179   block(
00180    [FF : [{1,2},{{1},{-1},{2},{-2}}],
00181     MUS : {{{1},{-1}},{{2},{-2}}}],
00182     assert(f(FF,Sol,0,0,0) = {}),
00183     assert(length(intersection(f(FF,Sol,1,0,0), MUS)) = 1),
00184     assert(length(intersection(f(FF,Sol,1,1,1), MUS)) = 1),
00185     assert(union(f(FF,Sol,1,0,0),f(FF,Sol,1,1,1)) = MUS),
00186     assert(f(FF,Sol,2,0,0) = MUS),
00187     assert(f(FF,Sol,2,0,1) = MUS),
00188     assert(f(FF,Sol,2,1,0) = MUS),
00189     assert(f(FF,Sol,2,1,1) = MUS)
00190   ),
00191   if oklib_test_level = 0 then return(true),
00192   block(
00193    [FF : [{1,2,3}, {{1},{-1},{2},{-2},{3},{-3},{1,2},{1,3},{2,3}}],
00194     MUS : { {{1},{-1}}, {{2},{-2}}, {{3},{-3}}, {{1,2},{-1},{-2}}, 
00195             {{1,3},{-1},{-3}}, {{2,3},{-2},{-3}} }, MUS2],
00196     assert(f(FF,Sol,6,0,0) = MUS),
00197     assert(f(FF,Sol,inf,0,0) = MUS),
00198     MUS2 : f(FF,Sol,5,0.5,0),
00199     assert(subsetp(MUS2,MUS) = true),
00200     assert(length(intersection(MUS2,MUS)) = 5)
00201   ),
00202   block([oklib_test_level : oklib_test_level - 1],
00203     okltest_all_irr_cores_bydef(buildq([f],lambda([FF,S],f(FF,S,inf,1,0)))),
00204     okltest_all_irr_cores_bydef(buildq([f],lambda([FF,S],f(FF,S,inf,0.5,0)))),
00205     okltest_all_irr_cores_bydef(buildq([f],lambda([FF,S],f(FF,S,inf,0,0))))
00206   ),
00207   true)$
00208 
00209 
00210 /* ********************************************
00211    * Maximally non-equivalent sub-clause-sets *
00212    ********************************************
00213 */
00214 
00215 okltest_all_max_noneq_scs(f) := (
00216   block([EQp : lambda([F],is(F={}))],
00217     assert(f({},EQp) = {})
00218   ),
00219   block([EQp : lambda([F], not dll_simplest_trivial1(cs_to_fcs(F)))],
00220     assert(f({},EQp) = {{}}),
00221     assert(f({{}},EQp) = {{}})
00222   ),
00223   true)$
00224 
00225 okltest_all_max_sat_scs(f) := block([S : dll_simplest_trivial1],
00226   assert(f({{}},S) = {{}}),
00227   assert(f({{1},{-1}},S) = {{{1}},{{-1}}}),
00228   assert(f({{1},{-1},{}},S) = {{{1}},{{-1}}}),
00229   assert(f({{1},{-1},{1,2}},S) = {{{1},{1,2}},{{-1},{1,2}}}),
00230   assert(f({{1},{-1},{2},{-2}},S) = {{{1},{2}},{{1},{-2}},{{-1},{2}},{{-1},{-2}}}),
00231   if oklib_test_level = 0 then return(true),
00232   block(
00233    [oklib_test_level : oklib_test_level - 1,
00234     muf : buildq([f],lambda([FF,S],transversal_hyp_rs(ecomp_hyp([FF[2],f(FF[2],S)]))[2]))],
00235     okltest_all_min_usat_cores(muf)),
00236   true)$
00237 
00238 okltest_equivalence_checker_scl(f) := block([S : dll_simplest_trivial1],
00239   assert(f({},S)({}) = true),
00240   block([EQp : f({{}},S)],
00241     assert(EQp({}) = false),
00242     assert(EQp({{}}) = true)
00243   ),
00244   true)$
00245 
00246 okltest_all_max_neq_scs(f) := block([S : dll_simplest_trivial1],
00247   assert(f({},S) = {}),
00248   assert(f({{}},S) = {{}}),
00249   if oklib_test_level = 0 then return(true),
00250   block(
00251    [oklib_test_level : oklib_test_level - 1],
00252      okltest_all_max_sat_scs(f)),
00253   if oklib_test_level = 1 then return(true),
00254   block(
00255    [oklib_test_level : oklib_test_level - 1,
00256     irf : buildq([f],lambda([FF,S],transversal_hyp_rs(ecomp_hyp([FF[2],f(FF[2],S)]))[2]))],
00257     okltest_all_irr_cores(irf)),
00258   true)$
00259 
00260 
00261 /* ************************************
00262    * Duality between MAXSAT and MUSAT *
00263    ************************************
00264 */
00265 
00266 okltest_all_max_neq_scs_bydual(f) := block([H : transversal_hyp_rs],
00267   okltest_all_max_neq_scs(buildq([f,H],
00268     lambda([F,S],f(F,lambda([GG],all_irr_cores_bydef(GG,S)),H)))),
00269   true)$
00270 
00271 okltest_all_irr_cores_bydual(f) := block([H : transversal_hyp_rs],
00272   okltest_all_irr_cores(buildq([f,H],
00273     lambda([F,S],f(F,lambda([G],all_max_neq_scs_bydef(G,S)),H)))),
00274   true)$
00275