Codex @codex  0

A clause or formula ensuring a selected action occurrence has all of its preconditions satisfied at the current time. It is one part of a plan encoding; action effects, persistence, initial conditions and goals require additional constraints.

A restricted goal-by-goal planning procedure chooses one subgoal, constructs a subplan for it without preparation motivated by other pending subgoals, then moves on while treating the earlier goal as protected. Destructive goal interaction in planning can defeat either ordering. Merely requiring the final plan to be a concatenation of subplans is a weaker condition: a subplan may already contain preparatory work useful to a later goal. A claimed impossibility must specify the stronger restriction rather than infer it from concatenation alone.

Two subgoals interact when actions needed for one can establish, obstruct or delete facts needed for the other. A plan for each subgoal separately need not combine into a plan for their conjunction. Preparing the world before committing to a subgoal, revising an earlier subplan or temporarily undoing an achieved fact can all be necessary. Goal-by-goal planning may therefore be incomplete.

An incremental belief-state search initially plans for a small subset $B_0$ of the possible initial states, then tests the candidate plan on the full initial belief state $B$. If a state in $B$ makes an action inapplicable or fails the final goal test, add that counterexample to $B_0$ and solve the enlarged problem. The new search may need to revise the entire plan, rather than append actions to the previous candidate.

With finitely many initial states and a complete finite-model solver for each restricted problem, at most $|B|$ state additions are required. Failure to find a plan even for a restricted subset proves that none can work for the whole belief state. A candidate that passes full validation is a genuine plan for sensorless planning. The advantage is selective tracking: a small number of representative initial states may force a universally successful plan without constructing the full power set search space.

Iterative lengthening search repeatedly runs cost-bounded depth-first search, starting with threshold zero and replacing each unsuccessful threshold by the smallest rejected path cost. It uses a depth-first search stack rather than the potentially large search frontier of uniform-cost search.

Suppose an optimal plan has cost $C^{\ast }$ and each pass terminates. At every unsuccessful threshold $L<C^{\ast }$, some first rejected prefix of an optimal plan has path cost at most $C^{\ast }$. Therefore the next threshold is no larger than $C^{\ast }$. Any first returned goal state has cost at most $C^{\ast }$ and hence exactly $C^{\ast }$. Finite branching factor and a positive lower bound on step costs ensure that only finitely many search nodes precede that cost, giving completeness as well as optimality. With arbitrary real step costs, the threshold increments can be much smaller than the smallest step cost: the difference between two path costs need not itself be a step cost.

Start with required facts $R=G$. If $R\subseteq I$, the empty prefix suffices. Otherwise choose an action adding a member of $R$ and deleting none of $R$, record it as a final action, and remove its add effects from $R$. Repeat and reverse the recorded actions when the residual requirements hold initially. Reject if no permitted action exists.

Soundness follows because each recorded last action supplies its removed requirements without deleting the remaining ones. If a plan satisfies a residual $R$ not contained in $I$, its last action affecting $R$ cannot delete an $R$-fact and must add one; therefore a candidate exists. Any selected candidate leaves a smaller required set, which is no harder to achieve than $R$. This proves completeness by mathematical induction. Every selection removes a required fact, so there are at most $|G|$ selections and a scan of all effect lists at each step gives polynomial time.

Suppose $0\le h(n)\le h^{\ast }(n)\le u(n)$ in a search problem, with $h^{\ast }=\infty$ at dead ends. Every finite $g(n)+u(n)$ bounds some reachable solution cost from above, so their running minimum $B$ is at least the global optimum $C^{\ast }$. Every node of an optimal path has $g+h\le C^{\ast }\le B$, and therefore survives the displayed strict pruning rule. Ordinary A-star search can continue to a selected goal without receiving a path witnessing $u$.

Equality pruning is unsafe without a stored incumbent solution: when $B=C^{\ast }$, it could delete every optimal continuation. A numerical upper bound does not by itself provide a plan to return. This distinguishes an upper-bound certificate from a constructed solution in branch and bound.

For an action sequence $\pi$, let $T_{\pi }(B)$ be the set of all physical states obtainable by applying it to the initial belief state $B$. Under a deterministic model this is an image; for nondeterministic outcomes it is the union of all permitted images. For $B^{\prime }\subseteq B$,If each action is applicable to every current possibility from $B$, it is also applicable to every possibility from $B^{\prime }$. If the final belief state for $B$ is contained in the physical goal set $G$, then $T_{\pi }(B^{\prime })\subseteq G$. Thus the same plan solves every subset of $B$.

Nothing comparable follows for an arbitrary superset. For example, let an action take $s_1$ to a goal and leave $s_2$ at a non-goal. It solves $\{s_1\}$ but not $\{s_1,s_2\}$. A larger belief state is solved by this particular sequence exactly when all added states also permit it and end in $G$. It may succeed on some supersets and fail on others; it cannot be guaranteed merely from success on $B$.

Use incremental belief-state search to find only the initial possibilities needed to constrain a successful plan. Choose one possible initial state, or a small subset $B_0$ of the full initial belief state $B$. Find an action sequence solving this restricted problem, then simulate it from every state in $B$.

If validation succeeds, return the candidate. Otherwise choose a state that makes some action inapplicable or ends outside the goal, add it to $B_0$, and search again for a plan that works for every selected state. Replanning can revise the earlier sequence; merely appending a repair to one arbitrary candidate can miss solutions. For a finite initial belief state, there are at most $|B|$ additions before every initial possibility has been included. If a complete restricted solver proves that even the selected subset is unsolvable, part (g) shows that the full problem is unsolvable.

The benefits are smaller intermediate belief states, fewer states propagated through candidate actions, and avoidance of unnecessary portions of the full power set search space. One physical-state counterexample can eliminate many invalid candidates. The worst case can still require all initial states; the method exploits instances where a few representative possibilities already force a plan that passes universal validation.

Let $G_1=\mathrm{On}(A,B)$ and $G_2=\mathrm{On}(B,C)$. The familiar obstruction is the Sussman anomaly for restricted goal-by-goal planning.

If one first constructs the obvious isolated plan for $G_1$, it moves $C$ off $A$ and then puts $A$ on $B$. Now $B$ is not clear, so achieving $G_2$ requires taking $A$ off $B$, undoing $G_1$. If one first achieves the isolated $G_2$ directly, it puts $B$ on $C$ while $C$ is still on $A$. To free $A$, it must move $C$, which first requires moving $B$ off $C$, undoing $G_2$. Therefore neither ordering of those independent subplans works while protecting the first achieved goal.

The literal concatenation-only definition in the question is too weak to imply the requested impossibility. A valid plan isThe first two actions constitute a plan for $G_2$ from the original state, and the last action is a plan for $G_1$ from the resulting state, preserving $G_2$. Thus this is itself a concatenation of the stated kind. Its crucial first action prepares for the later subgoal before completing $G_2$.

The green-outlined cells mark achieved goal facts. This original solution timeline makes the distinction explicit: independent goal-directed subplanning fails, but unrestricted concatenation does not. To obtain the intended impossibility claim, “non-interleaved” must also forbid anticipatory preparation or require the isolated subplans described above. No source input is missing; the issue is the breadth of the printed definition.

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.

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.

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.

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.

Use backward deletion of achieved goal requirements; this decides precondition-free ground STRIPS planning in polynomial time. Let $I$ be the initial set of true facts, $G$ the positive conjunctive goal set and $\mathcal{A}$ the ground actions. Assume the usual disjoint add and delete lists; if both lists contain a fact, first normalize the net effect according to the action semantics.

Maintain residual goal set $R=G$ and an initially empty list $L$. While $R⊈I$, look for an action $a$ satisfyingIf no such action exists, reject. Otherwise record $a$ in $L$ and replace $R$ by $R\setminus \mathrm{Add}(a)$. When $R\subseteq I$, return the actions in reverse order of recording. All actions are applicable because their precondition sets are empty.

For soundness, the selected action can be put last in a plan for the current residual goals: it supplies the removed goals and deletes none of the goals still being required. Reversing all recorded selections makes the final state satisfy the original $G$.

For completeness, suppose $R$ is not already satisfied initially but a plan achieves it. Consider the last action in that plan that changes any fact of $R$. Its effective changes cannot delete any member of $R$, because no later action repairs it; it must add at least one member. Thus a candidate exists. Moreover any candidate chosen by the algorithm is safe: removing some requirements gives a subset of $R$, so a plan for $R$, if one exists, also establishes the smaller goal set. Appending the chosen last action then restores the removed requirements without harming the rest. Mathematical induction therefore preserves solvability during all choices.

Each successful iteration removes at least one residual goal, so there are at most $|G|$ iterations and the returned plan has at most $|G|$ actions. Scanning all actions and their effect lists per iteration is polynomial in the input size, for example $O(|G||\mathcal{A}||P|)$ with simple fact-set representations over $P$. Merely taking the union of all add effects would be unsound, since actions can delete each other's achievements. This algorithm is the last-achiever algorithm for precondition-free planning.

In deterministic classical planning, a finite sequence of actions applicable successively from the initial state and ending in a state satisfying the goal. A STRIPS plan must respect every action's precondition set and both add and delete effects. A numerical bound on a possible plan's cost does not itself specify the action sequence.

The number of action layers allowed in a bounded automated planning encoding. Sequential layers permit at most one physical action, while a parallel semantics may permit several compatible actions. A sufficiently large horizon guarantees finding a solution only for a solvable input; shorter plans require idle layers or testing the successive smaller horizons.

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]

Sensorless planning chooses one action sequence that succeeds from every possible initial physical state without receiving distinguishing observations during execution. A belief state is a set of possibilities. For a deterministic search transition model $T$, an applicable action maps $B$ to $\{T(s,a):s\in B\}$; for nondeterministic outcomes, take the union of all possible successors. Applicability must hold for every member of $B$, and success requires the resulting belief state to be a subset of the physical goal set.

Every fixed action sequence preserves inclusion of the initial belief states. Consequently, a successful plan for $B$ also succeeds for every subset of $B$. Success on a superset is an additional requirement, so cannot be inferred from success on $B$ alone. This property supports incremental belief-state search.