Planning as Quantified Boolean Formula
Planning as Quantified Boolean Formula
复制标题
作为量化布尔公式进行规划
DOI：
10.3233/978-1-61499-098-7-217
复制
发表时间：
2012
期刊：
影响因子：
--
通讯作者：
E. Giunchiglia
中科院分区：
文献类型：
--
作者：
Michael Cashmore;M. Fox;E. Giunchiglia
本文介绍了两种将有界命题可达性问题转化为量化布尔公式（QBF）的技术。两者都利用 QBF 问题的二叉树结构来生成实例大小对数的编码，因此比具有相同边界的相应 SAT 编码小。第一个编码基于 Rintanen 的迭代平方公式。第二种编码是紧凑树编码，比第一种编码更有效，需要更少的量词和变量的交替。我们提供的实验结果表明，该方法是可行的，尽管尚未与当前最先进的基于 SAT 的求解器竞争。
This paper introduces two techniques for translating bounded propositional reachability problems into Quantified Boolean Formulae (QBF). Both exploit the binary-tree structure of the QBF problem to produce encodings logarithmic in the size of the instance and thus exponentially smaller than the corresponding SAT encoding with the same bound. The first encoding is based on the iterative squaring formulation of Rintanen. The second encoding is a compact tree encoding that is more efficient than the first one, requiring fewer alternations of quantifiers and fewer variables. We present experimental results showing that the approach is feasible, although not yet competitive with current state of the art SAT-based solvers.