# Propositional Planning

## Example

Block A is on block B which is on the table. Block C is
also on the table.
--------
| |
| A |
| |
-------- --------
| | | |
| B | | C |
TABLE | | | |
---------------------------------------------------------

Plan to achieve C on A and B on C.

## Time

Guess at a reasonable upper bound M on the number of steps you
will need in your plan. If no plan exists within your upper bound, increase
your estimate and try again. (The propositional method never gives you
the information that no plan of any length exists.)
## Propositional atoms

### Fluents

For each particular fluent and for each time within the
bounds, create a propositional atom assering that that fluent holds at that
time. In the example, there would be a fluent of the form ON-X-Y-T for each
pair of blocks (or block and table) X and Y and each time T; also a fluent
of the form CLEAR-X-T for each block X and time T. Thus ON-A-C-4
and CLEAR-B-3 are propositional atoms.
### Action occurrences.

For each particular action and each time,
create a propositional atom assering that the action is carried out beginning
at that time. In the example, create a propositional atom "PUTON-X-Y-T"
for each block X, block or table Y, and time T. Add a "WAIT" action with
no effects, in case you have overestimated the time needed for the plan.
## Axioms

Assert the following propositions:
### Start state

Describe the starting states in terms of fluents
at time 0. Example: ON-A-B-0, ON-B-TABLE-0, ON-C-TABLE-0, CLEAR-A-0,
CLEAR-C-0.
### Goal

Assert that the goal fluents hold at time M. Example:
if M=4, then assert ON-B-C-4, ON-A-B-4.
### Domain constraints

(i.e. constraints on fluents that hold at a given
time.) Each domain constraint must be stated as an axiom over all the
relevant fluents at all times. E.g. the definition of "Clear" in terms
of "On" leads to a whole collections of axioms such as
CLEAR-A-0 iff [not ON-B-A-0 and not ON-C-A-0]
CLEAR-B-3 iff [not ON-A-B-3 and not ON-C-B-3]

and so on.
The constraint that each block is other on exactly one other block or on
the table leads to axioms like
ON-A-B-3 or ON-A-C-3 or ON-A-TABLE-3.
not (ON-A-B-3 and ON-A-C-3)

and so on.
### Effect axioms

For each occurrence of each action, assert
that the effects of the axioms hold in the next state after the action.
E.g. For the action "puton" there would be axioms of the form
PUTON-A-B-2 implies ON-A-B-3

and so on.
### Frame axioms

For each fluent that is not affected by the action
add an axiom stating that it is the same at the end as at the beginning.
E.g.
PUTON-A-TABLE-3 implies [ON-C-TABLE-4 iff ON-C-TABLE-3].

### Precondition axioms

For each occurrence of each action,
assert that the preconditions for the actions (fluents) hold at the
beginning of the action. E.g.
PUTON-A-B-4 implies CLEAR-A-4 and CLEAR-B-4

Note: The action "WAIT" has no effects and no preconditions,
but has a frame axiom for each fluent.

### Exactly one action at a time.

For each time, assert that exactly one of the actions associated with that time
takes place. E.g.
PUTON-A-B-0 or PUTON-A-C-0 or PUTON-A-TABLE-0 or ... or PUTON-C-TABLE-0
or WAIT-0.
not (PUTON-A-B-0 and PUTON-A-C-0)

and so on.
That's it. Now give it to GSAT. Any valuation satisfying the axioms
is a valid plan.