Solution (source code)

= Solution

\b[The difficulty is representing dictionary membership and the one-letter relationship in positive conjunctive <STRIPS> <preconditions>; a finite dictionary nevertheless admits an exact encoding.] Pure <STRIPS> does not provide string indexing, a “differs in one position” operator, arbitrary disjunctive tests or a procedure that calls a dictionary lookup. Those relationships must be represented by ground facts or compiled into <ground actions>.

One exact whole-word encoding uses a <planning fluent> $\operatorname{At}(w)$ and a <static predicate> $\operatorname{Next}(w,w')$ containing exactly the permitted dictionary mutations. For the <action schema> $\operatorname{Change}(w,w')$, use
$$
\begin{aligned}
\operatorname{Pre}&=\{\operatorname{At}(w),\operatorname{Next}(w,w')\},\\
\operatorname{Add}&=\{\operatorname{At}(w')\},\\
\operatorname{Del}&=\{\operatorname{At}(w)\}.
\end{aligned}
$$
Initialize $\operatorname{At}(s)$ and the static transition facts, and use goal $\operatorname{At}(t)$. Only one $\operatorname{At}$ fact is true initially. Each applicable <ground action> deletes it and adds exactly its permitted successor, so <mathematical induction> proves that exactly one current-word fact remains true and that every <plan> is a legal <word ladder>. Conversely, every legal <word ladder> directly supplies a <plan>. An isolated non-dictionary start is handled as in (c). A shortest <plan> has the fewest mutations.

This encoding moves the hard lexical relationship into preprocessing. For $N$ dictionary words, checking all ordered pairs takes $O(N^2L)$ character comparisons, although indexing can do better; the number of stored transitions is at most $N L(|\Sigma|-1)$ when all states are dictionary words. The <STRIPS> representation is finite, but its size and preprocessing cost matter.

A position-based representation instead uses <planning fluents> $\operatorname{Letter}(i,\ell)$. Changing position $i$ must delete its old letter and add its new one; all other positions persist through the <STRIPS> update rule. Merely requiring each position to contain a letter admits non-dictionary strings. A disjunction over all dictionary words is not a positive conjunctive <STRIPS> <precondition>. It can be compiled into separate <ground actions>, each requiring every letter of a valid source word and changing one position to reach a valid destination. This again enumerates lexical cases and can be large. Arbitrary letter changes followed by an unconstrained “validate” action are unsound: several illegal intermediate strings could otherwise lead to a legal goal. Legality must hold after every mutation, not only at the endpoint.