2020/10/27 by Mohammad Abdulaziz, Abdulaziz, Mohammad, Friedrich Kurz +1 · 2 citations
Computer Science · #AI-based Problem Solving and Planning #Logic, programming, and type systems #Formal Methods in Verification
paper · pdf · doi:10.48550/arxiv.2010.14648
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.