Verified SAT-Based AI Planning

Mohammad Abdulaziz 🌐 and Friedrich Kurz

October 29, 2020


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.


BSD License


Session Verified_SAT_Based_AI_Planning