麻省理工学院：《自制决策制造原则》英文版 Programming SATPlan

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

Time To find the shortest plan, look for a plan at timestep 1, then 2,etc c.222003 16.410/13, Programming SATPlan, Greg Sullivan

Time • To find the shortest plan, look for a plan at timestep 1, then 2, etc. Oct. 22, 2003 16.410/13, Programming SATPlan, Greg Sullivan 6

Encoding Actions (action(fly(p plane)(from airport)(to airport) ((plane-at p from) ((not (plane-at p from)(plane-at p to) Base encoding on successor state axioms presented in r&n ch ch 7 for the situation calculus 16.410/13, Programming SATPlan, Greg Sullivan

Encoding Actions (action (fly (p plane) (from airport) (to airport)) ((plane-at p from)) ((not (plane-at p from)) (plane-at p to))) • Base encoding on successor state axioms presented in R&N ch. 7, for the situation calculus. Oct. 22, 2003 16.410/13, Programming SATPlan, Greg Sullivan 7

Actions Successor state axioms in words P is true at time t+1 if either of the following is true 1. For some action that establishes p(has p as a postcondition) a. all of P's preconditions are satisfied at time t b. the action was taken at time t 2. Or, p was true at time t, and whatever action that was taken at time t doesn ' t undo p c.222003 16.410/13, Programming SATPlan, Greg Su

Actions Successor State axioms in words: P is true at time t+1 if either of the following is true: 1. For some action that establishes P (has P as a postcondition), a. all of P’s preconditions are satisfied at time t b. The action was taken at time t. 2. Or, P was true at time t, and whatever action that was taken at time t doesn’t undo P. Oct. 22, 2003 16.410/13, Programming SATPlan, Greg Sullivan 8

Example Successor State Axiom (iff (2 plane-at pl jfk or (and (1 plane-at pl sfo)(1 fly pl sfo jfk)) (and (1 plane-at p1 jfk) (not (1 fly pl jfk sfo)))) Reminder Lists like (2 plane-at p1 jfk) are considered literals. It should be considered the same as a variable named 2-plane-at-p1-jfk, which is entirely different from the variable named 1-plane-at-p1-jtk 16.410/13, Programming SATPlan, Greg Sullivan

Example Successor State Axiom (iff (2 plane-at p1 jfk) (or (and (1 plane-at p1 sfo) (1 fly p1 sfo jfk)) (and (1 plane-at p1 jfk) (not (1 fly p1 jfk sfo))))) Reminder • Lists like (2 plane-at p1 jfk) are considered literals. It should be considered the same as a variable named 2-plane-at-p1-jfk, which is entirely different from the variable named 1-plane-at-p1-jfk. Oct. 22, 2003 16.410/13, Programming SATPlan, Greg Sullivan 9

Problem Successor state axioms do not rule out ridiculous plans such as (1 fly p1 sfo jfk) &(1 fly p1 jfk sfo) · The plan is a model Need precondition axioms 0ct.222003 16.410/13, Programming SATPlan, Greg Sullivan

Problem • Successor state axioms do not rule out ridiculous plans such as: (1 fly p1 sfo jfk) & (1 fly p1 jfk sfo) • The plan is a model • Need precondition axioms. Oct. 22, 2003 16.410/13, Programming SATPlan, Greg Sullivan 10