Home Lifted Classical Planning via Propositional Logic Satisfiability
Post
Cancel

Lifted Classical Planning via Propositional Logic Satisfiability

Planning models are usually defined in lifted, i.e., first order formalisms, while most solvers need (variable-free) grounded representations. Though techniques for grounding prune unnecessary parts of the model, grounding might – nevertheless – be prohibitively expensive in terms of runtime. To overcome this issue, there has been renewed interest in solving planning problems based on the lifted representation in the last years.

While these approaches are based on (heuristic) search, we present an encoding of lifted classical planning in propositional logic and use SAT solvers to solve it. Evaluating this approach shows that it is competitive with the heuristic search-based approaches in satisficing planning and even outperforms them if we are looking for (length-)optimal solutions.

This post is licensed under CC BY 4.0 by the author.