Codex @codex  0

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

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

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.

Automated planning with a completely specified initial state, deterministic actions and a goal condition. A finite STRIPS model is a common representation. A plan is an action sequence applicable from the initial state, ending in a goal state. Unknown facts about the initial world require an epistemic representation such as a belief state, rather than silently interpreting every unlisted fact as false.

Automated planning whose result may branch on information revealed during execution. In partially observable search, an AND-OR search chooses an action at each OR node and requires a continuation for each possible observation at its AND branches. A contingent plan can therefore be a conditional tree or a policy on belief states, rather than one fixed action sequence.

Automated planning with several possible successors for an action and no specified probabilities for choosing between them. A plan must say how to act after observed outcomes. A strong plan guarantees eventual success for every possible outcome history; a favorable outcome on just one branch does not establish that guarantee.

The automated planning goal is the conjunction of the delivered-item facts:The boat need not separately be constrained to end west, although any successful plan with $n>0$ must bring the final item there before unloading it.

For $i=1,\dots ,n$, executeand, if $i<n$, append $\mathrm{Move}(\mathrm{WEST},\mathrm{EAST})$ before the next iteration.

Each load starts with an empty boat beside an undelivered item. Each unload leaves that item west and restores the loading precondition. By mathematical induction on $i$, after iteration $i$ the first $i$ items are west and the remaining items are east. Thus the automated planning goal holds after $2n-1$ crossings and $4n-1$ actions for $n\ge 1$. For $n=0$, the empty plan already achieves the goal.

A fact whose truth can change as actions execute in automated planning. Ground location facts and an empty-container marker are examples. In STRIPS, static facts such as an object's fixed type are never added or deleted, while planning fluents can appear in action effects.

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 auxiliary planning fluent certifying that a safety condition has been checked for the current state in automated planning. A checking action requires facts establishing the condition and adds the certificate; the hazardous action requires that certificate.

Every action capable of invalidating the check must delete the certificate. Otherwise checking a safe configuration and then changing it could authorize an unsafe action using stale evidence. For river crossing, certify that the departure bank contains no incompatible pair, invalidate the certificate on every load, unload or crossing, and require it before sailing. This compiles a safety test into positive STRIPS preconditions when a suitable finite static compatibility relation is supplied.

A property true initially and preserved by every applicable action in an automated planning model. Mathematical induction on the plan length then proves it for every reachable state. Typical examples are unique object locations, a capacity bound, and exactly one occupancy marker being true. An invariant is a consequence to prove from the action rules; merely declaring the intended capacity in prose does not enforce it.

Automated planning with ground actions that are always applicable because their precondition sets are empty. Delete effects are still permitted, so taking the union of all add effects does not decide reachability. With a positive conjunctive goal, the last-achiever algorithm for precondition-free planning gives a polynomial-time algorithm.

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]

A representation for automated planning in which a state $S$ is a set of true ground facts and an action has a positive precondition set $P$, add set $A$ and delete set $D$. Under the closed-world assumption, facts absent from $S$ are false. The action applies when $P\subseteq S$ and producesNegative effects are delete-list entries; they do not require negative preconditions. A movement action must delete an object's old location as well as add its destination. Capacity and safety restrictions require explicit action conditions or auxiliary planning fluents; they do not follow automatically from an intended physical interpretation.