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 have implemented and analysed several different approaches for sequential and mult-threaded SAT solving. The different solver implementations are presented here.
