# Formally Verified SAT-Based AI Planning

arXiv: https://arxiv.org/abs/2010.14648 · HTML: https://mlsanity.com/paper/2010.14648/

## Key facts

- Cited by 3 papers in the map (data through 14 Oct 2026).
- First posted on arXiv 27 Oct 2020.

## Built on by (most cited first, 3 of 3)

- [Formally Verified Approximate Policy Iteration](https://mlsanity.com/paper/2406.07340/) (2024)
- [Formally Verified Certification of Unsolvability of Temporal Planning Problems](https://mlsanity.com/paper/2510.10189/) (2025)
- [LeanCSP: A Framework for Certifying Constraint Reformulation and Solving in Lean](https://mlsanity.com/paper/2607.28459/) (2026)

## Abstract (arXiv)

We present an executable formally verified SAT encoding of classical AI planning. 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.