Verified SAT-Based AI Planning

Mohammad Abdulaziz 🌐 and Friedrich Kurz

October 29, 2020

This is a development version of this entry. It might change over time and is not stable. Please refer to release versions for citations.

Abstract

We present an executable formally verified SAT encoding of classical AI planning that is based on the encodings by Kautz and Selman and the one by Rintanen et al. The encoding was experimentally tested and shown to be usable for reasonably sized standard AI planning benchmarks. We also use it as a reference to test a state-of-the-art SAT-based planner, showing that it sometimes falsely claims that problems have no solutions of certain lengths. The formalisation in this submission was described in an independent publication.

License

BSD License

Topics

Session Verified_SAT_Based_AI_Planning