OKlibrary  0.2.1.6
SplittingAnalysis.mac
Go to the documentation of this file.
00001 /* Oliver Kullmann, 24.4.2008 (Guangzhou) */
00002 /* Copyright 2008, 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/Satisfiability/Lisp/MinimalUnsatisfiability/Cores.mac")$
00024 oklib_include("OKlib/ComputerAlgebra/Satisfiability/Lisp/Reductions/DP-Reductions.mac")$
00025 
00026 /* Compute a sequence of minimally unsatisfiable clause-sets as subsets
00027    of a given clause-set under random splitting. */
00028 /* The sequence starts with a minimally unsatisfiable sub-clause-set
00029    of the given clause-set, then one where the first variable is set
00030    to a random value, etc. */
00031 /* Prerequisite: F is unsatisfiable. */
00032 /* This is a sort of a "random generator" for minimally unsatisfiable
00033     clause-sets. */
00034 random_splitting_mus(F, seed, solver) := block(
00035  [FF, V, v, eps,
00036   generator_state : make_random_state(seed)],
00037   set_random_state(generator_state),
00038   FF : first_mus_fcs(cs_to_fcs(F), solver),
00039   F : FF[2], V : var_cs(F),
00040   if emptyp(V) then return([F]),
00041   v : listify(V)[1 + random(length(V))],
00042   eps : random(2) * 2 - 1,
00043   return(cons(F,random_splitting_mus(apply_pa({eps * v},F), seed, solver))))$
00044 /* The variation where automatically singular DP-reduction is applied. */
00045 random_splitting_nsing_mus(F, seed, solver) := block(
00046  [FF, V, v, eps,
00047   generator_state : make_random_state(seed)],
00048   set_random_state(generator_state),
00049   F : sdp_reduction_cs(F),
00050   FF : first_mus_fcs(cs_to_fcs(F), solver),
00051   F : sdp_reduction_cs(FF[2]), V : var_cs(F),
00052   if emptyp(V) then return([F]),
00053   v : listify(V)[1 + random(length(V))],
00054   eps : random(2) * 2 - 1,
00055   return(cons(F,random_splitting_nsing_mus(apply_pa({eps * v},F), seed, solver))))$
00056 
00057