QUBE: A System for Deciding Quantified Boolean Formulas Satisfiability
QUBE: A System for Deciding Quantified Boolean Formulas Satisfiability
复制标题
DOI：
10.1007/3-540-45744-5_27
复制
发表时间：
2001-06
期刊：
影响因子：
--
通讯作者：
E. Giunchiglia;Massimo Narizzano;A. Tacchella
中科院分区：
文献类型：
--
作者：
E. Giunchiglia;Massimo Narizzano;A. Tacchella
确定量化布尔公式的可满足性是人工智能领域的一个重要研究课题。许多推理任务，包括规划b[1]、溯因、知识推理b[1]、非单调推理b[2]，都可以直接映射到确定QBF的可满足性问题。本文提出了一种判定QBFs可满足性的系统——QuBE。我们从第2节开始介绍本文其余部分所必需的一些术语和定义。在§3中，我们给出了QuBE基本算法的高层次描述。QuBE的可用选项在§4中有描述。在第5节的最后，我们给出了一些实验结果，证明了QuBE与其他系统的有效性。QuBE以及有关QuBE的更多信息，请访问www.mrg.dist.unige.it/star/qube。
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 in § 2 with some terminology and definitions necessary for the rest of the paper. In § 3 we present a high level description of QuBE’s basic algorithm. QuBE’s available options are described in § 4. We end our presentation in § 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.