Solving Dependency Quantified Boolean Formulas

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

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.