Compilation to SAT

Init: At-R-E-0 & At-A-E-0 & At-B-E-0

Goal: In-A-1 & In-B-1

Graph: “cond at k => one of the supporting actions at k-1”

In-A-1 => Load-A-1 In-B-1 => Load-B-1

At-R-M-1 => Fly-R-1 At-R-E-1 => P-At-R-E-1

Load-A-1 => At-R-E-0 & At-A-E-0 “Actions => preconds”

Load-B-1 => At-R-E-0 & At-B-E-0

P-At-R-E-1 => At-R-E-0h

~In-A-1 V ~ At-R-M-1 ~In-B-1 V ~At-R-M-1 “Mutexes”

Suppose we want to find a plan

that satisfies In(A) & In(B)