Programming SATPlan Greg Sullivan 16410/16413 October 22, 2003
Programming SATPlan Greg Sullivan 16.410/16.413 October 22, 2003
Outline SATPlan Programming TrickS · Programming SATPlan c.222003 16.410/13, Programming SATPlan, Greg Sullivan
Outline • SATPlan • Programming Tricks • Programming SATPlan Oct. 22, 2003 16.410/13, Programming SATPlan, Greg Sullivan 2
History · Kautz and selman.1992 Inspired by improvements in satisfiabilty algorithms Bia idea Encode planning problem as a(very large) logical formula Initial-state& all-possible-actions goal Find a satisfying assignment to action-time propositions, and we have a plan 16.410/13, Programming SATPlan, Greg Sullivan
History • Kautz and Selman, 1992 • Inspired by improvements in satisfiabity algorithms Big Idea • Encode planning problem as a (very large) logical formula. • Initial-state & all-possible-actions & goal • Find a satisfying assignment to action-time propositions, and we have a plan. Oct. 22, 2003 16.410/13, Programming SATPlan, Greg Sullivan 3
A Planning Problem ((domains (cargo cl c2)(airport sfo jfk)(plane pl p2)) predicates (cargo-at cargo airport) (plane-at pla (in cargo plane)) (plane-at pl sfo)(plane-at p2 jfk) dded(could be derived not (cargo-at cl jfk))(not (cargo-at c2 sfo)) (not (plane-at pl jfk))(not (plane-at p2 sfo))) (goal (cargo-at cl jfk)(cargo-at c2 sfo)) action (load (c cargo)(p plane)(a airport)) ((cargo-at c a)(plane -at p a))i preconditions ((not (cargo-at c a))(inc p)))i postconditions (action (unload (c cargo)(p plane)(a airport) ((in c p)(plane-at p a)) ((cargo-at c a)(not (in c p))) (action (fly(p plane)(from airport)(to airport)) (oplane-at p from)) ((not (plane-at p from))(plane-at p to))) Note that this is plain ol Scheme c.222003 16.410/13, Programming SATPlan, Greg Sullivan
A Planning Problem (define air-cargo-problem '((domains (cargo c1 c2) (airport sfo jfk) (plane p1 p2)) (predicates (cargo-at cargo airport) (plane-at plane airport) (in cargo plane)) (init (cargo-at c1 sfo) (cargo-at c2 jfk) (plane-at p1 sfo) (plane-at p2 jfk) ;; added (could be derived) (not (cargo-at c1 jfk)) (not (cargo-at c2 sfo)) (not (plane-at p1 jfk)) (not (plane-at p2 sfo))) (goal (cargo-at c1 jfk) (cargo-at c2 sfo)) (action (load (c cargo) (p plane) (a airport)) ((cargo-at c a) (plane-at p a)) ; preconditions ((not (cargo-at c a)) (in c p))) ; postconditions (action (unload (c cargo) (p plane) (a airport)) ((in c p) (plane-at p a)) ((cargo-at c a) (not (in c p)))) (action (fly (p plane) (from airport) (to airport)) ((plane-at p from)) ((not (plane-at p from)) (plane-at p to))) )) Note that this is plain ol’ Scheme Oct. 22, 2003 16.410/13, Programming SATPlan, Greg Sullivan 4
Encoding Initial State init (cargo-at c1 sfo)(cargo-at c2 jfk) (plane-at p1 sfo)(plane-at p2 jfk) Encoding the g; added (could be derived) Goal state not(cargo-at c1 jfk )(not( cargo-at c2 sfol)) (not (plane-at pl jfk))(not (plane-at p2 sfo) Same thing (and (1 cargo-at cl sfo)(1 cargo-at c2 jfk) (not (1 cargo-at cl jfk)).) Remember: We're dealing with Propositional logic WFF∷A|(notA)( and wfe…)l(orWF What are our literals(A)? lists: (t predicate-name literal ..(t action-name literal 16.410/13, Programming SATPlan, Greg Sullivan
Encoding Initial State (init (cargo-at c1 sfo) (cargo-at c2 jfk) (plane-at p1 sfo) (plane-at p2 jfk) ;; added (could be derived) (not (cargo-at c1 jfk)) (not (cargo-at c2 sfo)) (not (plane-at p1 jfk)) (not (plane-at p2 sfo))) Encoding the Goal State Same thing (and (1 cargo-at c1 sfo) (1 cargo-at c2 jfk) … (not (1 cargo-at c1 jfk)) … ) • Remember: We’re dealing with Propositional logic: • WFF ::= A | (not A) (and WFF …) | (or WFF …) • What are our literals (A)? • lists: (t predicate-name literal …) (t action-name literal …) Oct. 22, 2003 16.410/13, Programming SATPlan, Greg Sullivan 5