Classical Planning as QBF without Grounding (extended version)
This addresses a critical scalability issue for planners in domains with many action parameters, such as organic synthesis, though it is an incremental improvement over existing QBF methods.
The paper tackles the memory bottleneck in classical planning caused by grounding, which instantiates all action rules with concrete objects, by introducing a compact QBF encoding that avoids grounding using universal quantification. The result is that it can solve Organic Synthesis problems from IPC 2018 that were previously unsolvable by SAT/QBF-based planners.
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.