Partially Grounded Planning as Quantified Boolean Formula

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.