A python framework for Optimal Planning Modulo Theories.
This thesis is concerned with the problem of generating optimal plans for
numeric planning domains with action costs. Solving these
problems efficiently requires a seamless integration between
propositional and numeric reasoning. To this end, the candidate
will leverage recent advances in general-purpose automated reasoning
and implement a domain-independent optimal theory-planner.
To kickstart this work, the candidate will be given a prototypical
implementation of an OMT-based planner written in Python 2.
About the current implementation:
The planner takes as input planning problems written in PDDL
(https://en.wikipedia.org/wiki/Planning_Domain_Definition_Language),
compiles them into SMTLib (http://smtlib.cs.uiowa.edu/) formulas
and feeds them to nuZ, an optimizing SMT solver (i.e., OMT solver).
Parsing of PDDL domains is done using a python module taken
from the Temporal Fast Downward planning system
(http://gki.informatik.uni-freiburg.de/tools/tfd/).
Construction of SMTLib formulas and solving is done using
the python API of nuZ (http://z3prover.github.io/api/html/index.html)
Tasks of the candidate will include:
- converting the parsing module from Python 2 to Python 3;
- refactoring/improving the compilation into SMTLib
(namely, improve the way we traverse the parsed objects
in the current implementation);
- replace solver specific calls that are currently done
using the Z3 Python APIs with solver-agnostic API's of
pySMT (https://github.com/pysmt/pysmt);
- IMPORTANT: pySMT currently does not support optimization,
so one task of the candidate will include extending pySMT
with wrappers for optimizing solvers (e.g. nuZ, optimathsat, SMT-RAT);
- perform experiments on well-known benchmarks from the
planning literature to assess strengths and weaknesses
of different solvers on numeric domains.