Abstract:
While classical planning systems can usually detect if a task is
unsolvable, only recent research introduced a way to verify such a claim.
These methods have already been applied to a variety of explicit and symbolic
search algorithms, but so far no planning technique based on SAT has been
covered with them. We fill this gap by showing how \emph{property directed
reachability} can produce proofs while only minimally altering the framework by
allowing to utilize certificates for unsolvable SAT queries within the proof.
We additionally show that a variant of the algorithm that does not use SAT
calls can produce proofs that fit into the existing framework without
requiring any changes.
