Clausal Abstraction for DQBF (full version)

TL;DR

This paper extends the clausal abstraction algorithm from QBF to DQBF, enabling more effective solving of complex verification problems involving Boolean functions and partial dependencies.

Contribution

It introduces a generalized clausal abstraction algorithm for DQBF, addressing challenges with incomparable dependencies and spurious existential variable dependencies.

Findings

dCAQE solves significantly more DQBF formulas than previous algorithms.

The approach effectively handles partial orders of abstractions.

The method improves the efficiency of DQBF solving in verification tasks.

Abstract

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.