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