Property directed reachability for automated planning

摘要: Property Directed Reachability (PDR) is a very promising recent method for deciding reachability in symbolically represented transition systems. While originally conceived as model checking algorithm hardware circuits, it has already been successfully applied several other areas. This paper the first investigation of PDR from perspective automated planning. Similarly to planning satisfiability paradigm, draws its strength internally employing an efficient SAT-solver. We show that most standard encoding schemes into SAT can be directly used turn algorithm. As non-obvious alternative, we propose replace SAT-solver inside by planning-specific procedure implementing same interface. free variant not only more efficient, but offers additional insights and opportunities further improvements. An experimental comparison state art planners finds highly competitive, solving problems on domains.