Formally Verified SAT-Based AI Planning
DOI:
https://doi.org/10.1609/aaai.v37i12.26714Keywords:
GeneralAbstract
We present an executable formally verified SAT encoding of ground classical AI planning problems. We use the theorem prover Isabelle/HOL to perform the verification. We experimentally test the verified encoding and show that it can be used for reasonably sized standard 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.Downloads
Published
2023-06-26
How to Cite
Abdulaziz, M., & Kurz, F. (2023). Formally Verified SAT-Based AI Planning. Proceedings of the AAAI Conference on Artificial Intelligence, 37(12), 14665-14673. https://doi.org/10.1609/aaai.v37i12.26714
Issue
Section
AAAI Special Track on Safe and Robust AI