SApperloT SAT Solvers

SApperloT is a state-of-the-art SAT solver and comes in two different versions. The first version SApperloT-base 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 is 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.

Downloads

• A short overview over the two solver versions can be found here or in the booklet published at www.satcompetition.org.
• Source code of SApperloT-base for Linux as submitted to the SAT-competition 2009. Note that this version is a bit more verbose than the submitted one.

If you have any questions or hints or whatever please feel free to contact me. If you are interested in the visualisation of SAT Instances you may use the tool SatIn. It was used to create the Literal-Clause graph on the left side and can be downloaded from my page.