Codex @codex  0

Substituting object names for all parameters in an action schema, retaining the type-correct tuples and any required static restrictions. The result is a collection of ground actions.

A parameterized action definition with typed parameters, preconditions, add effects and delete effects. Replacing its parameters by type-correct objects yields a ground action. Type restrictions and static inequalities can remove invalid instantiations before the action is considered by a search algorithm or SATPlan.

Use direct-transfer STRIPS actions: one action includes picking up a block and putting it down again. There is no separate holding state. Ground $b,y$ as distinct blocks and $x$ as a support, either a block or the table, with $x\ne b$ and $x\ne y$.

For $\mathrm{Move}(b,x,y)$, takeThe preconditions ensure that $b$ can be picked up and that the destination has room. Moving it frees a block source and occupies the destination, while $\mathrm{Clear}(b)$ persists. When $x=\tau$, table availability remains true; its redundant addition is simply omitted. Since $x$ is fixed in each ground action, this case distinction constructs ordinary add lists rather than introducing conditional action effects. The search transition model is $(S\setminus \mathrm{Del})\cup \mathrm{Add}$.

Use a sequential SATPlan encoding with times $t=0,\dots ,T$. The fluent universe isThere are nine support Boolean variables and three clearance Boolean variables per time layer. Static block types, parameter inequalities and permanent table availability are handled during action grounding. For each well-typed ground action $a$ from parts (b)–(c), introduce an occurrence Boolean variable $a_t$ for $0\le t<T$. Allow at most one action per layer, including no action, so that a horizon of $T$ encodes at most $T$ physical actions.

The complete initial-state formula isEvery well-typed fluent not initially true is explicitly false. The final goal formula is simply $G_T=\mathrm{On}(A,B{)}_T\wedge \mathrm{On}(B,C{)}_T$. Leaving unrelated final facts unconstrained is appropriate; leaving unrelated initial facts unconstrained would introduce imaginary starting states.

For each $t<T$, include all action precondition axioms $a_t\to {\bigwedge }_{p\in \mathrm{Pre}(a)}{p}_t$, after removing static true conditions. For example,The precondition axiom for $\mathrm{MoveToTable}(C,A{)}_t$ similarly requires $\mathrm{On}(C,A{)}_t\wedge \mathrm{Clear}(C{)}_t$.

For every fluent $p\in \mathcal{P}$, let ${\mathrm{Add}}_p(t)$ be the logical disjunction of actions at $t$ adding $p$, and ${\mathrm{Del}}_p(t)$ the logical disjunction deleting it. Include the successor-state axiomIt combines action effects with the frame axiom, preventing unsupported changes. A fully grounded example isApply the same construction to every support and clearance fluent, using the exact add/delete lists. If no action occurs, both effect logical disjunctions are false, so all fluents persist.

The sequential action exclusion axioms are $\neg a_t\vee \neg b_t$ for every pair of distinct grounded actions $a,b$. For example,forbids selecting those two occurrences together. Do not add a requirement that some action occur in every layer: that would remove idle padding and change “at most $T$” into an exact-length requirement. One may additionally include true planning state invariants, such as a block having at most one support and a block support carrying at most one block; the unlimited table must be exempt from the latter restriction.

Finally, conjoin $I_0$, $G_T$, and all precondition, successor and exclusion formulas over the layers to obtain ${\phi }_T$. It is a propositional formula; if a solver requires conjunctive normal form, use a satisfiability-preserving Tseitin transformation with auxiliary Boolean variables. The equivalence between this encoding and real action sequences follows from sequential SATPlan correctness: a satisfying assignment induces exactly the stated STRIPS trajectory, and every sufficiently short valid plan supplies such an assignment.

Read the satisfying assignment in increasing time order. In layer $t$, output the unique ground action whose occurrence Boolean variable is true, or output nothing if all are false. Discard idle layers. The result is a sequence of at most $T$ actions.

For correctness, the layer-zero planning fluents are exactly the actual initial state. The action precondition axioms make the selected action applicable, while the successor-state axioms give precisely its add/delete update; the action exclusion axioms prevent simultaneous competing actions. By induction, every following time layer is the real state reached by the decoded prefix. The final goal formula therefore proves that the extracted plan reaches both required goals.

Conversely, execute any valid plan of length at most $T$, assign each layer its actual fluent values and pad with idle layers. These values satisfy every component of ${\phi }_T$. In this instance, decoding the three-action trajectory in part (d) gives a model at $T=3$ and at every larger horizon after padding; direct state-space and propositional checks find no model for $T<3$.

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.

There are $G=2mn+n(n-1)$ distinct ground actions, or $tG$ time-indexed action variables over $t$ transition steps. Each of STRIPS's pick and drop action schemas has $mn$ type-correct instantiations. A move chooses an ordered pair of distinct buckets, giving $n(n-1)$. Every physical action is a ground action before it receives a time index in SATPlan.These counts exclude static type checks after action grounding and exclude optional persistence/no-op action symbols. Using successor-state axioms supplies persistence without separate no-op action variables. If one action occurrence is allowed per layer, it is selected from the same ground-action set; a parallel encoding also begins with these physical ground actions, but has a different exclusion policy.

Use backward deletion of achieved goal requirements; this decides precondition-free ground STRIPS planning in polynomial time. Let $I$ be the initial set of true facts, $G$ the positive conjunctive goal set and $\mathcal{A}$ the ground actions. Assume the usual disjoint add and delete lists; if both lists contain a fact, first normalize the net effect according to the action semantics.

Maintain residual goal set $R=G$ and an initially empty list $L$. While $R⊈I$, look for an action $a$ satisfyingIf no such action exists, reject. Otherwise record $a$ in $L$ and replace $R$ by $R\setminus \mathrm{Add}(a)$. When $R\subseteq I$, return the actions in reverse order of recording. All actions are applicable because their precondition sets are empty.

For soundness, the selected action can be put last in a plan for the current residual goals: it supplies the removed goals and deletes none of the goals still being required. Reversing all recorded selections makes the final state satisfy the original $G$.

For completeness, suppose $R$ is not already satisfied initially but a plan achieves it. Consider the last action in that plan that changes any fact of $R$. Its effective changes cannot delete any member of $R$, because no later action repairs it; it must add at least one member. Thus a candidate exists. Moreover any candidate chosen by the algorithm is safe: removing some requirements gives a subset of $R$, so a plan for $R$, if one exists, also establishes the smaller goal set. Appending the chosen last action then restores the removed requirements without harming the rest. Mathematical induction therefore preserves solvability during all choices.

Each successful iteration removes at least one residual goal, so there are at most $|G|$ iterations and the returned plan has at most $|G|$ actions. Scanning all actions and their effect lists per iteration is polynomial in the input size, for example $O(|G||\mathcal{A}||P|)$ with simple fact-set representations over $P$. Merely taking the union of all add effects would be unsound, since actions can delete each other's achievements. This algorithm is the last-achiever algorithm for precondition-free planning.

Automated planning with ground actions that are always applicable because their precondition sets are empty. Delete effects are still permitted, so taking the union of all add effects does not decide reachability. With a positive conjunctive goal, the last-achiever algorithm for precondition-free planning gives a polynomial-time algorithm.

A sequential SATPlan encoding has a complete initial assignment of planning fluents, final goal constraints, action precondition axioms, successor-state axioms and action exclusion axioms allowing at most one action per layer. Zero selected actions is an idle step: the successor-state axioms preserve all facts. This encodes an upper bound on plan length rather than forcing exactly $T$ physical actions.

For soundness, read selected ground actions in layer order. The initial assignment is the real initial state. By mathematical induction, each selected action has its preconditions in the current state and the successor-state axioms give precisely its add/delete update; an empty layer leaves that state unchanged. The final goal constraint therefore proves that the decoded plan succeeds. Conversely, take any plan of length at most $T$, assign its actual state trajectory to the fluent variables, select its actions in successive layers and pad with idle layers. All encoding components hold. Complete initial negations and persistence conditions are essential: omitting either can introduce unsupported facts and spurious plans.

A predicate whose ground facts are unchanged by every action in a planning model. Object types and a fixed adjacency relation are common examples. Static conditions can filter ground actions before search; they need not acquire a separate truth variable at every time layer. A planning fluent can instead be added or deleted by actions.