Abstract
An open quantified boolean formula (QBF) is a QBF that contains free (unquantified) variables. A solution to such a QBF is a quantifier-free formula that is logically equivalent to the given QBF. Although most recent QBF research has focused on closed QBF, there are a number of interesting applications that require one to consider formulas with free variables. This article shows how clause/cube learning for DPLL-based closed-QBF solvers can be extended to solve QBFs with free variables. We do this by introducing sequents that generalize clauses and cubes and allow learning facts of the form "under a certain class of assignments, the input formula is logically equivalent to a certain quantifier-free formula". © 2013 Springer-Verlag.
Cite
CITATION STYLE
Klieber, W., Janota, M., Marques-Silva, J., & Clarke, E. (2013). Solving QBF with free variables. In Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics) (Vol. 8124 LNCS, pp. 415–431). https://doi.org/10.1007/978-3-642-40627-0_33
Register to see more suggestions
Mendeley helps you to discover research relevant for your work.
