Partially grounded planning as quantified boolean formula

Michael Cashmore, Maria Fox, Enrico Giunchiglia

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

12 Citations (Scopus)

Abstract

This paper describes a technique for translating bounded propositional reachability problems, such as Planning, into Quantified Boolean Formulae (QBF). The key feature of this translation is that the problem, and the resultant encoding is only partially grounded. The technique is applicable to other SAT or QBF encodings as an additional improvement, potentially reducing the size of the resulting formula by an exponential amount. We present experimental results showing that the approach applied to a simple SAT translation greatly improves the time taken to encode and solve problems in which there are many objects of a single type, even solving some problems that cannot be reasonably encoded as SAT.
Original languageEnglish
Title of host publicationICAPS 2013 - Proceedings of the 23rd International Conference on Automated Planning and Scheduling
Number of pages8
Publication statusPublished - 2013
EventTwenty-Third International Conference on International Conference on Automated Planning and Scheduling - ICAPS2013 - Rome, Italy
Duration: 10 Jun 201314 Jun 2013

Conference

ConferenceTwenty-Third International Conference on International Conference on Automated Planning and Scheduling - ICAPS2013
Abbreviated titleICAPS2013
CountryItaly
CityRome
Period10/06/1314/06/13

Keywords

  • quantified boolean formula
  • QBF
  • bounded propositional reachability problems

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

Cite this