= Sequential SATPlan correctness
{title2=$\varphi_T\text{ satisfiable}\iff\text{a plan of length at most }T\text{ exists}$}
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>.
Back to article page
