OKlibrary  0.2.1.6
OKsolver2002.mac
Go to the documentation of this file.
00001 /* Oliver Kullmann, 19.1.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 
00023 oklib_include("OKlib/ComputerAlgebra/Satisfiability/Lisp/Backtracking/DLL_solvers.mac");
00024 
00025 weightingscheme_OKsolver2002(k) :=
00026   if k = 2 then 1
00027   elseif k = 3 then 0.2
00028   elseif k = 4 then 0.05
00029   elseif k = 5 then 0.01
00030   elseif k = 6 then 0.003
00031   else 20.4514 * 0.218673^k$
00032 
00033 distances_OKsolver2002 : 
00034   [wn_newclauses_2(weightingscheme_OKsolver2002), delta_n]$
00035 
00036 heuristics_OKsolver2002 : 
00037   heuristics_lookahead_distances(
00038     generalised_ucp1,
00039     distances_OKsolver2002,
00040     [prod_proj],
00041     logprobrand)$
00042 aheuristics_OKsolver2002 : 
00043   amended_heuristics_lookahead_distances(
00044     generalised_ucp1,
00045     distances_OKsolver2002,
00046     [prod_proj],
00047     logprobrand,
00048     [])$
00049 
00050 
00051 /* The following abstraction of OKsolver_2002 ignores: 
00052   - clause-sets are for the OKsolver_2002 clause-*lists*;
00053   - the order of variables and clauses;
00054   - rounding errors regarding the heuristics;
00055   - tree pruning ("intelligent backtracking"), and so we
00056     specify actually "OKsolver_2002_NTP".
00057 */
00058 
00059 OKsolver_2002(FF) := dll_red(FF, heuristics_OKsolver2002, generalised_ucp_ple1)$
00060 OKsolver_2002_st(FF) := dll_red_st(FF, heuristics_OKsolver2002, generalised_ucp_ple1)$
00061 OKsolver_2002_ast(FF) := dll_red_st_dist(FF, aheuristics_OKsolver2002, generalised_ucp_ple1)$
00062 
00063 /*
00064  Splitting trees produced by OKsolver_2002_st for unsatisfiable clause-sets
00065  are r_2-splitting trees.
00066 */
00067