OKlibrary  0.2.1.6
Backtracking.mac
Go to the documentation of this file.
00001 /* Oliver Kullmann, 3.4.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/Backtracking/SplittingTrees.mac");
00023 oklib_include("OKlib/ComputerAlgebra/Satisfiability/Lisp/Backtracking/DLL_solvers.mac");
00024 
00025 
00026 /* For a SAT solver S returning a splitting tree, return a function from
00027    formal clause-sets to (precise) SAT-probabilities. */
00028 satprob_dll_generic(S) := buildq([S], lambda([FF],
00029  count_sat_st(S(FF),FF[1]) / 2^(length(FF[1]))))$
00030 /* Convenience instantiations: */
00031 satprob_dll_simplest_trivial1 : satprob_dll_generic(dll_simplest_st_trivial1)$
00032 
00033