Codex @codex  0

The blocks world is a classical planning model of movable blocks arranged in stacks on an unlimited table. Each block has one support, each block supports at most one other block, and the support relation has no directed cycle. A clear block can move onto another clear block or onto the table. In a direct-transfer STRIPS representation, an action includes the entire pickup-and-placement operation; a separate holding or empty-hand planning fluent is unnecessary unless the action model explicitly splits those operations.

The table has unlimited capacity, so its availability must not be deleted when a block is placed there. Planning state invariants connect the predicate describing a clear block to the absence of any block directly above it. Goal interaction in planning makes this small model useful for testing automated planning methods.

Write $\tau$ for the table. The positive initial planning fluents read from the original figure areThe static type facts are $\mathrm{Block}(A)$, $\mathrm{Block}(B)$ and $\mathrm{Block}(C)$; the table is not a block. With an explicit table-availability predicate, take $\mathrm{Clear}(\tau )$ to be permanently true. Under the closed-world assumption, all other well-typed initial planning fluents are false; in particular, $A$ is not clear.

The goal is the partial-state conjunctionIt need not redundantly prescribe every final fact. With only these three blocks and a valid blocks world state, the completed stack also places $C$ on the table and leaves $A$ clear.

Ground $b,x$ as distinct blocks. For $\mathrm{MoveToTable}(b,x)$, takeThus a clear block leaves its block support, makes that support clear, and joins the unlimited table. $\mathrm{Clear}(b)$ persists, and table availability is never deleted. Requiring $x$ to be a block excludes a redundant table-to-table action. The static predicates need not be stored as time-varying planning fluents.

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.

Use location, holding and hand-capacity planning fluents, together with static object types. Write $\mathrm{In}(b,k)$, $\mathrm{Holding}(b)$, $\mathrm{At}(k)$ and $\mathrm{Empty}$ for a ball's bucket, the held ball, the arm's location and an empty hand. Static predicates $\mathrm{Ball}(b)$, $\mathrm{Bucket}(k)$ and $\mathrm{Different}(k,\ell )$ identify types and distinct buckets. The latter can equivalently be a action grounding restriction.

For typed parameters, the STRIPS actions areUntyped notation adds the appropriate $\mathrm{Ball}$ and $\mathrm{Bucket}$ facts to every precondition set. Static type and inequality facts have no add or delete effects. A state is a set of true ground facts under the closed-world assumption, and an applicable action produces $(S\setminus \mathrm{Del})\cup \mathrm{Add}$.

Start from a physically valid state: each ball is in exactly one bucket or held; at most one ball is held; the arm is at exactly one bucket; and $\mathrm{Empty}$ is true exactly when no ball is held. The operators preserve these planning state invariants. In particular, picking requires an empty hand, dropping releases the held ball, and moving deletes the old arm location. Moving while holding a ball is permitted, so a separate carried-ball movement action is unnecessary.

Label the balls $a,b,c,d$ and buckets $1,2,3$. Ignoring unchanged static type facts, the initial state's true planning fluents areExpanding it produces exactly three successors. The held ball makes $\mathrm{Empty}$ false, so neither ball in bucket $1$ can be picked up yet.

For $\mathrm{Drop}(d,1)$, replace $\mathrm{Holding}(d)$ by $\mathrm{In}(d,1)$ and $\mathrm{Empty}$; the arm stays at bucket $1$. All four balls are then in buckets, with $a,b,d$ in $1$ and $c$ in $2$.

For $\mathrm{Move}(1,2)$, replace $\mathrm{At}(1)$ by $\mathrm{At}(2)$ and leave every ball planning fluent unchanged, including $\mathrm{Holding}(d)$.

For $\mathrm{Move}(1,3)$, similarly replace only the arm-location planning fluent by $\mathrm{At}(3)$. The arm is now over the destination while still holding $d$; it has not yet dropped that ball.

No other action is applicable: the other drop locations fail their arm-location precondition, no pick has an empty hand, and moves from another source bucket fail their source-location precondition. None of these three successors satisfies ${\bigwedge }_{z\in \{a,b,c,d\}}\mathrm{In}(z,3)$. This describes one forward state-space planning expansion, not an assertion that the search has already found a complete plan.

Use balls $a,b$, buckets $1,2$, transition index $k$ and the grounded action schemas from (a). Under a sequential encoding, one example successor-state axiom isBall $a$ is in bucket $1$ afterwards exactly when it is dropped there now, or it was there and is not picked up. Actions involving other balls or arm movement leave this fact unchanged. This is both an effect rule and a persistence rule, rather than an implication that permits spontaneous appearances.

An example action precondition axiom isA selected pick action must have the ball, arm and empty hand in the appropriate current state. The static type conditions have already been satisfied by action grounding.

An example action exclusion axiom isThe single arm cannot pick up both balls in one step. For a serial encoding include such an exclusion for every pair of distinct action occurrences at one layer; with at-most-one rather than exactly-one actions, a layer may idle. Initial-state clauses, goal clauses and corresponding successor-state axioms for all other planning fluents complete the plan-as-SAT construction. The plan-as-SAT approach was introduced by Henry Kautz and Bart Selman in 1992.^[ref]

A corrected STRIPS model can fix object roles in the action names, leaving only room parameters to instantiate. Use the same $a,w,g,r$ and introduce static $\mathrm{pitfree}(z)$ and $\mathrm{exit}(z)$ facts, plus a planning fluent $\mathrm{clear}(z)$ meaning “no live monster occupies $z$”. Unlike the supplied adjacency relation, let $\mathrm{adj}$ describe all geometrically adjacent rooms; safety is then explicit rather than hidden by missing edges.

Initially the agent, monster and gold have their specified locations, $\mathrm{have}(a,r)$, $\mathrm{alive}(w)$ and $\mathrm{active}$ hold, $\mathrm{exit}(s_{11})$ holds, $\mathrm{pitfree}$ holds at every room except $s_{12}$, and $\mathrm{clear}$ holds at every room except $s_{23}$. All unlisted facts are false by the closed-world assumption. The following positive preconditions, add lists and delete lists are a complete action specification:Require $\mathrm{exited}$ as the goal. If reaching the exit suffices, omit $\mathrm{Leave}$ and use the original two goal facts. Instantiating these schemata over the finite room set gives ordinary ground STRIPS actions.

Only $a$ moves, only $g$ is collectible and only $r$ can be fired at $w$. No action changes the monster’s location; its corpse can stay there, while $\mathrm{clear}$ records that it is harmless. The gold stays at its original room until collection. The arrow is consumed by its only use. By mathematical induction on plan length, every applicable action preserves the planning state invariant that the active agent occupies one pit-free room without a live monster. Consequently every solution is a safe execution. The plan in part a, followed by $\mathrm{Leave}(s_{11})$, is one such execution.

In STRIPS, a state records the true ground facts; under the closed-world assumption, an absent fact is false. An action with positive preconditions $P$, add effects $A$ and delete effects $D$ applies when $P\subseteq S$, producing $(S\setminus D)\cup A$.

The given movement action adds the destination fact without deleting the old boat location. After its first crossing the boat can therefore be recorded at both banks, allowing physically impossible loading. Its source-bank symbol is also not a declared action parameter. Repair both issues by using the fully parameterized STRIPS actionHere $\mathrm{notEqual}(s,t)$ excludes a vacuous same-bank crossing. The two static inequality facts already supplied suffice.

The given loading action has no capacity check. Consecutive loads can put arbitrarily many items aboard. Introduce a nullary planning fluent $\mathrm{Empty}$, true initially, and repair loading toUnloading must restore $\mathrm{Empty}$, as in part (c). Including the bank $s$ explicitly as an action parameter removes the other unbound action variable. Equivalently, instantiate separate east-bank and west-bank actions.

These repairs establish the planning state invariants that the boat is at exactly one bank, each item is either at one bank or aboard, and at most one item is aboard. The first two hold initially and are preserved by deleting the former location when adding the new one; the capacity marker permits loading only when no item is aboard. Grounding implicit location variables alone would not repair the missing delete effect or the missing capacity check.

Replace the one-place marker $\mathrm{Empty}$ by three nullary planning fluents $q_0,q_1,q_2$, meaning that zero, one or two items are aboard. Initially only $q_0$ is true. Exactly one of these facts is maintained. No additional object constants are needed.

For compactness, define the common loading preconditionsand common unloading preconditionsThe four STRIPS actions areHere the first unloading removes one of two items, and the last unloading removes the sole remaining item; items do not require fixed seat identities. The movement action remains as repaired in part (a) and changes none of the occupancy facts.

The planning state invariant is $q_j$ true exactly when $j$ items are aboard. Every action changes the marker by the same amount as the actual onboard count, so it follows by mathematical induction from the initial empty boat. In particular, a third load is impossible.

A fact whose truth can change as actions execute in automated planning. Ground location facts and an empty-container marker are examples. In STRIPS, static facts such as an object's fixed type are never added or deleted, while planning fluents can appear in action effects.

An auxiliary planning fluent certifying that a safety condition has been checked for the current state in automated planning. A checking action requires facts establishing the condition and adds the certificate; the hazardous action requires that certificate.

Every action capable of invalidating the check must delete the certificate. Otherwise checking a safe configuration and then changing it could authorize an unsafe action using stale evidence. For river crossing, certify that the departure bank contains no incompatible pair, invalidate the certificate on every load, unload or crossing, and require it before sailing. This compiles a safety test into positive STRIPS preconditions when a suitable finite static compatibility relation is supplied.

An approach to automated planning that constructs a Boolean satisfiability problem for a bounded planning horizon, solves it and decodes a satisfying assignment into a plan. A typical encoding has time-indexed action occurrences and planning fluents, initial and goal clauses, action precondition axioms, state-transition constraints and action exclusion axioms. Sequential and parallel encodings have different notions of a step.

Henry Kautz and Bart Selman introduced planning as satisfiability in their 1992 paper.^[ref]

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.

A representation for automated planning in which a state $S$ is a set of true ground facts and an action has a positive precondition set $P$, add set $A$ and delete set $D$. Under the closed-world assumption, facts absent from $S$ are false. The action applies when $P\subseteq S$ and producesNegative effects are delete-list entries; they do not require negative preconditions. A movement action must delete an object's old location as well as add its destination. Capacity and safety restrictions require explicit action conditions or auxiliary planning fluents; they do not follow automatically from an intended physical interpretation.

A logical equivalence characterizing exactly when a planning fluent is true after one step. Here ${\mathrm{Add}}_F$ and ${\mathrm{Delete}}_F$ are disjunctions of selected actions with the respective effects, under a suitable action-conflict policy. The persistence term excludes spontaneous changes and captures the relevant frame axiom. An implication from add effects alone would not constrain all other state changes.