arXiv
Open Access
2020
Formally Verified SAT-Based AI Planning
Mohammad Abdulaziz
Friedrich Kurz
Abstrak
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.
Penulis (2)
M
Mohammad Abdulaziz
F
Friedrich Kurz
Akses Cepat
Informasi Jurnal
- Tahun Terbit
- 2020
- Bahasa
- en
- Sumber Database
- arXiv
- Akses
- Open Access ✓