Proceedings

A Uniform Approach for Generating Proofs and Strategies for Both True and False QBF Formulas

Alexandra Goultiaeva, Allen Van Gelder, Fahiem Bacchus

Download BibTeX Cite

Proceedings of the Twenty-Second International Joint Conference on Artificial Intelligence. Pages 546-552.

https://doi.org/10.5591/978-1-57735-516-8/IJCAI11-099

Abstract

Many important problems can be compactly represented as quantified boolean formulas (QBF) and solved by general QBF solvers. To date QBF solvers have mainly focused on determining whether or not the input QBF is true or false. However, additional important information about an application can be gathered from its QBF formulation. In this paper we demonstrate that a circuit-based QBF solver can be exploited to obtain a Q-Resolution proof of the truth or the falsity of a QBF. QBFs have a natural interpretation as a two person game and our main result is to show how, via a simple computation, the moves for the winning player can be computed directly from these proofs. This result shows that the proof is a representation of the winning strategy. In previous approaches the winning strategy has often been represented in a way that makes it hard to verify. In our approach the correctness of the strategy follows directly from the correctness of the proof, which is relatively easy to verify.

Alexandra Goultiaeva, Allen Van Gelder, and Fahiem Bacchus. 2011. A Uniform Approach for Generating Proofs and Strategies for Both True and False QBF Formulas. In Proceedings of the Twenty-Second International Joint Conference on Artificial Intelligence, IJCAI-11. IJCAI, 546–552. https://doi.org/10.5591/978-1-57735-516-8/IJCAI11-099
Welcome Future Conferences AI Journal Division IJCAI Proceedings About IJCAI IJCAI Awards