# SAT-based Planning and an efficient encoding of the blocks world

### Time points

Fix a maximum number of time points to consider 0 ... N.
### Propositional atoms:

### Fluent atoms:

For each Boolean fluent F and each time T, create an atom F_T (F holds
at time T).
** Blocks world: **

For each time T, block B, and object O (an "object" is
either a block or TABLE), create an atom ON_B_O_T.

### Action atoms

For each action A, for each time T < N, create an atom A_T
(action A occurs at time T). (Assume the first action occurs at time 0.)
** Blocks world **

For each time T, block B, and object O != B.
create an atom MOVE_B_O_T. (Move block B to object O at time T.)

### Causal axioms

If action A causes fluent F to become true, assert the axiom
A_T => F_(T+1) at each time T < N.

If action A causes fluent F to become false, assert the axiom
A_T => ~F_(T+1) at each time T < N.

** Blocks world **

For each time T, block B, and object O != B,
assert the axiom: MOVE_B_O_T => ON_B_O_(T+1)

### Preconditions

If action A has precondition F, then assert the axiom A_T => F_T.
** Blocks world **

For each time T, blocks B1 and B2, object O !=B1, assert the axiom:

MOVE_B1_O_T => ~ON_B2_B1_T

If O != TABLE, then assert the axiom
MOVE_B1_O_T => ~ON_B2_O_T.

### Domain constraints

Domain constraints are constraints that hold among fluents at some
particular time. Assert these at each time point.
** Blocks world **

For each time T, block B, and objects O1 != O2, assert the axiom:
~(ON_B_O1_T ^ ON_B_O2_T).

(A block is on at most one object.)

For each time T and block B assert the axiom:
ON_B_O1_T V ... V ON_B_Ok_T, where O1 ... Ok ranges over all
the objects except B.

(A block is on at least one object.)

### Frame axioms: Explanation closure

For each fluent F, let A1 ... Ak be the actions that can cause
F to become true, and let B1 ... Bm be the actions that can cause
F to become false. Assert the axioms

(F_(T+1) ^ ~F_(T)) => (A1 V A2 V ... V Ak)

(~F_(T+1) ^ F_(T)) => (B1 V B2 V ... V Bm)
** Blocks world **

For each time T, block B, object O1, assert the axiom:

[ON_B_O1_{T+1} ^ ~ON_B_O1_T] => MOVE_B_O1__T.

### At most one action at a time.

For each pair of actions A1, A2 for each time T, assert
~(A1_T ^ A2_T).
** Blocks world **

For each time T,
for each block B1, object O1 != B1, block B2, object O2 != B2, where
not (B1=B2 and O1=O2) assert:

~(MOVE_B1_O1_T ^ MOVE_B2_O2_T).