OKlibrary  0.2.1.6
InverseSingularDP.mac
Go to the documentation of this file.
00001 /* Oliver Kullmann, 14.6.2008 (Swansea) */
00002 /* Copyright 2008, 2009, 2013 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/DataStructures/Lisp/Lists.mac")$
00024 oklib_include("OKlib/ComputerAlgebra/Satisfiability/Lisp/ClauseSets/BasicOperations.mac")$
00025 oklib_include("OKlib/ComputerAlgebra/Satisfiability/Lisp/ConflictCombinatorics/HittingClauseSets.mac")$
00026 
00027 
00028 /* ********************************
00029    * Performing single extensions *
00030    ********************************
00031 */
00032 
00033 /* Compute a new variable for a clause-set; likely best suited
00034    if variables are numeric, but can be applied also in other
00035    cases. */
00036 new_var_fcs(FF) := if emptyp(FF[1]) then 1 else lmax(FF[1])+1$
00037 
00038 /* Returns a sublist obtained from set or list S by including each
00039    element with probability p. */
00040 random_sublist(S,p) := 
00041  if p = 1 then listify(S)
00042  elseif p = 0 then []
00043  else block([res : []],
00044    for x in S do
00045      if random(1.0) < p then res : cons(x,res),
00046    res)$
00047 
00048 /* Perform inverse singular DP-reduction on FF, by adding
00049    a new clause containing the new singular variable v,
00050    and replacing the clauses in G by clauses containing -v. */
00051 /* Changes FF in-place, always returns true. */
00052 /* p regulates how many of the possible literals
00053    are included into the v-clause (as a choice-probability).
00054    while q regulates how many of these literals are included
00055    into the (-v)-clauses (that is, first C0 as as subset of the
00056    intersection of G is determined, containing each literal of the
00057    intersection with probability p, and then each clause of FF - G
00058    is considered, the elements of C0 are removed, and then each
00059    literal of C0 is added with probability q).
00060    <ul>
00061     <li> p=1, q=1 is the case that all clauses are as large as possible.
00062     These are the "hitting extensions", provided that FF is hitting,
00063     and that the intersection of the clauses in G clashes with all
00064     the clauses in FF minus G (see below). </li>
00065     <li> q=0,p=0 is the case of just introducing new unit-clauses (with
00066     new variables), while q=0 in general are the marginal extension
00067     (all clauses minimal). </li>
00068     <li> p=0 implies q=0. </li>
00069     <li> p=1, q=0 is an interesting marginal case, where
00070     the singular clause are as large as possible: it corresponds
00071     to factoring-out (all) common literals in the given clauses G. </li>
00072    </ul>
00073 */
00074 /* Prerequisite: G is a non-empty subset of FF[2];
00075    p, q are integers or reals with 0 <= p,q <= 1. 
00076 */
00077 basic_inverse_singulardp_fcs(FF,G,p,q) := block(
00078  [I : lintersection(G), v : new_var_fcs(FF), C0 : {}],
00079   FF[1] : adjoin(v,FF[1]),
00080   C0 : setify(random_sublist(I,p)),
00081   FF[2] : setdifference(FF[2],G),
00082   FF[2] : adjoin(adjoin(v,C0),FF[2]),
00083   for D in G do block([E : setdifference(D,C0)],
00084     FF[2] : adjoin(adjoin(-v,union(E,setify(random_sublist(C0,q)))),FF[2])),
00085   return(true))$
00086 
00087 hitting_extension_fcs(FF,G) := basic_inverse_singulardp_fcs(FF,G,1,1)$
00088 
00089 /* Testing whether G yields a "pre-hitting-extension", that is, G is a 
00090    non-empty sub-clause-set of FF such that the intersection of G clashes with
00091    every clause from FF - G.
00092 */
00093 /* TODO: this should better be called "hitting-divisor". */
00094 pre_hitting_extension_fcs_p(FF,G) := subsetp(G,FF[2]) and not emptyp(G) and
00095  block([I : lintersection(G)], every_s(lambda([C], clashp(C,I)), setdifference(FF[2],G)))$
00096 hittingdivisor_fcs_p(FF,G) := pre_hitting_extension_fcs_p(FF,G)$
00097 
00098 /* For a "hitting extension", G additionally needs to be a hitting clause-set
00099    (which is automatically fulfilled if FF is hitting):
00100 */
00101 hitting_extension_fcs_p(FF,G) := pre_hitting_extension_fcs_p(FF,G) and
00102  hittingcsp(G)$
00103 
00104 /* The set of all pre-hitting extensions (as formal clause-sets) of
00105    formal clause-set FF:
00106 */
00107 all_pre_hitting_extensions_fcs(FF) := 
00108  map(lambda([G], block([FF2 : copy(FF)], hitting_extension_fcs(FF2,G), FF2)), 
00109      subset(disjoin({},powerset(FF[2])), lambda([G], pre_hitting_extension_fcs_p(FF,G))))$
00110 
00111 /* The smallest superset of G such that hittingdivisor_fcs_p(cs2fcs(F),G)
00112    holds, where F is a clause-set, G is a non-empty sub-clause-set of F:
00113 */
00114 hittingdivisor_extension_cs(F,G) := block([EG, I : lintersection(G)],
00115   while not emptyp(
00116     EG : subset(setdifference(F,G), lambda([C], not clashp(C,I)))) do
00117       (G : union(G,EG), I : intersection(I,lintersection(EG))),
00118   G)$
00119 
00120 
00121 /* ********************************
00122    * Performing random extensions *
00123    ********************************
00124 */
00125 
00126 /* Find a random subset of a set-system, of size exactly s and 
00127    with intersection size at least i; return false in case it 
00128    doesn't exist. */
00129 random_subset_si(S,s,i) := if s=0 then {} else
00130 block([found : false],
00131   for A in random_permutation(powerset(S,s)) unless found # false do
00132     if length(apply(intersection,listify(A))) >= i then
00133       found : A,
00134   return(found))$
00135 
00136 /* Applies inverse singular DP-reduction, where a is the minimal number of 
00137    literals other than the singular variable for the "singular" clause
00138    before applying the random selection, and b is the (exact) number of
00139    negative occurrences. */
00140 /* Changes FF in-place, and returns false in case the transformation
00141    is impossible, and true otherwise. */
00142 /* Prerequisites: a >= 0, b >= 1 */
00143 si_inverse_singulardp_fcs(FF,p,q,a,b) := block(
00144  [G : random_subset_si(FF[2],b,a)],
00145   if G = false then return(false)
00146   else return(basic_inverse_singulardp_fcs(FF,G,p,q)))$
00147 
00148 /* Simply iterating si_inverse_singulardp_fcs N times, aborting in
00149    case of failure, and returning the number of successful transformations.
00150 */
00151 it_si_inverse_singulardp_fcs(FF,p,q,a,b,N) := block([aborted : false],
00152   for i : 1 thru N unless aborted # false do
00153     if not si_inverse_singulardp_fcs(FF,p,q,a,b) then
00154       aborted : i-1,
00155   if aborted # false then return(aborted)
00156   else return(N))$
00157