OKlibrary  0.2.1.6
InclusionExclusion.mac
Go to the documentation of this file.
00001 /* Oliver Kullmann, 3.2.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/Satisfiability/Lisp/ConflictCombinatorics/Conflicts.mac")$
00023 oklib_include("OKlib/ComputerAlgebra/Hypergraphs/Lisp/SetSystems.mac")$
00024 oklib_include("OKlib/ComputerAlgebra/Satisfiability/Lisp/ClauseSets/Constructions.mac")$
00025 oklib_include("OKlib/ComputerAlgebra/Satisfiability/Lisp/ConflictCombinatorics/HittingClauseSets.mac")$
00026 oklib_include("OKlib/ComputerAlgebra/Satisfiability/Lisp/ClauseSets/Statistics.mac")$
00027 
00028 
00029 /* The probability of a satisfying assignment computed via the Iwama-formula
00030    ([Iwama, 1989, CNF satisfiability test by counting and polynomial average
00031    time]). 
00032    Computing the independent sets via the recursive-splitting-transversal
00033    algorithm. */
00034 satprob_mcind_trrs(F) := block([MI : listify(cind_cs_trrs(F)[2])],
00035   sum((-1)^(ncl_cs(MI[i])) * 2^(-nvar_cs(MI[i])), i,1,length(MI)))$
00036 
00037 /* Computes the full list of approximations of satprob(F) of length
00038    independence_number_cs(F) + 1 */
00039 /* The first element is always 1, the second element is a lower bound (assuming the
00040    falsifying assignments for different clauses are different). The last element
00041    is the true probability. */
00042 satprob_seqap_mcind_trrs(F) := block([MI : cind_cs_trrs(F)[2], r, appr, res],
00043   r : lmax(map(length,MI)), appr : make_array(fixnum, r+1),
00044   for S in MI do block([l : length(S)],
00045     appr[l] : appr[l] + (-1)^(ncl_cs(S)) * 2^(-nvar_cs(S))),
00046   res : [appr[0]],
00047   for i : 1 thru r do
00048     res : endcons(appr[i]+last(res), res),
00049   return(res))$
00050 /* The second element of that list (compare firstorder_sat_approx) */
00051 satprob_hitting(F) := 1 - weighted_ncl_2n_cs(F)$
00052 satprob_hitting_f(FF) := satprob_hitting(FF[2])$
00053 
00054 /* Direct application of inclusion/exclusion to a clause-set represented via
00055    a list of hitting clause-sets (as their union).
00056    According to [Dubois 1991, Counting the number of solutions for instances
00057    of satisfiability, TCS]. */
00058 satprob_incexl_hitting(L) := if emptyp(L) then 1 else
00059  block([P : powerset(setn(length(L)))],
00060   P : listify(disjoin({},P)),
00061   return(sum(
00062           satprob_hitting(apply(or_cs,create_list(L[i],i,listify(P[p])))) * 
00063             (-1)^(length(P[p])-1),
00064           p, 1, length(P))))$
00065 
00066 /* Using the partitioning into hitting clause-sets via the maxima
00067    max-clique function */
00068 satprob_incexl_hitting_hcm(F) := satprob_incexl_hitting(hitting_decomposition_m_cs(F))$
00069