SATPlan

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

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

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.