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 | ICAPS 2013 - Proceedings of the 23rd International Conference on Automated Planning and Scheduling |
Number of pages | 8 |
Publication status | Published - 2013 |
Event | Twenty-Third International Conference on International Conference on Automated Planning and Scheduling - ICAPS2013 - Rome, Italy Duration: 10 Jun 2013 → 14 Jun 2013 |
Conference
Conference | Twenty-Third International Conference on International Conference on Automated Planning and Scheduling - ICAPS2013 |
---|---|
Abbreviated title | ICAPS2013 |
Country/Territory | Italy |
City | Rome |
Period | 10/06/13 → 14/06/13 |
Keywords
- quantified boolean formula
- QBF
- bounded propositional reachability problems