AAAI 2023technical5 citations
Formally Verified SAT-Based AI Planning
Mohammad Abdulaziz, Friedrich Kurz
Abstract
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.
BibTeX
@article{Abdulaziz_Kurz_2023, title={Formally Verified SAT-Based AI Planning}, volume={37}, url={https://ojs.aaai.org/index.php/AAAI/article/view/26714}, DOI={10.1609/aaai.v37i12.26714}, abstractNote={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.}, number={12}, journal={Proceedings of the AAAI Conference on Artificial Intelligence}, author={Abdulaziz, Mohammad and Kurz, Friedrich}, year={2023}, month={Jun.}, pages={14665-14673} }