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.