Fakultät > Wilhelm-Schickard-Institut > Algorithmik > Forschung > Algorithm Engineering > SApperloT SArTagnan MoUsSaka

Boolean formula in cnf written in DIMACS format

SApperloT

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

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

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.

Downloads

At the main page all sources of the mentioned solvers as well as the solver descriptions and related publications can be found. If you have questions or any kind of feedback to the software please don't hesitate to contact Stephan!

Anregungen / Kritik Impressum

Universität Tübingen	Fakultät > Wilhelm-Schickard-Institut > Algorithmik > Forschung > Algorithm Engineering > SApperloT SArTagnan MoUsSaka

Startseite Lehrstuhl Mitarbeiter Studentische Mitarbeiter Ehemalige Mitarbeiter Forschung Smog - Slog Graphenzeichnen BPMN Layouter Graph Archive EuroGIGA - GraDR Netzwerkanalyse BiNA Algorithm Engineering SApperloT SArTagnan MoUsSaka CoPAn: Conflict Pattern Analysis MUStICCa: MUS Extraction with Interactive Choice of Candidates Abgeschlossene Arbeiten Lehre Aktuelles Semester Studien- und Diplomarbeiten Vergangene Semester Intern	SApperloT 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 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 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. Downloads At the main page all sources of the mentioned solvers as well as the solver descriptions and related publications can be found. If you have questions or any kind of feedback to the software please don't hesitate to contact Stephan!
Anregungen / Kritik Impressum