Universität Tübingen Fakultät > Wilhelm-Schickard-Institut > Algorithmik > Lehrstuhl > Mitarbeiter > Stephan Kottler
Arbeitsbereich Algorithmik

Dr. Stephan Kottler

Stephan Kottler

Contact Information

Email: stephan.kottleratuni-tuebingen.de
... is forwarded to my current address.

Teaching | Publications | Software | Prices | Talks | Education

Research Interests




Scientific Service


  • The Java tool CoPAn (Conflict Pattern Analysis) allows the user for an in-depth analysis of conflicts and the associated process of producing learnt clauses. The main attention is drawn to the analysis and comparison of patterns within the resolution operation for different conflicts. Recurring patterns of resolution can be related to several properties of conflicts - configurable by the user.
  • 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!

Awards and Prices

Some Talks


Anregungen / Kritik Impressum minicms