Effective SAT Planning by Speculative Computation

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 SATplanner firstly translates a planning problem into the boolean satisfiability (SAT) problem, and secondly solves it by a general-purpose SAT solver. Blackbox [1], 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).

Authors and Affiliations

1. Yamanashi University, 4-3-11 Takeda, 400-8511, Kofu-shi, Japan

   Hidetomo Nabeshima & Koji Iwanuma

2. Kobe University, Rokkodai-cho, 657-8501, Nada-ku, Kobe, Japan

   Katsumi Inoue

Editors and Affiliations

1. Australian Defence Force Academy, University of New South Wales, ACT 2600, Canberra, Australia

   Bob McKay

2. Computer Science Laboratory, Australian National University, RSISE Building, ACT 0200, Canberra, Australia

   John Slaney

Reprints and permissions

© 2002 Springer-Verlag Berlin Heidelberg

Policies and ethics