# Classical Planning as QBF without Grounding (extended version)

arXiv: https://arxiv.org/abs/2106.10138 · HTML: https://mlsanity.com/paper/2106.10138/

## Key facts

- Cited by 5 papers in the map (data through 14 Oct 2026).
- Builds on 0 of its 32 references that are in the map.
- First posted on arXiv 18 Jun 2021.

## Built on by (most cited first, 5 of 5)

- [Optimal Layout Synthesis for Quantum Circuits as Classical Planning (full version)](https://mlsanity.com/paper/2304.12014/) (2023)
- [MinePlanner: A Benchmark for Long-Horizon Planning in Large Minecraft Worlds](https://mlsanity.com/paper/2312.12891/) (2023)
- [Optimal Layout-Aware CNOT Circuit Synthesis with Qubit Permutation](https://mlsanity.com/paper/2408.04349/) (2024)
- [Implicit State and Goals in QBF Encodings for Positional Games (extended version)](https://mlsanity.com/paper/2301.07345/) (2023)
- [Concise QBF Encodings for Games on a Grid (extended version)](https://mlsanity.com/paper/2303.16949/) (2023)

## Abstract (arXiv)

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.