Download PDFOpen PDF in browser

iDQ: Instantiation-Based DQBF Solving

14 pagesPublished: July 28, 2014

Abstract

Dependency Quantified Boolean Formulas (DQBF) are obtained by adding Henkin quantifiers to Boolean formulas and have seen growing interest in the last years. Since deciding DQBF is NEXPTIME-complete, efficient ways of solving it would have many practical applications. Still, there is only few work on solving this kind of formulas in practice. In this paper, we present an instantiation-based technique to solve DQBF efficiently. Apart from providing a theoretical foundation, we also propose a concrete implementation of our algorithm. Finally, we give a detailed experimental analysis evaluating our prototype iDQ on several DQBF as well as QBF benchmarks.

Keyphrases: dqbf, qbf, sat, epr, instantiation, dqdimacs

In: Daniel Le Berre (editor). POS-14. Fifth Pragmatics of SAT workshop. EPiC Series in Computing, vol 27, pages 103-116

Download PDFOpen PDF in browser