Classical Planning as QBF without Grounding (extended version)

TL;DR

This paper introduces a compact QBF encoding for classical planning that avoids grounding by using universal quantification, enabling the solution of complex problems previously infeasible due to large encodings.

Contribution

The authors present a novel QBF encoding method that eliminates grounding, reducing memory usage and enabling the solving of large-scale planning problems.

Findings

Successfully solved Organic Synthesis problems previously unsolvable by SAT/QBF planners

Encoding size is logarithmic in the number of objects, improving scalability

Demonstrated effectiveness on IPC 2018 Organic Synthesis benchmarks

Abstract

Most classical planners use grounding as a preprocessing step, essentially reducing planning to propositional logic. However, grounding involves instantiating all action rules with concrete object combinations, and results in large encodings for SAT/QBF-based planners. This severe cost in memory becomes a main bottleneck when actions have many parameters, such as in the Organic Synthesis problems from the IPC 2018 competition. 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 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.