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
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
- 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
- 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
- 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
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
- 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,
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
- 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.
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.