OKlibrary  0.2.1.6
MatchingAutarkies.mac
Go to the documentation of this file.
```00001 /* Oliver Kullmann, 1.6.2008 (Swansea) */
00002 /* Copyright 2008, 2009, 2010 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/Hypergraphs/Lisp/SetSystems.mac")\$
00023 oklib_include("OKlib/ComputerAlgebra/Satisfiability/Lisp/ClauseSets/Hypergraphs.mac")\$
00024 oklib_include("OKlib/ComputerAlgebra/DataStructures/Lisp/Lists.mac")\$
00025 oklib_include("OKlib/ComputerAlgebra/Satisfiability/Lisp/ClauseSets/PartialAssignments.mac")\$
00026
00027
00028 /* ********************
00029    * Basic operations *
00030    ********************
00031 */
00032
00033 /* The ordered directed clause-literal graph of an ordered
00034    clause-set, restricted to the edges to satisfying
00035    literal-occurrences for a given partial assignment:
00036 */
00037 cllit_aut_odg(F,phi) :=
00038   [append(
00039      map(lambda([C],[C,1]),F),
00040      map(lambda([x],[x,2]),
00041        listify(intersection(literals_v(var_ocs(F)),phi)))),
00042    lappend(
00043      map(
00044        lambda([C],
00045          map(lambda([x],[[C,1],[x,2]]),
00046              listify(intersection(phi,C)))),
00047        F))]\$
00048
00049 /* Test for a matching autarky for an ordered clause-set: */
00050 maut_paocs_p(phi,F) := block([F0 : socs_V(F,var_pa(phi))],
00051   is(length(max_matching(og2mg_nl(odg2og(cllit_aut_odg(F0,phi))))) = length(F0)))\$
00052
00053 /* The set of all matching autarkies for an ordered clause-set: */
00054 all_maut_ocs(F) := subset(all_pass(var_ocs(F)),
00055   lambda([phi],maut_paocs_p(phi,F)))\$
00056 /* The matching autarky monoid of an ordered clause-set: */
00057 mautmon_ocs(F) := [all_maut_ocs(F), compo_pass, {}]\$
00058
00059
00060 /* *****************************
00061    * Matching-lean clause-sets *
00062    *****************************
00063 */
00064
00065 /* Testing matching-leanness of clause-sets by the strict maximality of the
00066    maximum deficiency: */
00067 matchinglean_smax_p(F) := if emptyp(F) then true else block(
00068  [V : var_cs(F), def],
00069   def : deficiency_fcs([V,F]),
00070   if def <= 0 then return(false),
00071   block([found : false],
00072     for C in F unless found do
00073       found : is(def <= max_deficiency_fcs([V,disjoin(C,F)])),