Synthesis of Boolean Functions with Clausal Abstraction

Abstract

Dependency quantified Boolean formulas (DQBF) is a logic admitting existential quantification over Boolean functions, which allows us to elegantly state synthesis problems in planning and verification. 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 quantifiers. 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 (partial) Skolem functions during the execution. Our prototype implementation shows improved performance compared to previous algorithms.