SMT Solving for AI Planning: Theory, Tools and Applications

 28th International Conference on Automated Planning and Scheduling
June 25th, 2018
Delft, NL

Organizers: Erika Ábrahám, Francesco Leofante

Satisfiability checking aims to develop algorithms and tools for checking the satisfiability of quantifier-free logical formulas. Besides powerful SAT solvers for propositional logic, sophisticated SAT-modulo-theories (SMT) solvers are available for a wide range of theories (real, integer and mixed-integer arithmetic, theories of lists, bit vectors, uninterpreted functions, etc.), and recently offer also functionalities for optimization. Modern SMT solvers achieve impressive performance and are applied as black-box engines in many technologies in different areas. This tutorial aims to introduce the audience to SMT solving and to demonstrate how SMT solvers can be exploited to solve planning problems.

The tutorial will begin with a short introduction to the theoretical foundations of satisfiability checking, followed by an overview of the most popular SMT solvers, their common standards, and an illustration of how to use their satisfiability checking and optimization capabilities. The tutorial will finally present an application for integrated planning and execution within the Planning and Execution Competition for Logistics Robots in Simulation.

Additional resources