SAT Encodings
Propositional CNF: no variables or quantifiers
Sets of clauses specified by axiom schemas
fully instantiated before problem-solving
Discrete time, modeled by integers
state predicates: indexed by time at which they hold
action predicates: indexed by time at which action begins
each action takes 1 time step
many actions may occur at the same step
fly(Plane, City1, City2, i) É at(Plane, City2, i +1)