Read the satisfying assignment in increasing time order. In layer , 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 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 , assign each layer its actual fluent values and pad with idle layers. These values satisfy every component of . In this instance, decoding the three-action trajectory in part (d) gives a model at and at every larger horizon after padding; direct state-space and propositional checks find no model for .
Articles by others on the same topic
There are currently no matching articles.