Quantified Boolean Formula (QBF) solvers that utilize non-CNF representations are able to reason dually about conflicts and solutions by accessing structural information contained in the non-CNF representation. This structure is not as easily accessed from a CNF representation, hence CNF based solvers are not able to perform the same kind of reasoning. Recent work has shown how this additional structure can be extracted from a non-CNF representation and encoded in a form that can be fed directly to a CNF-based QBF solver without requiring major changes to the solver's architecture. This combines the benefits of specialized CNF-based techniques and dual reasoning. This approach, however, only works if one has access to a non-CNF representation of the problem, which is often not the case in practice. In this paper we address this problem and show how working only with the CNF encoding we can successfully extract partial structural information in a form that can be soundly given to a CNF-based solver. This yields performance benefits even though the information extracted is incomplete, and allows CNF-based solvers to obtain some of the benefits of dual reasoning in a more general context. To further increase the applicability of our approach we develop a new method for extracting structure from a CNF generated with the commonly used Plaisted-Greenbaum transformation. © 2013 Springer-Verlag.
CITATION STYLE
Goultiaeva, A., & Bacchus, F. (2013). Recovering and utilizing partial duality in QBF. In Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics) (Vol. 7962 LNCS, pp. 83–99). https://doi.org/10.1007/978-3-642-39071-5_8
Mendeley helps you to discover research relevant for your work.