Algorithm Engineering

Universität Tübingen

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

Events

Workshop on SAT 2011

Related Publications

Stephan Kottler and Michael Kaufmann: SArTagnan - A parallel portfolio SAT solver with lockless physical clause sharing, Pragmatics of SAT, to appear 2011
BibTex -- Abstract
Michael Kaufmann and Stephan Kottler: Beyond Unit Propagation in SAT Solving, Symposium on Experimental Algorithms 2011
BibTex -- Abstract
Michael Kaufmann and Stephan Kottler: A parallel portfolio SAT solver with lockless physical clause sharing, Technical Report, 2011
BibTex -- Abstract
Stephan Kottler: Description of the SApperloT, SArTagnan and MoUsSaka solvers for the SAT-Competition 2011, SAT 2011, USA
Stephan Kottler: SAT Solving with Reference Points, Theory and Applications of Satisfiability Testing - SAT 2010, 2010
BibTex -- Abstract
Stephan Kottler: Description of the SApperloT solver for the SAT-Race 2010, SAT 2010, Scotland
Stephan Kottler: Description of the parallel solver SArTagnan for the SAT-Race 2010, SAT 2010, Scotland
Michael Kaufmann, Stephan Kottler: Proving or Disproving Planar Straight-Line Embeddability onto given Rectangles, 17th International Symposium on Graph Drawing (GD '09), 2010
BibTex -- Abstract
Stephan Kottler: Description of the SApperloT solvers for the SAT-Competition 2009, SAT 2009, Wales
Stephan Kottler, Michael Kaufmann, Carsten Sinz: A New Bound for an NP-Hard Subclass of 3-SAT Using Backdoors, Theory and Applications of Satisfiability Testing - SAT 2008, 2008
BibTex -- Abstract
Stephan Kottler, Michael Kaufmann, Carsten Sinz: Computation of Renameable Horn Backdoors, Theory and Applications of Satisfiability Testing - SAT 2008, 2008
BibTex -- Abstract

Software

Source code of MoUsSaka as submitted to the SAT-competition 2011. It is an extension of SApperloT 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.
Source code of SApperloT for Linux as submitted to the SAT-competition 2011. Some information can be found in the solver description for the SAT-competition.
Source code of SArTagnan for Linux as submitted to the SAT-competition 2011. SArTagnan is a parallel 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. More information can be found in the Technical Report or in the solver description for the SAT Race 2010 and the SAT-competition 2011.
Source code of SApperloT for Linux as submitted to the SAT-Race 2010. This version combines DMRP with state-of-the-art CDCL solving. For more information please take a look at my paper about DMRP or the solver description for the SAT-Race. The preprocessor of this version of SApperloT was written by Christian Zielke.
The tool GridFit can be used to prove or disprove whether or not a plane graph can be embedded onto a given rectangle/grid. The embedding assumes edges to be drawn straight-line and without crossings. Internally GridFit encodes this problem into SAT and uses a modified version of SApperloT to solve the transformed problem. Source code for Linux of a preliminary version of GridFit is available for download. Just invoke 'make' in the top level directory and execute 'GridFit' to see the options. GridFit can be used for small graphs but it might get into trouble with larger graphs!
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. More information about SApperloT can be found here.
SatIn is a visualisation tool for SAT instances (Sat Insight) written in Java on top of the yFiles library. It allows for depicting different kinds of graphs that can be gained from SAT instances in conjunctive normal form. The layout of a graph can be chosen from a set of available automated layouts and, moreover, can be modiefied manually. Selecting an element in one graphical representation automatically highlights the according elements in all other graphical representations. Execute it with the command: java -jar SatIn.jar.

Affiliates

Support

Deutsche Forschungsgemeinschaft (DFG)
within Priority Programme 1307 "Algorithm Engineering"

--> Our website has moved permanently to https://uni-tuebingen.de/fakultaeten/mathematisch-naturwissenschaftliche-fakultaet/fachbereiche/informatik/lehrstuehle/algorithmik/home/!

Impressum Datenschutzerklärung

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

	Events Workshop on SAT 2011 Related Publications Stephan Kottler and Michael Kaufmann: SArTagnan - A parallel portfolio SAT solver with lockless physical clause sharing, Pragmatics of SAT, to appear 2011 BibTex -- Abstract Michael Kaufmann and Stephan Kottler: Beyond Unit Propagation in SAT Solving, Symposium on Experimental Algorithms 2011 BibTex -- Abstract Michael Kaufmann and Stephan Kottler: A parallel portfolio SAT solver with lockless physical clause sharing, Technical Report, 2011 BibTex -- Abstract Stephan Kottler: Description of the SApperloT, SArTagnan and MoUsSaka solvers for the SAT-Competition 2011, SAT 2011, USA Stephan Kottler: SAT Solving with Reference Points, Theory and Applications of Satisfiability Testing - SAT 2010, 2010 BibTex -- Abstract Stephan Kottler: Description of the SApperloT solver for the SAT-Race 2010, SAT 2010, Scotland Stephan Kottler: Description of the parallel solver SArTagnan for the SAT-Race 2010, SAT 2010, Scotland Michael Kaufmann, Stephan Kottler: Proving or Disproving Planar Straight-Line Embeddability onto given Rectangles, 17th International Symposium on Graph Drawing (GD '09), 2010 BibTex -- Abstract Stephan Kottler: Description of the SApperloT solvers for the SAT-Competition 2009, SAT 2009, Wales Stephan Kottler, Michael Kaufmann, Carsten Sinz: A New Bound for an NP-Hard Subclass of 3-SAT Using Backdoors, Theory and Applications of Satisfiability Testing - SAT 2008, 2008 BibTex -- Abstract Stephan Kottler, Michael Kaufmann, Carsten Sinz: Computation of Renameable Horn Backdoors, Theory and Applications of Satisfiability Testing - SAT 2008, 2008 BibTex -- Abstract Software Source code of MoUsSaka as submitted to the SAT-competition 2011. It is an extension of SApperloT 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. Source code of SApperloT for Linux as submitted to the SAT-competition 2011. Some information can be found in the solver description for the SAT-competition. Source code of SArTagnan for Linux as submitted to the SAT-competition 2011. SArTagnan is a parallel 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. More information can be found in the Technical Report or in the solver description for the SAT Race 2010 and the SAT-competition 2011. Source code of SApperloT for Linux as submitted to the SAT-Race 2010. This version combines DMRP with state-of-the-art CDCL solving. For more information please take a look at my paper about DMRP or the solver description for the SAT-Race. The preprocessor of this version of SApperloT was written by Christian Zielke. The tool GridFit can be used to prove or disprove whether or not a plane graph can be embedded onto a given rectangle/grid. The embedding assumes edges to be drawn straight-line and without crossings. Internally GridFit encodes this problem into SAT and uses a modified version of SApperloT to solve the transformed problem. Source code for Linux of a preliminary version of GridFit is available for download. Just invoke 'make' in the top level directory and execute 'GridFit' to see the options. GridFit can be used for small graphs but it might get into trouble with larger graphs! 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. More information about SApperloT can be found here. SatIn is a visualisation tool for SAT instances (Sat Insight) written in Java on top of the yFiles library. It allows for depicting different kinds of graphs that can be gained from SAT instances in conjunctive normal form. The layout of a graph can be chosen from a set of available automated layouts and, moreover, can be modiefied manually. Selecting an element in one graphical representation automatically highlights the according elements in all other graphical representations. Execute it with the command: java -jar SatIn.jar. If you have questions or any kind of feedback to the above software please don't hesitate to contact me! Affiliates Prof. Dr. Michael Kaufmann Prof. Dr. Wolfgang Küchlin Dr. Carsten Sinz Dr. Katharina A. Zweig Stephan Kottler Christian Zielke Support Deutsche Forschungsgemeinschaft (DFG) within Priority Programme 1307 "Algorithm Engineering" --> Our website has moved permanently to https://uni-tuebingen.de/fakultaeten/mathematisch-naturwissenschaftliche-fakultaet/fachbereiche/informatik/lehrstuehle/algorithmik/home/!
Impressum Datenschutzerklärung