OKlibrary  0.2.1.6
MatchingAutarkies.mac
Go to the documentation of this file.
00001 /* Oliver Kullmann, 1.6.2008 (Swansea) */
00002 /* Copyright 2008 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/Hypergraphs/Lisp/SetSystems.mac")$
00024 oklib_include("OKlib/ComputerAlgebra/Satisfiability/Lisp/ClauseSets/Hypergraphs.mac")$
00025 oklib_include("OKlib/ComputerAlgebra/Satisfiability/Lisp/ClauseSets/Statistics.mac")$
00026 oklib_include("OKlib/ComputerAlgebra/Satisfiability/Lisp/ConflictCombinatorics/HittingClauseSets.mac")$
00027 oklib_include("OKlib/ComputerAlgebra/Satisfiability/Lisp/Autarkies/MatchingAutarkies.mac")$
00028 oklib_include("OKlib/ComputerAlgebra/Algebra/Lisp/Groupoids/BasicNotions.mac")$
00029 
00030 kill(f)$
00031 
00032 /* ********************
00033    * Basic operations *
00034    ********************
00035 */
00036 
00037 okltest_cllit_aut_odg(f) := (
00038   assert(f([],{}) = [[],[]]),
00039   assert(f([],{1}) = [[],[]]),
00040   assert(f([{}],{}) = [[[{},1]],[]]),
00041   assert(f([{}],{1}) = [[[{},1]],[]]),
00042   assert(f([{1}],{1}) = [[[{1},1],[1,2]], [[[{1},1],[1,2]]]]),
00043   assert(f([{1}],{-1}) = [[[{1},1],[-1,2]], []]),
00044   assert(f([{1},{-1,2}],{-1}) = [[[{1},1],[{-1,2},1],[-1,2]], [[[{-1,2},1],[-1,2]]]]),
00045   true)$
00046 
00047 okltest_maut_paocs_p(f) := (
00048   assert(f({},[]) = true),
00049   assert(f({},[{}]) = true),
00050   assert(f({1,-2},[]) = true),
00051   assert(f({1,-2},[{}]) = true),
00052   assert(f({1},[{1}]) = true),
00053   assert(f({1},[{-1}]) = false),
00054   assert(f({1},[{1},{1,2}]) = false),
00055   assert(f({1,2},[{1},{1,2}]) = true),
00056   assert(f({1,2},[{1,-3},{1,2,3,-4},{},{3,4}]) = true),
00057   assert(f({1,2,3},[{1,-3},{1,2,3,-4},{},{3,4}]) = true),
00058   assert(f({1,-2,3},[{1,2,-3},{-1,-2,-3},{3}]) = true),
00059   true)$
00060 
00061 okltest_all_maut_ocs(f) := block(
00062   assert(f([]) = {{}}),
00063   assert(f([{}]) = {{}}),
00064   assert(f([{1}]) = {{},{1}}),
00065   assert(f([{1},{-1}]) = {{}}),
00066   assert(f([{1},{2}]) = {{},{1},{2},{1,2}}),
00067   assert(f([{1},{1,-2}]) = {{},{1,-2},{-2}}),
00068   assert(f([{1,2},{2,3},{3,4}]) = {{},{1},{1,2},{1,2,3},{1,2,3,4},{1,2,3,-4},{1,2,4},{1,2,4,-3},{3,4},{2,3,4},{-1,2,3,4},{1,3,4},{1,-2,3,4},{4},{4,1}}),
00069   if oklib_test_level = 0 then return(true),
00070   block([oklib_test_level : oklib_test_level-1],
00071     assert(okltest_matchinglean_p(buildq([f],lambda([F],is(f(cs2ocs(F))={{}})))))),
00072   true)$
00073 
00074 okltest_mautmon_ocs(f) := block(
00075   exm : [
00076    [], [{}],
00077    [{1},{2}]
00078   ],
00079   for F in exm do
00080     assert(mon_p(f(F))),
00081   if oklib_test_level = 0 then return(true),
00082   exm1 : [
00083    [{1,2},{2,3},{3,4}]
00084   ],
00085   for F in exm1 do
00086     assert(mon_p(f(F))),
00087   true)$
00088 
00089 
00090 /* *****************************
00091    * Matching-lean clause-sets *
00092    *****************************
00093 */
00094 
00095 /* Testing whether f decides correctly matching leanness: */
00096 okltest_matchinglean_p(f) := block(
00097   assert(f({}) = true),
00098   assert(f({{}}) = true),
00099   assert(f({{1}}) = false),
00100   assert(f({{1},{-1}}) = true),
00101   assert(f({{1},{1,2}}) = false),
00102   assert(f({{1},{1,2},{2,-1}}) = true),
00103   assert(f({{1,2},{-1,2},{1,-2}}) = true),
00104   true)$
00105 
00106 okltest_clawfree_mlean_def1(FF) := block(
00107   assert(FF[1] = setn(8)),
00108   assert(deficiency_fcs(FF) = 1),
00109   assert(literal_degrees_list_fcs(FF) = [[2,15],[4,1]]),
00110   assert(variable_degrees_list_cs(FF[2]) = [[4,7],[6,1]]),
00111   assert(hitting1rcsp(FF[2]) = true),
00112   assert(sat_decision_hitting_cs(FF[2]) = true), 
00113     /* The satisfiability of FF is actually implied, since every unsatisfiable
00114     hitting clause-set with deficiency 1 must contain a variables with
00115     (1,1)-occurrence. */
00116   assert(matchinglean_smax_p(FF[2]) = true),
00117   true)$
00118