Planning as quantified boolean formula

Michael Cashmore, Maria Fox, Enrico Giunchiglia

Research output: Chapter in Book/Report/Conference proceedingConference contribution book

8 Citations (Scopus)
4 Downloads (Pure)

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.
Original languageEnglish
Title of host publicationProceedings of the 20th European Conference on Artificial Intelligence (ECAI) 2012
Place of PublicationAmsterdam
PublisherIOS Press
Pages217-222
Number of pages6
Volume242
ISBN (Print)9781614990970
DOIs
Publication statusPublished - 31 Aug 2012
Event20th European Conference on Artificial Intelligence - ECAI 2012 - Montpellier, France
Duration: 27 Aug 201231 Aug 2012

Conference

Conference20th European Conference on Artificial Intelligence - ECAI 2012
Abbreviated titleECAI 2012
CountryFrance
CityMontpellier
Period27/08/1231/08/12

Keywords

  • planning
  • quantified boolean formula

Fingerprint Dive into the research topics of 'Planning as quantified boolean formula'. Together they form a unique fingerprint.

  • Cite this

    Cashmore, M., Fox, M., & Giunchiglia, E. (2012). Planning as quantified boolean formula. In Proceedings of the 20th European Conference on Artificial Intelligence (ECAI) 2012 (Vol. 242, pp. 217-222). IOS Press. https://doi.org/10.3233/978-1-61499-098-7-217