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)])),
00074     return(not found)))$
00075 
00076 /* An example for a claw-free matching lean clause-set of deficiency 1.
00077    From [Kullmann, SAT 2003], Section 5. */
00078 clawfree_mlean_def1 : 
00079 [setn(8), {
00080   {1,3,8},{1,-3,4},{-1,-2,6,7},{-1,-2,-5,-6},{2,-3,-4,-5},{-4,5,-7,-8},
00081   {-1,5,-6,8},{-1,4,6,-7},{2,3,7,-8}
00082  }]$
00083