2018/08/27 by Leander Tentrup, Markus N. Rabe, Tentrup, Leander +1
Computer Science · #FOS: Computer and information sciences #Formal Methods in Verification #Logic in Computer Science (cs.LO) #Logic, programming, and type systems #Software Testing and Debugging Techniques
paper · pdf · doi:10.48550/arxiv.1808.08759
openalex publication_date 2018/08/27 · openalex created_date 2025/10/10 · openalex updated_date 2026/07/28
Dependency quantified Boolean formulas (DQBF) is a logic admitting existential quantification over Boolean functions, which allows us to elegantly state synthesis problems in verification such as the search for invariants, programs, or winning regions of games. In this paper, we lift the clausal abstraction algorithm for quantified Boolean formulas (QBF) to DQBF. Clausal abstraction for QBF is an abstraction refinement algorithm that operates on a sequence of abstractions that represent the different quantifier levels. For DQBF we need to generalize this principle to partial orders of abstractions. The two challenges to overcome are: (1) Clauses may contain literals with incomparable dependencies, which we address by the recently proposed proof rule called Fork Extension, and (2) existential variables may have spurious dependencies, which we prevent by tracking consistency requirements during the execution. Our implementation dCAQE solves significantly more formulas than the existing DQBF algorithms.