Structure Based Algorithm Engineering for SAT Solving

Description

Prof. Dr. Michael Kaufmann, Prof. Dr. sc. techn. Wolfgang Küchlin; Universität Tübingen

 

Project website

 

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 like hardware and software verification, planning, automotive product configuration and problems in bioinformatics.

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 tackle many real-world SAT instances with hundreds and thousands of variables.

We aim to improve SAT solving by analysing and enhancing current solving techniques. Our main goal is to allow for more structural analysis of instances during the solving process. Moreover, we implement and evaluate hybrid and parallel solving techniques to combine different successful approaches to one robust solver.

This work requires extensive evaluation and verification of the solver on huge sets of benchmarks. In the international SAT-competition 2009 our solver was able to win the silver medal in the category of satisfiable crafted instances.

  
  

Publications

  • S. Kottler and M. Kaufmann. "SArTagnan - A parallel portfolio SAT solver with lockless physical clause sharing". Pragmatics of SAT. 2011. [More] 
  • M. Kaufmann and S. Kottler. "Beyond Unit Propagation in SAT Solving". Symposium on Experimental Algorithms. 2011. [More] 
  • S. Kottler. "SAT Solving with Reference Points". Theory and Applications of Satisfiability Testing. 2010. [More] 
  • M. Kaufmann and S. Kottler. "Proving or Disproving Planar Straight-Line Embeddability onto given Rectangles". 17th International Symposium on Graph Drawing. 2010. [More] 
  • S. Kottler, M. Kaufmann and C. Sinz. "Computation of Renameable Horn Backdoors". Theory and Applications of Satisfiability Testing. 2008. [More] 
View All
  

Projects

[ Back ]