Classical Planning as QBF without Grounding (extended version)

Most classical planners use grounding as a preprocessing step, reducing planning to propositional logic. However, grounding comes with a severe cost in memory, resulting in large encodings for SAT/QBF based planners. Despite the optimisations in SAT/QBF encodings such as action splitting, compact encodings and using parallel plans, the memory usage due to grounding remains a bottleneck when actions have many parameters, such as in the Organic Synthesis problems from the IPC 2018 planning competition (in its original non-split form). In this paper, we provide a compact QBF encoding that is logarithmic in the number of objects and avoids grounding completely by using universal quantification for object combinations. We compare the ungrounded QBF encoding with the simple SAT encoding and also show that we can solve some of the Organic Synthesis problems, which could not be handled before by any SAT/QBF based planners due to grounding.