Parallel SAT
The propositional satisfiability problem (SAT) is one of the problems
in the complexity class NP which has received much attention. In the
last 20 years SAT-solvers have become so powerful, that they are
applied in many domains (e.g. verification, scheduling, model
checking). This increase in power is based on significant improvements
in 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 are
often equipped with vector and SIMD units. To utilize modern and
future computer architectures, sequential algorihms must be
parallelized and adapted to the new architectures.
The development of a parallel SAT-solver with acceptable parallel
efficiency for a large set of SAT-instances which are selected from
different applicatino domains is a major challenge and the main goal of this
project.
Todays parallel SAT-solver are mostly based on a portfolio approach,
where several, differently configured, sequential solvers are solving
the same SAT-instance. In most cases, a real parallelization of the
search process is not taken place. On the other hand, partitioning
approaches split the search space, where iterative (in contrast to
flat) partitioning approaches do not just solve the subproblems in
parallel, but use an additional sequential solver in parallel to solve
a given SAT-instance. Common characteristics of all parallel
approaches are that they run sequential solvers on the cores whose
implementation and data structes have not been adapted to multi-core
architectures, their performance on unsatisfiable SAT-instances is
comparatively poor, they do not parallelize simplification techniques and they are not
systematically evaluated. Moreover, the behavior of parallel solvers
is not adequately modelled by formal systems.
Based on the hypothesis that iterative partitioning solvers will
outperform portfolio and flat partitioning solvers if the number of
cores is growing, this projects is aiming to achieve the following
goals: development of a scalable parallel partitioning solver;
development and integration of specialized methods to decide
unsatisfiable SAT-instances faster and to generate corresponding
proofs; better utilization of the available ressources by optimizing
the algorithms with respect to special properties of the
underlying architecture; development and integration of parallel
simplification techniques; development of a proof theory which
adequately models the behavior of the solver; configuration and
evaluation of the solver. The new parallel solver shall replace
existing sequential solvers in all typical applications.