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