Parallel SAT-Solving

命题可满足性问题（SAT）是复杂度类NP中备受关注的问题之一。在过去的20年里，sat求解器已经变得如此强大，以至于它们被应用于许多领域（例如验证、调度、模型检查）。这种能力的提高是基于形式系统、算法和数据结构、策略和启发式、参数优化等领域的重大改进，特别是在求解器对现有顺序架构的适应方面。然而，新的架构是并行的，有几个核心，并且通常配备矢量和SIMD单元。为了利用现代和未来的计算机体系结构，顺序算法必须并行化并适应新的体系结构。为从不同应用领域中选择的大量sat实例开发具有可接受并行效率的并行sat求解器是本项目的主要挑战和主要目标。今天的并行sat求解器主要基于组合方法，其中几个不同配置的顺序求解器解决同一个sat实例。在大多数情况下，没有发生真正的并行化搜索过程。另一方面，划分方法分割了搜索空间，迭代（与平坦划分方法相反）划分方法不仅并行地解决子问题，而且并行地使用额外的顺序求解器来求解给定的sat实例。所有并行方法的共同特点是，它们在实现和数据结构尚未适应多核架构的核心上运行顺序求解器，它们在不令人满意的sat实例上的性能相对较差，它们不并行化简化技术，并且它们没有被系统地评估。此外，并行解的行为没有被正式系统充分地模拟。基于迭代分区求解器在内核数量增加时优于组合和平面分区求解器的假设，该项目旨在实现以下目标：开发可扩展的并行分区求解器；开发和集成专门的方法来更快地确定不满意的sat实例并生成相应的证明；通过针对底层架构的特殊属性优化算法，更好地利用可用资源；并行化简技术的发展与集成；发展证明理论，充分模拟求解器的行为；解算器的配置和贬值。新的并行求解器将在所有典型应用中取代现有的顺序求解器。

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.