Parallel SAT-Solving

并行 SAT 求解

• 批准号: 259253065
• 负责人: Professor Dr. Steffen Hölldobler
• 金额: --
• 依托单位: Professur für Wissensverarbeitung
• 依托单位国家: 德国
• 项目类别: Research Grants
• 财政年份: 2014
• 资助国家: 德国
• 起止时间: 2013-12-31 至 2019-12-31
• 项目状态: 已结题
• 来源: https://gepris.dfg.de/gepris/projekt/259253065?language=en
• 关键词: Parallel; SAT; Solving

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.

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