frame a  ioms that say when facts retain their truth values  schema      .

i,t -> 1 t 0  t+1  t or operators
n' The frame a  iom says  that if literal   is false at   and true at   +  , then one of the operators m that make   true is e ecuted at  .

f we allow the e ecution of several operators simultaneously, we need formulae that state that two operators are not e  ecuted at the same time if they are dependent; that is, if a propositional variable in the postcondition of one occurs in the precondition of the other.

f no parallelism is allowed, we have formulae and for rrrr 5 o such that   ≠  .

all The si e of the set of formulae obtained from schemata . . and . is of the order F 
re a s '
Example 4.1 n the blocks world e ample, the formulae describing the preconditions and the postconditions of the operators are the following for 0 2 o t → onAB t clearA t contableA t +1 onAB t +1 clearB t +1 1 t → onBA t clearB t contableB t+1 onBA t+1 clearA t+1 2,t → ontableAt clearBt onABt+1    clearBt+1     ontableAt+1 3,t → ontableBt clearAt onBAt+1    clearAt+1    ontableBt+1 The frame a  ioms are as follows for 0 on A Be on A Be+1 onBAt+1 l t onABt onBAt      onBAt+1       3,t onta ble At l , t ontableAt ontableAt+1 3, t clearAf     clearAf+1 clearAt  clearAt+1 3, t clearBe+1 clearBe   clearBe+1 2, t The simultaneous application of two operators is not allowed, which is represented by the following formulae for all 0

$${\dot{i}},t$$

$$j,t$$

□
To represent classical planning as a satisfiability problem, as proposed by aut and elman
, in addition to the above formulae it su ces to give a set of literals that describe an initial state and a formula that describes the goals. Then a satisfiability algorithm can be used for finding a truth value assignment that satisfies the propositional formulae. The truth values for propositional variables should be applied to reach the goals.