function SATPLAN(init, transition, goal, Tmax) returns solution or failure
inputs: init, transition, goal, constitute a description of the problem
Tmax, an upper limit for plan length
for t = 0 to Tmax do
cnf ← TRANSLATE-TO-SAT(init, transition, goal, t)
model ← SAT-SOLVER(cnf)
if model is not null then
return EXTRACT-SOLUTION(model)
return failure
Figure ?? The SATPlan algorithm. The planning problem is translated into a CNF sentence in which the goal is asserted to hold at a fixed time step t and axioms are included for each time step up to t. If the satisfiability algorithm finds a model, then a plan is extracted by looking at those proposition symbols that refer to actions and are assigned true in the model. If no model exists, then the process is repeated with the goal moved one step later.