OKlibrary  0.2.1.6
DLL_solvers.mac
Go to the documentation of this file.
00001 /* Oliver Kullmann, 17.2.2008 (Swansea) */
00002 /* Copyright 2008, 2009 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 
00021 oklib_include("OKlib/ComputerAlgebra/Satisfiability/Lisp/Backtracking/DLL_solvers.mac")$
00022 oklib_include("OKlib/ComputerAlgebra/Satisfiability/Lisp/Backtracking/tests/DLL_solvers.mac")$
00023 
00024 /* **********************************
00025    * Backtracking without reduction *
00026    **********************************
00027 */
00028 
00029 okltest_dll_simplest(dll_simplest);
00030 okltest_dll_simplest_spa(dll_simplest_spa);
00031 
00032 /* ***********************************
00033    * Backtracking with r_k-reduction *
00034    ***********************************
00035 */
00036 
00037 
00038 /* *****************************************
00039    * Backtracking with arbitrary reduction *
00040    *****************************************
00041 */
00042 
00043 
00044 /* *******************************
00045    * Simple heuristics for DLL   *
00046    *******************************
00047 */
00048 
00049 okltest_choose_most_sat_literal_h(choose_most_sat_literal_h);
00050 
00051 okltest_johnson_heuristic(johnson_heuristic);
00052 
00053 okltest_dll_heuristics_max_lit_tb(dll_heuristics_max_lit_tb);
00054 
00055 /* ****************************
00056    * Heuristics via distances *
00057    ****************************
00058 */
00059 
00060 okltest_ast2tbt(ast2tbt);
00061 
00062 okltest_check_inf_branches_ast(check_inf_branches_ast);
00063 
00064 okltest_collapse_inf_branches_ast(collapse_inf_branches_ast);
00065 
00066 /* *************
00067    * Distances *    
00068    *************
00069 */
00070 
00071 
00072 /* ***************
00073    * Projections *
00074    ***************
00075 */
00076 
00077 
00078 /* *********************************
00079    * Satisfiability approximations *
00080    *********************************
00081 */
00082 
00083 okltest_locallemma_satapprox(locallemma_satapprox);
00084 okltest_locallemmasum_satapprox(locallemmasum_satapprox);
00085