 Solution

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 $\mathrm{At}(w)$ and a static predicate $\mathrm{Next}(w,w^{\prime })$ containing exactly the permitted dictionary mutations. For the action schema $\mathrm{Change}(w,w^{\prime })$, useInitialize $\mathrm{At}(s)$ and the static transition facts, and use goal $\mathrm{At}(t)$. Only one $\mathrm{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^{2}L)$ character comparisons, although indexing can do better; the number of stored transitions is at most $NL(|\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 $\mathrm{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.