QUBE A system for deciding quantified boolean formulas satisfiability.pdf

下载文档

3
0
约1.44万字
约 5页
2017-04-09 发布于江苏
举报
版权申诉
保障服务

QUBE A system for deciding quantified boolean formulas satisfiability.pdf

1、本文档共5页，可阅读全部内容。
2、有哪些信誉好的足球投注网站（book118）网站文档一经付费（服务费），不意味着购买了该文档的版权，仅供个人/单位学习、研究之用，不得用于商业用途，未经授权，严禁复制、发行、汇编、翻译或者网络传播等，侵权必究。
3、本站所有内容均由合作方或网友上传，本站不对文档的完整性、权威性及其观点立场正确性做任何保证或承诺！文档内容仅供研究参考，付费前请自行鉴别。如您付费，意味着您自己接受本站规则且自行承担风险，本站不退款、不进行额外附加服务；查看《如何避免下载的几个坑》。如果您已付费下载过本站文档，您可以点击这里二次下载。
4、如文档侵犯商业秘密、侵犯著作权、侵犯人身权等，请点击“版权申诉”（推荐），也可以打举报电话：400-050-0827(电话支持时间：9:00-18:30)。

QUBE A system for deciding quantified boolean formulas satisfiability

QUBE: A system for deciding Quantified Boolean Formulas Satisfiability ? Enrico Giunchiglia, Massimo Narizzano, and Armando Tacchella DIST, Universita? di Genova, Viale Causa 13, 16145 Genova – Italy 1 Introduction Deciding the satisfiability of a Quantified Boolean Formula (QBF) is an important re- search 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 x 2 with some terminology and definitions necessary for the rest of the paper. In x 3 we present a high level description of QUBE’s basic algorithm. QUBE’s available options are described in x 4. We end our presentation in x 5 with some experimental results showing QUBE effectiveness in comparison with other sys- tems. QUBE, and more information about QUBE, are available at www.mrg.dist. unige.it/star/qube. 2 Formal preliminaries Consider a set P of propositional letters. An atom is an element of P. A literal is an atom or the negation of an atom. For each literal l, (i) l is x if l = :x, and is :x if l = x; (ii)jlj is the atom occurring in l. A clause C is an n-ary (n 0) disjunction of literals such that no atom occurs twice in C. A propositional formula is a k-ary (k 0) conjunction of clauses. As customary, we represent a clause as a set of literals, and a propositional formula as a set of clauses. A QBF is an expression of the formQ1x1 : : : Qnxn; (n 0) (1) where everyQi (1 i n) is a quantifier, either existential 9 or universal 8; x1; : : : ; xn are pairwise distinct atoms in P; and is a propositional formula in the atoms x1; : : : ; xn.Q1x1 : : : Qnxn is the prefix and is the (quantifier-free) matrix of (1). Consider a QBF of the form (1). A literal l occurring in is: – existential if 9jlj belongs to the prefix of (1),