Universität Tübingen Fakultät > Wilhelm-Schickard-Institut > Paralleles Rechnen > Forschung > Algorithm Engineering
Arbeitsbereich Paralleles Rechnen

DFG-Schwerpunktprogramm 1307 Algorithm Engineering Structure Based Algorithm Engineering
for SAT-Solving


Given a boolean formula the satisfiability problem (SAT) asks if there exists a truth assignment to the variables of the formula such that the formula evaluates to true. Even though this problem seems to be purely theoretical there are several real-world problems that can be formulated as a SAT problem. From the theoretical point of view SAT is NP-complete and should thus be not solvable in feasible time. However, in the last 15 years state-of-the-art SAT Solvers became able to solve many real-world SAT instances with hundreds and thousands of variables. This is reasond by the fact that real-world SAT problems exhibit some internal structure that can be somehow exploited by SAT Solvers.

In the last years we have worked out a general methological approach that can be used to analyze the structure of real-world problems. One of our goals is to apply this methodology for solving SAT problems. We aim to develop and implement a SAT Solver that analyzes the structure of the underlying SAT instance and uses these information for the solving process. One big challange is to handle the trade-off between the quality of structural information and on the other hand the complexity to compute these information in the first phase of the algorithm. We submitted two solvers for the SAT Competition 2009. The first solver performed very well for industrial and crafted instances and it even managed to become second in the category of crafted satisfiable instances. The second solver implements our new hybrid approach and could already show some promising results.

Related Publications

Software

  • Source code (c++) of our solver SApperloT-base for Linux can be downloaded from 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.
  • 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!
    • If you have questions or any kind of feedback to the above software please don't hesitate to contact me!

Affiliates

Support
Anregungen / Kritik Impressum minicms