= Solution
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 \b[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 $\varphi_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$.
Back to article page
