Summary: In recent years, SAT planning has been studied actively. In this paper, we propose a new method, called speculative computation, for accelerating the SAT planning. A SAT planner firstly translates a planning problem into the boolean satisfiability (SAT) problem, and secondly solves it by a general-purpose SAT solver. Blackbox, which is one of the fastest planning systems in the world, is based on this approach. Given a planning problem, Blackbox performs the following; (i) assumes that the plan length is \(i\) (initially, \(i =1)\), (ii) translates the planning problem into a SAT problem \(P_{i}\), and (iii) solves \(P_{i}\). If \(P_{i}\) is found to be satisfiable, the Blackbox extracts a plan of length \(i\) from the truth assignment satisfying \(P_{i}\). When \(P_{i}\) is unsatisfiable, the planner increases the plan length to be \(i +1\), and returns to (i).
For the entire collection see [Zbl 1014.00019].