Deciding the satisfiability of a Quantified Boolean Formula (QBF) is an important research issue in Artificial Intelligence. Many reasoning tasks involving planning [1], abduction, reasoning about knowledge, non monotonic reasoning [2], can be directly mapped into the problem of deciding the satisfiability of a QBF. In this paper we present quBE, a system for deciding QBFs satisfiability. We start our presentation is Section 2 with some terminology and definitions necessary for the rest of the paper. In Section 3 we present a high level description of QuBE's basic algorithm. QuBE's available options are described in Section 4. We end our presentation is Section 5 with some experimental results showing QuBE effectiveness in comparison with other systems. QuBE, and more information about QuBE are available at www.mrg.dist.unige.it/star/qube
QUBE: A System for Deciding Quantified Boolean Formulas Satisfiability.
GIUNCHIGLIA, ENRICO;NARIZZANO, MASSIMO;TACCHELLA, ARMANDO
2001-01-01
Abstract
Deciding the satisfiability of a Quantified Boolean Formula (QBF) is an important research issue in Artificial Intelligence. Many reasoning tasks involving planning [1], abduction, reasoning about knowledge, non monotonic reasoning [2], can be directly mapped into the problem of deciding the satisfiability of a QBF. In this paper we present quBE, a system for deciding QBFs satisfiability. We start our presentation is Section 2 with some terminology and definitions necessary for the rest of the paper. In Section 3 we present a high level description of QuBE's basic algorithm. QuBE's available options are described in Section 4. We end our presentation is Section 5 with some experimental results showing QuBE effectiveness in comparison with other systems. QuBE, and more information about QuBE are available at www.mrg.dist.unige.it/star/qube
I documenti in IRIS sono protetti da copyright e tutti i diritti sono riservati, salvo diversa indicazione.
