Dimetheus

Overview

Dimetheus is a SAT solver, an algorithm that is able to decide whether a given Boolean formula is in the language SAT. Check this page for details on propositional logic and SAT.

The Dimetheus solver follows the LAE design approach for highly modular hybrid portfolio solvers. Check this page for more information on the LAE.

The menu to the right allows you to browse specific sub-topics regarding the Dimetheus solver.

Introduction

The name Dimetheus is a neologism which results from a combination of the words Prometheus (the ''forethinker'') and Epimetheus (the ''afterthinker''). The name is supposed to capture the modularity of the solver. Several modules like CDCL are ''afterthinkers''. They perform agressive search without thinking too much on what is useful or not and analyze the situation only after something goes ''wrong''. Other modules like MP are ''forethinkers''. These modules do not advance the search but they somehow analyze the situation and suggest what would be best in order to advance the search. The two types of modules therefore complement each other.

The ''forethinkers'' and the ''afterthinkers'' are wired together using (search) strategies that define what module is to do what action in what situation. Thereby, the ''forethinkers'' can provide the ''afterthinkers'' with valuable heuristical information. The ''afterthinkers'' can provide the ''forethinkers'' with additional data in order for them to refine their thinking.

Dimetheus has been tested substantially using a CNF fuzzer written by Armin Biere, as well as a memory profiling tool called Valgrind. However, we do not live in a perfect world. So in case you find any bugs or strange behavior, do not hesitate and write me an email.

The major design goals of Dimetheus are as follows.

  • Accessibility. Dimetheus is research software and as such, it is intended to be studied by others. I did my best to write mnemonic code and tried to comment it clearly and pretty exhaustively.
  • Flexibility, Maintainability, and Extensibility. Dimetheus is a large scale software with several 10.000 lines of code. In order to be able to extend and maintain it, I followed the LAE concept. This concept ensures a highly modular and easily extensible software.
  • Robustness. The solver should be as robust as possible. It does various checks on the consistency of parameters, the given formulas, and is very cautious with presenting any results. Furthermore, given the large set of search-, inprocessing-, and preprocessing-modules, it is also able to solve a wide variety of CNF formulas.
  • Performance. Each of the modules and search strategies is implemented in a way that guarantees maximum performance without violating the above design goals.

As clarified by the LAE, solving a CNF formula with Dimetheus is done in phases.

Phases of Solving

The Dimetheus solver implements the following phases of the LAE design concept.

  • RESET: This phase resets all the memory. It initializes values to zero and pointers to NULL. Also, all strategy pointers are pointing to a NULL strategy with empty methods.
  • PARAMS: This phase reads the parameters and checks them for consistency. After this phase, all parameters have been read from the command line and seem to make sense. It also ensures that mandatory parameters are given.
  • GUIDANCE: Guides are hard-wired sets of parameters. Selecting a guide is done via the command line. If a guide was selected, it will try to enforce all internal parameters such that the target of the guide is satisfied. This might result in an error if the user provided ambigious parameters at the command line that are in conflict with the guide. The idea behind guides is that you do not have to provide parameters anymore (except for the mandatory formula filename) -- or that the parameters you must provide are confined to a very small set.
  • STARTUP: This phase actually loads the formula from file or via interface. It detects what input format is used and might translate an arbitrary propositional logic formula into CNF. This phase also verifies that the input actually is correct (obeys all rules for the specific input format).
  • CLASSIFY: The classification will compute all the attributes of the formula and provides them in an attribute vector. It furthermore determines a CNF class (a problem type) that the formula belongs to.
  • ADAPT: The adaptation will choose for all the adaptable strategies and parameters the best setting for the given formula class. It may use the computed properties of the attribute vector provided by the previous phase. The adaptation will obey the selected guide. In other words, it only adapts what it is allowed to adapt.
  • PREPROCESS: In the preprocessing phase, the solver will follow the given preprocessing strategy in order to simplify the given formula.
  • SEARCH (including INPROCESS): The search phase actually does search if this should be necessary. It will follow the given search strategy and calls for the search modules (like SLS, CDCL, MP) to perform the search. The search phase might call for the inprocessing phase. The inprocessing phase is pretty much like the preprocessing phase in the sense that it tries to simplify the remaining formula by following its selected inprocessing strategy.
  • HANDLERESULT: In case the search strategy terminates, this phase will make sure that the result is printed correctly. This also includes a solution reconstruction in case the preprocessor performed things like NIVER or GE or ACCE. Printing the result might also output statistical data that has been gathered during the search.
  • SHUTDOWN: This phase ensures that all not yet freed memory is freed. Actually, the completion of this phase resets the solver into a state similar to the RESET phase.

Phases consist of modules that group functionality.

Modules within Phases

The execution of each phase might trigger the execution of modules that reside within a phase. For example, the PREPROCESS phase might call for the module PRE that implements a preprocessor. The modules that are currently available sorted by phase are as follows.

  • STARTUP contains DETERM, SPECCER, and LOADER.
  • CLASSIFY contains ATTRIBUTOR and RANDOMFOREST.
  • ADAPT contains ITEADAPTER.
  • PREPROCESS contains PRE.
  • SEARCH contains MP, SLS, CDCL and the phase INPROCESS.
  • INPROCESS contains IN.

Each of the modules can perform a specific task. The SLS for example does Stochastic Local Search. It is worth noting that due to the modularity of the software, one can easily add more modules (like SLS2, SLS3, or whatever).

Each module can contain a set of plug-ins that implement certain features that might be realized in different ways. For example in the SLS, the pickAndFlipVarRules plug-in is supposed to perform the flipping in the SLS. This can, however, be realized according to WalkSAT, ProbSAT, or any other hyped local search heuristic.

Plug-Ins within Modules

The list of plug-ins for each (currently available) module along with some of the realizations it provides is as follows (these lists are not complete and are subject to changes during the ongoing development).

  • DETERM: Determines the input format used for presenting a propositional formula. Currently, this module does not have any plug-ins.
  • SPECCER: Translates the formula into CNF (if that is necessary) and determines the CNF specifications (number of variables, number of clauses). Currently, this module does not have any plug-ins.
  • LOADER: Load the CNF into the CNF data-structures of the solver. Currently, this module does not have any plug-ins.
  • ATTRIBUTOR: Compute all attributes of the formula in order to use them in a classification process. Currently, this module does not have any plug-ins.
  • RANDOMFOREST: Classify the formula using the attributes with a random forest approach. Currently, this module does not have any plug-ins.
  • ITEADAPTER: Does the adaptation. Determines strategies and parameter settings. Currently, this module does not have any plug-ins.
  • SLS: Does Stochastic Local Search. It tries to find a total and satisfying assignment. This module performs incomplete search. In contains the following plug-ins.
    • datastructures: Special SLS friendly representation of the remaining formula.
    • pickAndFlipVarRules[WalkSAT, ProbSAT]: Pick and flip the assignment of a single variable.
    • assInitRules[Provided, Random]: Determines how to initialize the starting assignment for the local search.
    • tryRestartRules[SingleUnlimited, Const, Linear, ...]: Determines how often and in what way the SLS solver performs restarts.
  • MP: Does Message Passing. It tries to estimate biases for all the variables. The biases give an indication what variables are highly constrained (have a large numerical abstract value) and in what direction the variable should be assigned first if one tries to find a satisfying assignment. MP contains the following plug-ins.
    • datastructures: Special MP friendly representation of the remaining formula.
    • updateRules[BP, SP, EMBPG, EMSPG, ijMPP]: The update rules actually implement the message passing process and send around disrespect and warning messages. They are also updating the biases according to their style of message passing. The ijMPP version is what I developed in my Ph.D. thesis..
  • CDCL: Does conflict driven clause learning. It tries to construct a complete assignment from scratch and might learn new clauses on the way. This module performs complete search if the abort rule is NULL. The CDCL module contains the following plug-ins.
    • datastructures: Special CDCL friendly representation of the remaining formula.
    • abortRules[NULL, GENIEBBCDCL]: Early abort the search with return code unknown but keep currently learned clauses and assignments.
    • computeBJLRule[FirstAssert]: Computes the back-jump level after learning a conflict clause.
    • conflictAnalysisRule[AllDec, AllUIP, FirstUIP, LastUIP]: In the conflicting state, this plug-in extracts the reason for this conflict to arise and learns a new clause from it.
    • inprocessingRules[NULL, ReduceOnly, Simple, Testing]: Does inprocessing when the CDCL hit decision level zero.
    • maintenanceRules[NULL, Inactivity, LBD, LBDInact, LBDInactLuby]: Performs clause database maintenances according to different maintenance schedules.
    • restartRules[NULL, InnerOuter, InnerOuterAgility, InnerOuterStag, Luby, LubyAgility, LubyStag]: Implements restarts according to different restart schedules.
    • selectVarRules[Random, VSIDS, RVSIDS, RRVSIDS]: Picks a decision variable.
    • selectDirRules[Random, FailBinary, PhaseSaving, PhaseFlip]: Selects an assignment for the given decision variable.
    • strLearnedRules[Null, Local, LocalRecursive, Antecedents, Reasons, AllOcc]: Tries to strengthen a learned clause that was provided by the conflictAnalysisRule. It might apply different types of strengthening.
    • strOtherRules[Null, WTwo]: Tries to strengthen other clauses given the (possibly strengthened) learned clause.
    • tools: Implements various tools like a decision stack for the CDCL.

Again, due to the modularity of the design we can easily add more plug-ins into modules or extend the implementations that a plug-in provides. The limit is basically the imagination of the researcher...

Given all these modules and plug-ins, one might wonder how these things are actually combined in order to work together. For plug-ins, the module containing them defines when they are called. For example in the SLS, the SLS module might want to perform a flip, so it just calls for a pre-defined interface method. This method is actually just a pointer that points to one of the available plug-in implementations of flipping. So whether SLS performs flipping as in WalkSAT or as in ProbSAT just depends on the initialization that makes the pointer point to one of the available implementations.

Modules reside within phases, and phases wire the modules together using strategies as explained in the next section.

Strategies

Assume you want to use several modules of the SEARCH phase. Exemplarily, assume that you first want to do SLS for a small number of flips, followed by MP-based CDCL. In Dimetheus, writing such a search strategy is easily done because of the modularity of the program. Each search strategy consists of four methods as follows.

  • Reset. Resets the search strategy and all the modules by calling their respective reset methods.
  • Initialize. Initializes the search strategy, all data structures and all modules it needs. This triggers calls to the initialize methods of the modules used.
  • Execute. Executes the search strategy. This triggers calls to the search modules of the search strategy. How and when these calls are performed and what to do with the result is depending on the strategy itself. Coding this is actually the real work. The search strategy basically defines what type of solver you have in the end.
  • Dispose. Disposes the search strategy and its data-structures. This includes calling the dispose functions of all modules that are used by this strategy.

Strategies are also available for CLASSIFY, ADAPT, PREPROCESS and INPROCESS.

All together, Dimetheus is a very flexible and easily extensible SAT solver that provides great robustness and decent performance. Those of you that do research in SAT might want to take a look at the source (see right hand side). If you are interested in more up-to-date versions drop me a mail and I can grant you access to the Subversion repository.

GNET BANNER
(C) 2019 Oliver Gableske
www.gableske.net
Valid CSS
Valid XHTML
Verified by Starfield
Copyright