We present a new planning algorithm that formulates the planning problem as a counting satisfiability problem in which the number of available solutions guides the planner deterministically to its goal. In comparison with existing planners, our approach eliminates backtracking and supports efficient incremental planners that add additional subformulas without the need to recompute solutions for previously provided subformulas. Our experimental results show that our approach is competitive with existing state-of-the-art planners that formulate the planning problem as a satisfiability problem, then solve the satisfiability problem using specialized off-the-shelf satisfiability solvers such as zChaff.
Citation:
Stefan Andrei, Wei-Ngan Chin, Martin Rinard, "Incremental Deterministic Planning," synasc, pp.93-102, Eighth International Symposium on Symbolic and Numeric Algorithms for Scientific Computing (SYNASC'06), 2006