Planning as quantified boolean formula

Cashmore, Michael and Fox, Maria and Giunchiglia, Enrico; (2012) Planning as quantified boolean formula. In: Proceedings of the 20th European Conference on Artificial Intelligence (ECAI) 2012. IOS Press, FRA, pp. 217-222. ISBN 9781614990970 (https://doi.org/10.3233/978-1-61499-098-7-217)

[thumbnail of Cashmore-etal-ECAI2012-Planning-quantified-boolean-formula]
Preview
 Text. Filename: Cashmore_etal_ECAI2012_Planning_quantified_boolean_formula.pdf
Final Published Version
License: Creative Commons Attribution-NonCommercial 4.0 logo
Download (296kB)| Preview

Abstract

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.

CORE (COnnecting REpositories)