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.