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 language | English |
|---|---|
| Title of host publication | Proceedings of the twenty-third international conference on automated planning and scheduling (ICAPS 2013) |
| Editors | Daniel Borrajo, Subbarao Kambhampati, Angelo Oddi, Simone Fratini |
| Publisher | AAAI Press |
| Pages | 29-36 |
| Number of pages | 7 |
| ISBN (Print) | 9781577356097 |
| Publication status | Published - Aug 2012 |