Streszczenie (autorskie):

Planning as satisfiability encodes a planning problem as a logical formula and delegates the search to a general-purpose solver — structurally analogous to bounded model checking for transition systems. This talk presents an implementation and systematic empirical evaluation of this paradigm using SMT and Bounded Model Checking. We encode a parameterised grid-world planning domain as a single SMT formula over the Z3 solver, extended with cost constraints over linear integer arithmetic, and benchmark it against Fast Downward configurations (A* with LM-cut, hmax, and LAMA) across five experimental axes. The results characterise a clear expressiveness-versus-scalability trade-off: SMT-based planning handles rich arithmetic constraints that heuristic search cannot natively represent, but pays a significant computational cost on pure classical planning tasks. We close by discussing when solver-based approaches are the right tool, and open questions motivating extensions to richer planning settings.