Parallel SAT-Solving

• Applicant: Professor Dr. Steffen Hölldobler
• Subject Area: Theoretical Computer Science ; Image and Language Processing, Computer Graphics and Visualisation, Human Computer Interaction, Ubiquitous and Wearable Computing ; Security and Dependability, Operating-, Communication- and Distributed Systems
• Term: from 2014 to 2020
• Project identifier: Deutsche Forschungsgemeinschaft (DFG) - Project number 259253065

The propositional satisfiability problem (SAT) is one of the problemsin the complexity class NP which has received much attention. In thelast 20 years SAT-solvers have become so powerful, that they areapplied in many domains (e.g. verification, scheduling, modelchecking). This increase in power is based on significant improvementsin the areas of formal systems, algorithms and data structures,strategies and heuristics, parameter optimization and, in particular,in the adaptation of the solvers to existing sequential architectures. New architectures, however, are parallel, have several cores, and areoften equipped with vector and SIMD units. To utilize modern andfuture computer architectures, sequential algorihms must beparallelized and adapted to the new architectures. The development of a parallel SAT-solver with acceptable parallelefficiency for a large set of SAT-instances which are selected fromdifferent applicatino domains is a major challenge and the main goal of thisproject. Todays parallel SAT-solver are mostly based on a portfolio approach,where several, differently configured, sequential solvers are solvingthe same SAT-instance. In most cases, a real parallelization of thesearch process is not taken place. On the other hand, partitioningapproaches split the search space, where iterative (in contrast toflat) partitioning approaches do not just solve the subproblems inparallel, but use an additional sequential solver in parallel to solvea given SAT-instance. Common characteristics of all parallelapproaches are that they run sequential solvers on the cores whoseimplementation and data structes have not been adapted to multi-corearchitectures, their performance on unsatisfiable SAT-instances iscomparatively poor, they do not parallelize simplification techniques and they are notsystematically evaluated. Moreover, the behavior of parallel solversis not adequately modelled by formal systems. Based on the hypothesis that iterative partitioning solvers willoutperform portfolio and flat partitioning solvers if the number ofcores is growing, this projects is aiming to achieve the followinggoals: development of a scalable parallel partitioning solver;development and integration of specialized methods to decideunsatisfiable SAT-instances faster and to generate correspondingproofs; better utilization of the available ressources by optimizingthe algorithms with respect to special properties of theunderlying architecture; development and integration of parallelsimplification techniques; development of a proof theory whichadequately models the behavior of the solver; configuration andevaluation of the solver. The new parallel solver shall replaceexisting sequential solvers in all typical applications.

• DFG Programme: Research Grants