Computing Plan-Length Bounds Using Lengths of Longest Paths

Rintanen and Gretton 2013; Abdulaziz, Gretton, and Norrish Many techniques for solving problems defined on transition 2015; Abdulaziz, Gretton, and Norrish 2017; Abdulaziz systems, like SATbased planning (Kautz and Selman 2019). Such compositional methods are currently the only 1992) and bounded model checking (Biere et al. 1999), benefit practically viable method to compute bounds on plan lengths from knowledge of upper bounds on the lengths of solution or the state space diameter. Compositional approaches provide transition sequences, aka completeness thresholds. If N useful approximations of plan bounds using smaller is such a bound, and if a solution exists, then that solution computational effort, since only explicit representations of need not comprise more than N transitions.