Verified SAT-Based AI Planning

Title:	Verified SAT-Based AI Planning
Authors:	Mohammad Abdulaziz and Friedrich Kurz
Submission date:	2020-10-29
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.
BibTeX:	@article{Verified_SAT_Based_AI_Planning-AFP, author = {Mohammad Abdulaziz and Friedrich Kurz}, title = {Verified SAT-Based AI Planning}, journal = {Archive of Formal Proofs}, month = oct, year = 2020, note = {\url{https://isa-afp.org/entries/Verified_SAT_Based_AI_Planning.html}, Formal proof development}, ISSN = {2150-914x}, }
License:	BSD License
Depends on:	AI_Planning_Languages_Semantics, List-Index, Propositional_Proof_Systems
Status: [ok]	This is a development version of this entry. It might change over time and is not stable. Please refer to release versions for citations.