7.3 Planning by Satisfiability 151
We can now formalize the notion of encoding correctly a planning problem into
a satisfiability problem. Let = (S, A , γ ) be a deterministic state-transition system
(as described in Section 1.4). Let P = (, s
0
, S
g
) be a classical planning problem,
where s
0
and S
g
are the initial and goal states, respectively. Let Enc be a function
that takes a planning problem P and a length bound n and returns a propositional
formula : Enc(P, n) = .
Definition 7.1 Enc encodes the planning problem P to a satisfiability problem when the
following holds: is satisfiable iff there exists a solution plan of length n to P.We
say, in short, that Enc encodes planning to satisfiability.
Proposition 7.1 The encoding defined by Formulas 7.9