OKlibrary  0.2.1.6
DLL_solvers.hpp File Reference

Plans for DLL-solvers. More...

Go to the source code of this file.


Detailed Description

Plans for DLL-solvers.

Todo:
Organisation
  • Split DLL_solvers.mac into several submodules.
Todo:
Heuristics, distances etc.
  • Likely these things should go into a dedicated module.
  • We should also implement the well-known branching rules from the literature as heuristics (but in the documentation we should somehow emphasise their "historical status").
    1. Jeroslow-Wang ([Jeroslow, Wang, 1990, Solving propositional satisfiability problems])
    2. 2-sided Jeroslow-Wang ([Hooker, Vinay, 1995, Branching rules for satisfiability])
    3. dsj ([Van Gelder, Tsuji, 1996, Satisfiability Testing with More Reasoning and Less Guessing])
    4. B ([Ouyang, 1999, Implementations of the DPLL algorithm])
    5. MAR ([van Maaren, Warners, 2000, Solving satisfiability problems using elliptic approximations --- Effective branching rules]); based on using var_int_scom_fcs (ComputerAlgebra/Satisfiability/Lisp/ClauseSets/Hypergraphs.mac). Additionally here we need appropriate weights for clause-lengths.
Todo:
Concepts for heuristics
  • Instead of passing arguments, one could use "inheritance", i.e., dynamic binding, for heuristic-functions?

Definition in file DLL_solvers.hpp.