Solving Dependency Quantified Boolean Formulas

求解依赖量化布尔公式

• 批准号: 278046454
• 负责人: Professor Dr. Bernd Becker
• 金额: --
• 依托单位: Institut für Informatik (IIF)
• 依托单位国家: 德国
• 项目类别: Research Grants
• 财政年份: 2015
• 资助国家: 德国
• 起止时间: 2014-12-31 至 2020-12-31
• 项目状态: 已结题
• 来源: https://gepris.dfg.de/gepris/projekt/278046454?language=en
• 关键词: Solving; Dependency; Quantified; Boolean; Formulas

Solvers for Boolean satisfiability problems (SAT) are nowadays applied in numerous domains of Computer Science and Electronic Design Automation with great success: To mention only a few, they are most relevant in (formal) verification and test of hard- and software, e. g., for bounded model checking (BMC) and automatic test pattern generation (ATPG), but also have been successfully used in the area ofartificial intelligence, e. g., for planning. In spite of the problem being NP-complete, modern solvers can handle formulas with hundred thousands of variables and millions of clauses. Therefore SAT solvers have gained high industrial relevance; most major chip manufacturers apply SAT-based techniques to find bugs in their hardware designs.Besides ongoing work to further increase the capabilities of SAT solvers, currently research is focused on solving an extension of the SAT problem, so-called quantified Boolean formulas (QBF). QBF is computationally even harder (PSPACE-complete); nevertheless, modern solvers have made enormous progress in solving practically relevant problems, and thereby opened a serious possibility to tackle many computationally hard problems.A number of problems, however, cannot be encoded naturally into QBFs, but require a generalization thereof. Examples are realizability of incomplete digital circuits, the analysis of non-cooperative games with incomplete information, certain bit-vector logics, and the synthesis of safe controllers. For a natural and compact formulation they require so-called Henkin-quantifiers, which leads to dependency quantified Boolean formulas (DQBF). DQBFs allow to express arbitrary dependencies of existential variables in the quantifier prefix, while QBF is restricted to linear dependencies.Currently the lack of efficient DQBF solvers severely limits its applicability to practical problems. In the proposed project we are planning to develop and enhance solving techniques for DQBF. One crucial task is to improve efficiency w. r. t. computation time and memory consumption. Another essential goal is to enable solvers to not only decide the satisfiability of a formula, but also to compute certificates for satisfiability in the form of so-called Skolem functions, which play an important role for many applications, e. g., as implementations of black boxes in incomplete designs or winning strategies in games. To prove the feasibility of the developed techniques we will apply them to problems instances coming from the different application areas.

布尔可满足性问题(SAT)的求解器目前在计算机科学和电子设计自动化的许多领域都得到了巨大的成功：仅举几个例子，它们在硬件和软件的(形式化)验证和测试中最相关，例如有界模型检测(BMC)和自动测试模式生成(ATPG)，但也已成功地用于人工智能领域，例如规划。尽管这个问题是NP完全的，但现代的求解器可以处理包含数十万个变量和数百万个子句的公式。因此，SAT解算器获得了很高的工业相关性；大多数主要芯片制造商都应用基于SAT的技术来发现其硬件设计中的错误。除了正在进行的进一步提高SAT解算器能力的工作外，目前的研究集中在解决SAT问题的一个扩展，即所谓的量化布尔公式(QBF)。QBF在计算上更加困难(PSPACE-Complete)；然而，现代求解器在解决实际相关问题方面取得了巨大的进步，从而为解决许多计算困难的问题提供了严重的可能性。然而，许多问题不能自然地编码成QBF，而需要对其进行推广。例如不完备数字电路的可实现性，不完全信息非合作博弈的分析，某些位向量逻辑，以及安全控制器的综合。对于自然和紧凑的公式，它们需要所谓的Henkin量词，这导致了依赖量化布尔公式(DQBF)。DQBF允许表达量词前缀中存在变量的任意依赖关系，而QBF仅限于线性依赖，目前缺乏有效的DQBF求解器严重限制了其在实际问题中的应用。在拟议的项目中，我们计划开发和增强DQBF的求解技术。一项重要的任务是提高效率、工作效率、计算时间和内存消耗。另一个基本目标是使求解器不仅能够确定公式的可满足性，而且能够以所谓的Skolem函数的形式计算可满足性证书，这些函数在许多应用中扮演着重要的角色，例如，作为不完全设计中的黑盒的实现或游戏中的获胜策略。为了证明所开发技术的可行性，我们将它们应用于来自不同应用领域的问题实例。