Classical Planning as QBF without Grounding

Authors

  • Irfansha Shaik Aarhus University
  • Jaco van de Pol Aarhus University

DOI:

https://doi.org/10.1609/icaps.v32i1.19817

Keywords:

Classical Planning, Quantified Boolean Formula, QBF, Organic Synthesis, Grounding

Abstract

Most classical planners use grounding as a preprocessing step, essentially reducing planning to propositional logic. However, grounding involves instantiating all rules and actions 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.

Downloads

Published

2022-06-13

How to Cite

Shaik, I., & van de Pol, J. (2022). Classical Planning as QBF without Grounding. Proceedings of the International Conference on Automated Planning and Scheduling, 32(1), 329-337. https://doi.org/10.1609/icaps.v32i1.19817