In this paper we approach the problem of reason- ing with quantified Boolean formulas (QBFs) by combining search and resolution, and by switch- ing between them according to structural proper- ties of QBFs. We provide empirical evidence that QBFs which cannot be solved by search or resolu- tion alone, can be solved by combining them, and that our approach makes a proof-of-concept imple- mentation competitive with current QBF solvers.
A Structural Approach to Reasoning with Quantified Boolean Formulas
PULINA, LUCA;TACCHELLA, ARMANDO
2009-01-01
Abstract
In this paper we approach the problem of reason- ing with quantified Boolean formulas (QBFs) by combining search and resolution, and by switch- ing between them according to structural proper- ties of QBFs. We provide empirical evidence that QBFs which cannot be solved by search or resolu- tion alone, can be solved by combining them, and that our approach makes a proof-of-concept imple- mentation competitive with current QBF solvers.
File in questo prodotto:
Non ci sono file associati a questo prodotto.
I documenti in IRIS sono protetti da copyright e tutti i diritti sono riservati, salvo diversa indicazione.
