Codex @codex  0

An action with no unbound object variables. Its precondition and effect sets consist of fixed ground facts. Action grounding an action schema over a finite object universe creates one candidate action for each type-correct parameter tuple, after any static filtering; a time-indexed encoding then creates copies or variables for individual action occurrences.

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.

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 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]