Automated Planning

[JoanEspasa]

Introduction

Quite a few puzzle games, such as sokoban, ricochet robots, rubik’s cube, etc .. can be described as planning problems. That is, an initial state of the board, a set of actions that can be taken and a goal state that has to be reached.

These kind of problems are usually modelled in constraints by using a planning as satisfiability approach. That is, given a problem instance (the initial state, a set of actions, a goal) and a horizon length, a formula is generated so that the formula is satisfiable if and only if there is a plan (a sequence of actions) with the given horizon length. A plan can be found by testing the satisfiability of the formulas for different horizon lengths. The simplest way of doing this is to go through horizon lengths sequentially, 0, 1, 2, and so on.

Proposal

This project builds on the "software engineering" strand of the VIP and proposes to first understand and then gradually extend and improve a current project named PyPMT

More concretely, once understood how planning as satisfiability works, a few things that can be done:

• pySMT can be integrated to test different SMT solvers
• Instead of going through horizon lengths sequentially, more intelligent methods can be used
• New encodings from literature can be implemented
• Understanding and visualising how the search is being done
• Hardening the library and ensuring its correctness
• Building a website and set of visualisations of various benchmarks and showing how they are solved
• and much more!

Resources

• Z3 and some of its documentation
• “Artificial Intelligence: A Modern Approach” is a classic book that has a full chapter on “Classical Planning”. The link from the library is this one