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.
