 Solution

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.