AAAI Publications, Twenty-First International Joint Conference on Artificial Intelligence

Font Size: 
A Structural Approach to Reasoning with Quantified Boolean Formulas
Luca Pulina, Armando Tacchella

Last modified: 2009-06-25


In this paper we approach the problem of reasoning with quantified Boolean formulas (QBFs) by combining search and resolution, and by switching between them according to structural properties of QBFs. We provide empirical evidence that QBFs which cannot be solved by search or resolution alone, can be solved by combining them, and that our approach makes a proof-of-concept implementation competitive with current QBF solvers.


Satisfiability;Automated Reasoning and Theorem Proving

Full Text: PDF