OKlibrary  0.2.1.6
RBases.mac
Go to the documentation of this file.
00001 /* Oliver Kullmann, 27.12.2009 (Swansea) */
00002 /* Copyright 2009, 2010, 2011 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/DataStructures/Lisp/Lists.mac")$
00023 oklib_include("OKlib/ComputerAlgebra/Satisfiability/Lisp/ClauseSets/PartialAssignments.mac")$
00024 oklib_include("OKlib/ComputerAlgebra/Satisfiability/Lisp/ClauseSets/BasicOperations.mac")$
00025 
00026 
00027 /* *****************
00028    * Basic notions *
00029    *****************
00030 */
00031 
00032 /*
00033  Consider a function r: CLS -> CLS; the meaning is that r is a "reduction",
00034  which means that r(F) is sat-equivalent to F, but for the general definitions
00035  actually no requirements are needed for r.
00036  Consider a clause-set F (regarding as CNF).
00037  An "r-generating subset of F" is a subset F' <= F such that for all
00038  clauses C in F we have {} in r(vp_C * F').
00039  An "r-base of F" is a minimal r-generating subset of F.
00040 */
00041 
00042 /* Predicate for deciding whether G is r-generating for F:
00043 */
00044 
00045 /* First without subsumption-check (without stipulating any relation between
00046    G and F), assuming only that if {} in F, then {} in red_(F)): */
00047 rgen0_p_cs(G,F,red_) :=
00048   every_s(lambda([C], elementp({}, red_(apply_pa_cs(comp_sl(C), G)))),
00049           setdifference(F,G))$
00050 /* For arbitrary clause-lists G, F (without stipulating any relation between
00051    G and F), without any assumption of red_ (but red_ now operates on
00052    clause-lists):
00053 */
00054 rgen0_p_cl(G,F,red_) :=
00055   every_s(lambda([C], elementp({}, cl2cs(red_(apply_pa_cl(comp_sl(C), G))))),
00056           F)$
00057 
00058 /* Now the complete test: */
00059 rgen_p_cs(G,F,red_) := subsetp(G,F) and rgen0_p_cs(G,F,red_)$
00060 
00061 
00062 /* Now the predicate whether G is an r-base for F: */
00063 rbase_p_cs(G,F,red_) := rgen_p_cs(G,F,red_) and
00064   every_s(lambda([C], not rgen0_p_cs(disjoin(C,G),F,red_)), G)$
00065 
00066 /* Computes the set of all r-bases of clause-set F "by definition": */
00067 all_rbases_bydef(F,red_) :=
00068   subset(powerset(F), lambda([G], rbase_p_cs(G,F,red_)))$
00069 
00070 
00071 /* ********************
00072    * Basic algorithms *
00073    ********************
00074 */
00075 
00076 /* Computing the red_-base of clause-list F according to the definition,
00077    that is, a minimal sublist S of F such that for all clauses D in F - S
00078    we have {} in red_(phi_D * F), by trying to remove the clauses from
00079    F in the given order.
00080    The only assumption on red_ (besides {} in F => {} in red_(F)) is that
00081    if {} in red_(F) then also {} in red_(F') for any super-set F'
00082    of F (so that once a clause is classified as unremovable, then this
00083    doesn't change after further removals).
00084 */
00085 rbase_cl(F,red_) := block([Fb : F],
00086   for C in F do block([Fb_new : delete(C,Fb)],
00087     if rgen0_p_cl(Fb_new,F,red_) then Fb : Fb_new),
00088  return(Fb))$
00089 
00090 
00091 /* ************
00092    * Sampling *
00093    ************
00094 */
00095 
00096 /* Computing some red_-base of clause-set F according to the definition,
00097    that is, a minimal subset S of F such that for all clauses D in F - S
00098    we have {} in red_(phi_D * F).
00099    The only assumption on red_ (besides {} in F => {} in red_(F)) is that
00100    if {} in red_(F) then also {} in red_(F') for any super-set F'
00101    of F (so that once a clause is classified as unremovable, then this
00102    doesn't change after further removals).
00103    Any possible red_-base will be chosen if its clauses come first in the
00104    order; so given that random_permutation is really random, all possible
00105    bases have non-zero probability of being chosen.
00106 */
00107 
00108 rand_rbase_cs(F,red_) := block([F0 : F], 
00109   for C in random_permutation(F0) do
00110     if rgen0_p_cs(disjoin(C,F),F0,red_) then F : disjoin(C,F),
00111  return(F))$
00112 
00113 /* Remarks:
00114    If red_(F) = F then rand_rbase_cs(F,red_) is subsumption elimination for F.
00115    If red_(F) = generalised_ucp_cs(F,inf) then rand_rbase_cs(F,red_) returns
00116    a choice of an irredundant core of F.
00117 */
00118