SApperloT is a state-of-the-art SAT solver and comes in different versions.
The first version SApperloT-base was published in 2009 and implements
common techniques of conflict-driven SAT solvers with some
improvements and extensions.
It was submitted to the SAT Competition
2009 for the first time and has already
won the silver medal in the crafted category of satisfiable instances.
The second version in 2009 was SApperloT-hrp which enhances the base version to a new hybrid
three-phase approach that uses reference points for decision making.
Our motivation behind SApperloT-hrp is to develop a solver that utilises more
information during the solving process and we intend to extend the solver by
incorporating more structural information in the future.
In 2010 SApperloT was extended by a preprocessing unit by Christian Zielke
Moreover, DMRP became an inherent part
of the solver as it is published in the SAT 2010 paper
The SApperloT version 2011 uses a new technique for fast Unit Porpagation.
It also combines assymetric branching with hyper binary resolution to extensively simplify a SAT instance in between search.
SArTagnan is a multi-threaded portfolio SAT solver that runs different strategies in different threads.
Clauses can be shared logically and physically among all threads without the use of operation system locks.
In particular, one thread extensively applies simplification techniques and another thread uses DMRP.
Five threads apply the technique to extend Unit Propagation as described in the SEA paper 2011.
SArTagnan won the SAT-Race 2010 Award for the Best Student Solver in the parallel track.
MoUsSaka is an extension of the SApperloT 2011 version that
allows to find Minimal Unsatisfiable Subsets
(MUS) of a CNF formula.
It supports the plain MUS computation where the minimisation considers the number of clauses in the final unsatisfiable subset.
Furthermore, the computation can be set to minimise the number of categories or groups of clauses that appear in the unsatisfiable subset.
MoUsSaka became third in the plain MUS track
of the SAT Competition 2011.
At the main page all sources
of the mentioned solvers as well as the solver descriptions and
can be found.
If you have questions or any kind of feedback to the software please don't hesitate to contact Stephan