Formally Verified SAT-Based AI Planning

In the realm of planning, this approach was pioneered by Howey, Long, and Fox As witnessed by the different planning competitions (Long who developed VAL (Howey, Long, and Fox 2004) that, 2000; Coles et al. 2012; Vallati et al. 2015), planning algorithms given a planning problem and potential solution, certifies and systems are becoming more and more scalable that the solution actually solves the given problem. Also, and efficient, which makes them suited for more realistic certifying unsolvability for planning was tackled by Eriksson, applications. Given that many applications of planning Röger, and Helmert (2017) who provided unsolvability are safety-critical, increasing the trustworthiness of certificates and checkers for state-space search algorithms planning algorithms and systems--i.e. the likelihood that and by Eriksson and Helmert (2020) for property they compute correct results--could be instrumental in their directed SATbased planning.