OMTPlan provides a Python framework for cost-optimal planning in numeric domains.

Clone the OMTPlan repository in your favourite folder.

git clone https://github.com/fraleo/OMTPlan.git

To run OMTPlan, make sure you have the following on your machine

• Python 2.7
• Z3 (4.8.6) and its Python API. Make sure you add z3 Python bindings to your Python search path.
• NetworkX (as simple as pip install networkx)
• the VAL plan validation software. Here you can find some instructions to help you set it up. Once built, add the validate binary to the /bin folder.

Already provided within this repo are the following external modules

• A modified version of the Temporal Fast Downward Python parser.

To see the list of input arguments, type

./omtplan -h

To run OMTPlan on a problem, type, e.g.,

./omtplan -omt -parallel -domain domain.pddl problem.pddl

or

./omtplan -omt -parallel problem.pddl

if PDDL files describing domain and problem are in the same folder.

To produce an SMT-LIB encoding of the bounded planning problem, type, e.g.,

./omtplan.py -smt -parallel -translate bound problem.pddl 

You can find some planning problems written in PDDL in pddl_examples.

Further documentation is available here.

Francesco Leofante

Do not hesitate to contact me if you have problems using OMTPlan, or if you find bugs :)

If you decide to use OMTPlan for your experiments, please cite

@inproceedings{LeofanteGAT20,
  author    = {Francesco Leofante and
	       Enrico Giunchiglia and
	       Erika {\'{A}}brah{\'{a}}m and
	       Armando Tacchella},
  editor    = {Christian Bessiere},
  title     = {Optimal Planning Modulo Theories},
  booktitle = {Proceedings of the Twenty-Ninth International Joint Conference on
	       Artificial Intelligence, {IJCAI} 2020 },
  pages     = {4128--4134},
  publisher = {ijcai.org},
  year      = {2020},
  url       = {https://doi.org/10.24963/ijcai.2020/571}
}