Dependency Schemes for DQBF
Dependency schemes allow to identify variable independencies in QBFs or DQBFs. For QBF, several dependency schemes have been proposed, which differ in the number of independencies they are able to identify. In this paper, we analyze the spectrum of depend
- PDF / 633,390 Bytes
- 17 Pages / 439.37 x 666.142 pts Page_size
- 58 Downloads / 214 Views
Albert-Ludwigs-Universit¨ at Freiburg im Breisgau, Freiburg im Breisgau, Germany {wimmer,scholl,wimmerka,becker}@informatik.uni-freiburg.de 2 Dependable Systems and Software, Saarland University, Saarbr¨ ucken, Germany
Abstract. Dependency schemes allow to identify variable independencies in QBFs or DQBFs. For QBF, several dependency schemes have been proposed, which differ in the number of independencies they are able to identify. In this paper, we analyze the spectrum of dependency schemes that were proposed for QBF. It turns out that only some of them are sound for DQBF. For the sound ones, we provide a correctness proof, for the others counter examples. Experiments show that a significant number of dependencies can either be added to or removed from a formula without changing its truth value, but with significantly increasing the flexibility for modifying the representation.
1
Introduction
During the last two decades an enormous progress in the solution of quantifierfree Boolean formulas (SAT) has been observed. Nowadays, SAT solving is successfully used in many application areas, e.g., in formal verification of hard- and software systems [1,5,10], automatic test pattern generation [11,12], or planning [22]. Motivated by the success of SAT solvers, more general formalisms like quantified Boolean formulas (QBFs) have been studied. However, for applications like the verification of partial circuits [17,24], the synthesis of safe controllers [6], and the analysis of games with incomplete information [21], even QBF is not expressive enough to provide a compact and natural formulation. The reason is that the dependencies of existential variables on universal ones are restricted in QBF: Each existential variable implicitly depends on all universal variables in whose scope it is, i.e., in a model for a QBF in prenex normal form the value of an existential variable can be chosen depending on the values of the universal variables to the left. Consequently, the dependency sets of the existential variables (i.e., the sets of universal variables they may depend on) are linearly ordered w.r.t. set inclusion in QBF. In so-called dependency quantified Boolean formulas (DQBFs) this restriction is removed and for each existential variable a dependency set is explicitly specified. The more general DQBF formulations can be tremendously more compact than equivalent QBF formulations; on the other hand the decision problem is NEXPTIME-complete for DQBF [21] instead of This work was partly supported by the German Research Council (DFG) as part of the project “Solving Dependency Quantified Boolean Formulas”. c Springer International Publishing Switzerland 2016 N. Creignou and D. Le Berre (Eds.): SAT 2016, LNCS 9710, pp. 473–489, 2016. DOI: 10.1007/978-3-319-40970-2 29
474
R. Wimmer et al.
PSPACE-complete for QBF. Driven by the needs of the applications mentioned above, research on DQBF solving has started during the last few years, leading to first solvers like iDQ and HQS [14,15,18,28]. Although the dependency sets of existential varia
Data Loading...
