Programming SATPlan Greg Sullivan 16.410/16.413 October 22, 2003 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 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 (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) ;; 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. 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. 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. Oct. 22, 2003 16.410/13, Programming SATPlan, Greg Sullivan 8 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. Oct. 22, 2003 16.410/13, Programming SATPlan, Greg Sullivan 10 Precondition Axioms ? (t action) ? (t action-precondition) ? Ex: (implies (1 fly p1 jfk sfo) (1 plane-at jfk)) Oct. 22, 2003 16.410/13, Programming SATPlan, Greg Sullivan 11 Still Problems ? Still allow plans such as: (1 fly p1 sfo jfk) and (1 fly p1 sfo lax) ? Need action exclusion axioms to prevent simultaneous actions. – To allow partial ordering, only rule out simultaneous actions that interfere. Oct. 22, 2003 16.410/13, Programming SATPlan, Greg Sullivan 12 Action Exclusion Axioms ? Ex: (not (and (1 fly p1 jfk sfo) (1 fly p1 jfk lax))) ? We only allow not on simple propositions, so we change this to be: (and (implies (1 fly p1 jfk sfo) (not (1 fly p1 jfk lax))) (implies (1 fly p1 jfk lax) (not (1 fly p1 jfk sfo))) … ) Oct. 22, 2003 16.410/13, Programming SATPlan, Greg Sullivan 13 Generating Initial Axioms (define (problem-initial-propositions problem) (cdr (assq 'init problem))) That was easy! Oct. 22, 2003 16.410/13, Programming SATPlan, Greg Sullivan 14 Generating Precondition Axioms For each timestep 1 in [1… max_t] For every action ((act x_1 … x_n) (pre_1 …) (post_1 …)) For every n-tuple <a,b,…> subst = [a/x_1, b/x_2, …] For every precondition pre_i (implies (t act a b …) (t (do-subst subst pre_i))) Oct. 22, 2003 16.410/13, Programming SATPlan, Greg Sullivan 15 Code for precondition axioms (define (problem-precondition-axioms problem max-timesteps) (fold (lambda (t axioms) ; for each time t (fold (lambda (action axioms) ; for each action (fold (lambda (arg-tuple axioms) ; for each arg-tuple (let ((subst (make-subst arg-tuple (action-args action)))) (fold (lambda (precond axioms) ; for each precondition (cons (list 'implies (cons t (cons (action-act action) arg-tuple)) (cons t (do-subst subst precond))) axioms)) axioms (action-preconditions action)))) axioms (value-tuples (action-domains action problem)))) axioms (problem-actions problem))) '() (ints-from-to 1 max-timesteps)))) Oct. 22, 2003 16.410/13, Programming SATPlan, Greg Sullivan 16 What’s fold again? (define (fold kons knil l) (let loop ((l l) (out knil)) (if (null? l) out (loop (cdr l) (kons (car l)) out)))) Why “kons”? Oct. 22, 2003 16.410/13, Programming SATPlan, Greg Sullivan 17 Actually, ;; kons must be a function expecting n+1 args, ;; where the n is the number ;; of lists, and the 1st n args are the next ;; elements from each list, and ;; the n+1st element is the current result ;; For a single list, returns ;; (kons en ... (kons e2 (kons e1 knil))) (define (fold kons knil . lists) (let loop ((lists lists) (out knil)) (if (any? null? lists) out (loop (map cdr lists) (apply kons (append (map car lists) (list out))))))) Oct. 22, 2003 16.410/13, Programming SATPlan, Greg Sullivan 18 Using fold ? 1 ]=> (fold cons '() '(a b c)) ;Value 13: (c b a) ? 1 ]=> (fold + 0 '(1 2 3)) ;Value: 6 ? 1 ]=> (fold (lambda (n max) (if (> n max) n max)) 0 '( 2 1 5 2 9 3)) ;Value: 9 ? 1 ]=> (define (mymap f l) (fold cons '() (fold (lambda (e l1) (cons (f e) l1)) '() l))) ? 1 ]=> (mymap (lambda (x) (+ 1 x)) '(1 2 3)) ;Value 14: (2 3 4) ? (fold (lambda (x y l) (cons (list x y) l)) '() '(1 2 3) '(one two three)) ;Value 15: ((3 three) (2 two) (1 one)) Oct. 22, 2003 16.410/13, Programming SATPlan, Greg Sullivan 19 Nested folds (fold (lambda (arg1 out) ; for each possible arg1 (fold (lambda (arg2 out) ; for each possible arg2 (fold (lambda (arg3 out) ; for each possible arg3 (cons (list arg1 arg2 arg3) out)) out '(arg3-1 arg3-2))) out '(arg2-1 arg2-2))) '() '(arg1-1 arg1-2)) ((arg1-2 arg2-2 arg3-2) (arg1-2 arg2-2 arg3-1) (arg1-2 arg2-1 arg3-2) (arg1-2 arg2-1 arg3-1) (arg1-1 arg2-2 arg3-2) (arg1-1 arg2-2 arg3-1) (arg1-1 arg2-1 arg3-2) (arg1-1 arg2-1 arg3-1)) Oct. 22, 2003 16.410/13, Programming SATPlan, Greg Sullivan 20 Action Exclusion Axioms for each action ((act x_1 … x_n) (pre_1 …) (post_1 …)) for each n-tuple <a,b,…>, subst = [a/x_1, b/x_2, …] for each action ((act’ x’_1 … x’_m) (pre’_1 …) (post’_1 …)) for each m-tuple <a’,b’,…>, subst’ = [a’/x’_1, b’/x’_2, …] if exists <i,j,k,l> with (pre_i, pre’_j, post_k, post’_l) s.t. (or (negates (subst post_k) (subst’ pre_k)) (negates (subst’ post’_l) (subst pre_i)) (negates (subst’ post’_l) (subst post_k)) for each time t in [t … max_t] [1] (implies (t act a b …) (not (t act’ a’ b’ …))) [2] (implies (t act’ a’ b’ …) (not (t act a b …)) Your homework: (define (problem-action-exclusion-axioms problem max_timesteps)) Oct. 22, 2003 16.410/13, Programming SATPlan, Greg Sullivan 21 Complexity of Encoding ? Action exclusion axioms: – a actions, arity n, domain size d –ad n d n Oct. 22, 2003 16.410/13, Programming SATPlan, Greg Sullivan 22 Successor State Axioms For each timestep t in t … t_max for each predicate pred with arity n for every n-tuple <a,b, …> collect doers = (action subst) pairs for every action ((act x_1 … x_m)(pre_1 …)(post_1 …)) for every m-tuple <a’,b’,…>, subst = [a’/x_1, …] if some (subst post_i) = (pred a b …) doers += (action subst) collect undoers similarly, looking for (subst post_i) = (not (pred a b …)) then (iff (t+1 pred a b …) (or ;; preconds satisfied and did action with post = (pred a b …) (or for each (action subst) in doers (and (subst pre_1) … (subst act x_1 …))( ;; (pred a b …) already true at t, and didn’t undo it (and (t pred a b …) for each (action subst) in undoers (not (t (subst act x_1 …)))))) Oct. 22, 2003 16.410/13, Programming SATPlan, Greg Sullivan 23 How to use DPLL? ? Need to convert to Conjunctive Normal Form. ? P. 215 in R&N 1. Eliminate ? 2. Eliminate ? (implies A B) = (or (not A) B) 3. More not inwards 4. Distribute or over and Oct. 22, 2003 16.410/13, Programming SATPlan, Greg Sullivan 24