OKlibrary  0.2.1.6
Cores.mac
Go to the documentation of this file.
00001 /* Oliver Kullmann, 8.4.2008 (Swansea) */
00002 /* Copyright 2008, 2009, 2010, 2012 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/ClauseSets/BasicOperations.mac")$
00023 oklib_include("OKlib/ComputerAlgebra/Hypergraphs/Lisp/SetSystems.mac")$
00024 oklib_include("OKlib/ComputerAlgebra/Satisfiability/Lisp/MinimalUnsatisfiability/Basics.mac")$
00025 oklib_include("OKlib/ComputerAlgebra/Hypergraphs/Lisp/Basics.mac")$
00026 oklib_include("OKlib/ComputerAlgebra/Satisfiability/Lisp/Backtracking/DLL_solvers.mac")$
00027 
00028 
00029 /* *************************************************
00030    * Minimally unsatisfiable cores of minimum size *
00031    *************************************************
00032 */
00033 
00034 /* Returns the minimum size of a minimally unsatisfiable sub-clause-set
00035    of clause-set F; uses sat-solver S: */
00036 min_size_mus_bydef(F, S) := if S([var_cs(F),F]) then inf else
00037  block([k : 0, scls : {}],
00038   while every_s(lambda([G], S([var_cs(G),G])), scls) do (
00039    k : k+1, scls : powerset(F, k)),
00040  return(k))$
00041 
00042 /* Decides whether clause-set F contains a (minimally) unsatisfiable
00043    sub-clause-set of size at most k; uses sat-solver S */
00044 contains_us_bydef(F, k, S) :=
00045  not every_s(lambda([G], S([var_cs(G),G])), powerset(F,min(k,ncl_cs(F))))$
00046 
00047 
00048 /* ***********************************
00049    * Computing all irredundant cores *
00050    ***********************************
00051 */
00052 
00053 /* The set of all irredundant cores of a formal clause-set, using
00054    solver S. */
00055 
00056 monitor_message_all_irr_cores_bydef() :=
00057   if oklib_monitor and oklib_monitor_level >= 1 then
00058     print("all_irr_cores_bydef: ENTRY;", statistics_fcs(FF))$
00059 
00060 all_irr_cores_bydef(FF,S) := block(
00061  [counter_irr : 0, potentially_unusable_clauses : false],
00062   monitor_message_all_irr_cores_bydef(),
00063   all_forced_irr_cores_bydef({}, FF[2], S))$
00064 all_irr_cores_bydef_fcs(FF) := all_irr_cores_bydef(FF,current_satsolver)$
00065 all_irr_cores_bydef_cs(F) := all_irr_cores_bydef_fcs(cs2fcs(F))$
00066 
00067 /* All minimally unsatisfiable cores of an unsatisfiable formal clause-set: */
00068 all_min_usat_cores_bydef(FF,S) := all_irr_cores_bydef(FF,S)$
00069 all_min_usat_cores_bydef_fcs(FF) := all_min_usat_cores_bydef(FF,current_satsolver)$
00070 all_min_usat_cores_bydef_cs(F) := all_min_usat_cores_bydef(cs2fcs(F),current_satsolver)$
00071 
00072 
00073 /* The set of all irredundant cores of union(Forced,Possible) which contain
00074    the given "forced" clauses. Prerequisite: Forced, Possible are disjoint. */
00075 /* Uses inherited variables counter_irr and potentially_unusable_clauses. */
00076 
00077 monitor_message_1_all_forced_irr_cores_bydef() :=
00078   if oklib_monitor and oklib_monitor_level >= 1 then (
00079     print("all_forced_irr_cores_bydef: Entry"),
00080     print("Forced:", statistics_cs(Forced)),
00081     print("Possible:", statistics_cs(Possible)))$
00082 monitor_message_2_all_forced_irr_cores_bydef() :=
00083   if oklib_monitor then (
00084     counter_irr : counter_irr + 1,
00085     print("all_forced_irr_cores_bydef: found no.", counter_irr, ",", statistics_cs(Forced)),
00086     if oklib_monitor_level >= 2 then print(Forced))$
00087 
00088 all_forced_irr_cores_bydef(Forced, Possible, S) := block(
00089  monitor_message_1_all_forced_irr_cores_bydef(),
00090  block( /* find new forced clauses */
00091   [Possible_old : Possible, F : union(Forced, Possible), V],
00092    V : var_cs(F),
00093    for C in Possible_old do (
00094      if not impliesp_f([V,disjoin(C,F)],C,S) then (
00095        Possible : disjoin(C,Possible),
00096        Forced : adjoin(C,Forced)))),
00097  if potentially_unusable_clauses and not irredundant_bydef(cs_to_fcs(Forced),S) then return({}),
00098  block( /* remove superfluous clauses */
00099   [Possible_old : Possible, V : var_cs(Forced)],
00100    for C in Possible_old do
00101      if impliesp_f([V,Forced],C,S) then Possible : disjoin(C,Possible)),
00102  /* now compute solutions */
00103  if emptyp(Possible) then (
00104    monitor_message_2_all_forced_irr_cores_bydef(),
00105    return({Forced})),
00106  block([C : choose_element(Possible), Cores_without_C],
00107   Possible : disjoin(C,Possible),
00108   Cores_without_C : all_forced_irr_cores_bydef(Forced, Possible,S),
00109   Forced : adjoin(C,Forced), potentially_unusable_clauses : true,
00110   return(union(Cores_without_C, all_forced_irr_cores_bydef(Forced,Possible,S)))))$
00111 
00112 
00113 /* *************************************************
00114    * Heuristical search for some irredundant cores *
00115    *************************************************
00116 */
00117 
00118 /* Returns some minimally unsatisfiable sub-clause-set of input FF,
00119    a formal unsatisfiable clause-set (trivial heuristics, removing
00120    the first possible clause). */
00121 /* The set of variables of the result is the original set. */
00122 /* RENAME: first_mus_fcsss */
00123 first_mus_fcs(FF, S) := block(
00124  [V : FF[1], F : FF[2], Core : {}],
00125   for C in FF[2] do (
00126       if S([V, disjoin(C,F)]) then Core : adjoin(C,Core)
00127       else F : disjoin(C,F)),
00128   return([V,Core]))$
00129 /* RENAME: first_mus_csss */
00130 first_mus_cs(FF, S) := fcs2cs(first_mus_fcs(cs2fcs(F),S))$
00131 
00132 /* RENAME: first_mus_fcs */
00133 first_mus_bs_fcs(FF) := first_mus_fcs(FF, current_satsolver)$
00134 /* RENAME: first_mus_cs */
00135 first_mus_bs_cs(F) := first_mus_cs(F, current_satsolver)$
00136 
00137 /* More generally, returns some irredundant core of input FF,
00138    (trivial heuristics, removing the first possible clause). */
00139 first_irr_fcs(FF, S) := block(
00140  [V : FF[1], F : FF[2], Core : {}],
00141     for C in FF[2] do
00142       if not impliesp_f([V,disjoin(C,F)],C,S) then
00143         Core : adjoin(C,Core)
00144       else F : disjoin(C,F),
00145   return([V,Core]))$
00146 
00147 
00148 /* *********************************
00149    * Sampling of irredundant cores *
00150    *********************************
00151 */
00152 
00153 /* A sample of at most N elements of the set of all irredundant cores,
00154    where for the recursive branching with probability p first the left
00155    branch is taken (not including the considered clause). */
00156 sample_irr_cores(FF,Solver,Count,branch_probability,seed) := block(
00157  [counter_irr : 0,
00158   potentially_unusable_clauses : false,
00159   generator_state : make_random_state(seed)],
00160   set_random_state(generator_state),
00161   monitor_message_all_irr_cores_bydef(),
00162   sample_forced_irr_cores({}, FF[2]))$
00163 
00164 /* The set of all irredundant cores of union(Forced,Possible) which contain
00165    the given "forced" clauses. Prerequisite: Forced is irredundant. */
00166 /* Uses inherited variable Solver, Count, branch_probability and
00167    counter_irr, potentially_unusable_clauses. */
00168 sample_forced_irr_cores(Forced, Possible) := block(
00169  if Count <= 0 then return({}),
00170  monitor_message_1_all_forced_irr_cores_bydef(),
00171  block( /* find new forced clauses */
00172   [Possible_old : Possible, F : union(Forced, Possible), V],
00173    V : var_cs(F),
00174    for C in Possible_old do (
00175      if not impliesp_f([V,disjoin(C,F)],C,Solver) then (
00176        Possible : disjoin(C,Possible),
00177        Forced : adjoin(C,Forced)))),
00178  if potentially_unusable_clauses and not irredundant_bydef(cs_to_fcs(Forced),Solver) then return({}),
00179  block( /* remove superfluous clauses */
00180   [Possible_old : Possible, V : var_cs(Forced)],
00181    for C in Possible_old do
00182      if impliesp_f([V,Forced],C,Solver) then Possible : disjoin(C,Possible)),
00183  /* now compute solutions */
00184  if emptyp(Possible) then (
00185    Count : Count - 1,
00186    monitor_message_2_all_forced_irr_cores_bydef(),
00187    return({Forced})),
00188  block([C : choose_element(Possible)],
00189   Possible : disjoin(C,Possible),
00190   if random(1.0) <= branch_probability then block([Cores_without_C],
00191     Cores_without_C : sample_forced_irr_cores(Forced, Possible),
00192     Forced : adjoin(C,Forced), potentially_unusable_clauses : true,
00193     return(union(Cores_without_C, sample_forced_irr_cores(Forced,Possible))))
00194   else block([Cores_with_C],
00195     potentially_unusable_clauses : true,
00196     Cores_with_C : sample_forced_irr_cores(adjoin(C,Forced), Possible),
00197     return(union(Cores_with_C, sample_forced_irr_cores(Forced,Possible))))))$
00198 
00199 
00200 /* ********************************************
00201    * Maximally non-equivalent sub-clause-sets *
00202    ********************************************
00203 */
00204 
00205 /* The set of sub-clause-sets of clause-set F, which are not equivalent to
00206    some given boolean function F_0, and which are maximal w.r.t. this
00207    property.
00208    EQp(F) decides whether F is equivalent to this underlying F_0 or not.
00209    It is assumed that if EQp(G) is true for G <= F, then also EQp(G') is
00210    true for all G <= G' <= F.
00211 */
00212 all_max_noneq_scs_bydef(F,EQp) := if F = {} then
00213  if EQp({}) then {} else {{}}
00214  else all_forced_max_noneq_scs_bydef({},F,{})$
00215 
00216 /* The variation where the elements of Forced need to be taken,
00217    and the whole F is union(Forced,Possible,Removed). */
00218 /* Inherits EQp. Invariant: EQp(Forced) is false. */
00219 all_forced_max_noneq_scs_bydef(Forced,Possible,Removed) := block(
00220  [extension : []],
00221  for C in Possible while emptyp(extension) do
00222    if not EQp(adjoin(C,Forced)) then extension : [C],
00223  if emptyp(extension) then (
00224    extension : false,
00225    for C in Removed unless extension do
00226      if not EQp(adjoin(C,Forced)) then extension : true,
00227    if extension then return({}) else return({Forced}))
00228  else block([C : extension[1]],
00229    Possible : disjoin(C,Possible),
00230    return(union(
00231      all_forced_max_noneq_scs_bydef(adjoin(C,Forced),Possible,Removed),
00232      all_forced_max_noneq_scs_bydef(Forced,Possible,adjoin(C,Removed))))))$
00233 
00234 /* The special case where F is unsatisfiable: */
00235 all_max_sat_scs_bydef(F,S) :=
00236  all_max_noneq_scs_bydef(F,buildq([S],lambda([G],not(S(cs_to_fcs(G))))))$
00237 
00238 /* Delivers a generic equivalence-checker for sub-clause-sets: */
00239 equivalence_checker_scl_bydef(F,S) :=
00240  buildq([F,S],lambda([G],every_s(lambda([C],impliesp(G,C,S)),setdifference(F,G))))$
00241 
00242 /* All maximally non-equivalent sub-clause-sets of clause-set F: */
00243 /* Remark: For unsatisfiable F use all_max_sat_scs_bydef. */
00244 all_max_neq_scs_bydef(F,S) := all_max_noneq_scs_bydef(F,equivalence_checker_scl_bydef(F,S))$
00245 
00246 
00247 /* ************************************
00248    * Duality between MAXSAT and MUSAT *
00249    ************************************
00250 */
00251 
00252 /* The irredundant cores are exactly the minimal transversals of
00253    the complements of maximally not-equivalent sub-clause-sets,
00254    and vice versa. */
00255 
00256 /* Given a function for computing all irredundant cores (from formal
00257    clause-sets), and a function for computing hypergraph transversals,
00258    compute all maximally
00259    not-equivalent sub-clause-sets. */
00260 all_max_neq_scs_bydual(F,f_irr_cores,f_hyp_trans) :=
00261   ecomp_hyp(f_hyp_trans([F,f_irr_cores(cs_to_fcs(F))]))[2]$
00262 /* Given a function for computing all maximally not-equivalent
00263    sub-clause-sets (for a clause-set), compute all irredundant cores. */
00264 all_irr_cores_bydual(FF,f_all_max_neq,f_hyp_trans) :=
00265   f_hyp_trans(ecomp_hyp([FF[2],f_all_max_neq(FF[2])]))[2]$
00266 
00267