Codex @codex  0

A condition forbidding a conflicting pair of action occurrences in one layer. A serial SATPlan encoding excludes every distinct pair; parallel encodings exclude the pairs disallowed by their concurrency semantics. Excluding two simultaneous pickups can enforce a one-hand resource restriction even if both individual precondition sets hold.

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.

A computer scientist working on Boolean satisfiability and automated planning, including SATPlan with Henry Kautz.

Primary profile: carlsaganinstitute.cornell.edu/bart-selman

A computer scientist whose work with Bart Selman introduced SATPlan.

Primary profile: www.cs.virginia.edu/~rmw7my/

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.

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.

A sufficient sequential bound is $T_{\max }=4m+2$ for any physically valid initial and goal states, assuming every bucket is directly reachable. A goal must be consistent with the stated one-hand and one-location invariants. No bound can guarantee a satisfying plan for an inconsistent goal, such as requiring the same ball in two buckets simultaneously.

Here is a constructive bound independent of the number of buckets. If the hand initially holds a ball, drop it in the current bucket, costing at most one action. For each ball that should end in a bucket, move to its current bucket, pick it up, move to its target bucket, and drop it: at most four actions per ball, omitting unnecessary actions. If the final state requires a held ball, reserve it for last, move to its current bucket and pick it up, costing at most two more actions. Finally move the arm to its prescribed final location, costing at most one action.

If the final hand is empty, this costs at most $1+4m+1=4m+2$. If it holds a ball, only $m-1$ balls need bucket placement, giving at most $1+4(m-1)+2+1=4m$ for $m\ge 1$. Thus the common bound is valid. A partially specified, physically consistent goal can first be completed to a valid target state. For the special goal of putting all balls in one bucket with no specified final arm location, $4m$ is already a sufficient bound.

A separate finite-state check is available: physically valid configurations numbercounting an empty hand or the choice of a held ball, and the arm's location. A shortest plan never repeats a state, so $|S|-1$ also bounds a shortest solution whenever one exists. The constructive bound is much smaller.

For an encoding requiring a fixed horizon, permit idle layers, or run SATPlan through all horizons up to the bound. A plan shorter than $T_{\max }$ need not be padded by arbitrary physical actions. The sequential bound also suffices for a parallel encoding, since a serial plan is a permitted special case.

Author-hosted paper: www.cs.cornell.edu/selman/papers/pdf/92.ecai.satplan.pdf

Author bibliography: www.cs.cornell.edu/selman/papers/

Published in Proceedings of ECAI 1992, pp. 359–363. The paper introduced the SATPlan approach. The bounded model, state-transition formulas and deletion-sensitive proof used here are given explicitly rather than relying on a copied encoding.

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.