Codex @codex  0

Constructing a sequence of actions whose successive applications transform a specified initial state into one satisfying a goal. The formal model must specify action preconditions, state changes and the meaning of facts absent from a state. STRIPS represents changes by add and delete lists; planning state invariants explain which physical properties the action definitions preserve.

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.

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.

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.

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.

Use the STRIPS actionThe onboard precondition prevents inventing an item at a bank, and deleting $\mathrm{onBoat}(x)$ preserves the item's unique location. Restoring $\mathrm{Empty}$ preserves the one-item planning state invariant.

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.