Chapter 7 Propositional Satisfiability TechniquesMotivationOutlineOverall ApproachNotationFluentsEncoding Planning ProblemsFormulas in Frame AxiomsExampleExample (continued)Slide 12Summary of the ExampleExtracting a PlanPlanningThe Davis-Putnam ProcedureLocal SearchGSATDiscussionSatPlanOther Translation ApproachesDana Nau: Lecture slides for Automated PlanningLicensed under the Creative Commons Attribution-NonCommercial-ShareAlike License: http://creativecommons.org/licenses/by-nc-sa/2.0/1Chapter 7Propositional Satisfiability TechniquesDana S. NauUniversity of Maryland10:28 AM January 14, 2019Lecture slides forAutomated Planning: Theory and PracticeDana Nau: Lecture slides for Automated PlanningLicensed under the Creative Commons Attribution-NonCommercial-ShareAlike License: http://creativecommons.org/licenses/by-nc-sa/2.0/2MotivationPropositional satisfiability: given a boolean formula»e.g., (P  Q)  ( Q  R  S)  ( R  P), does there exist a model»i.e., an assignment of truth values to the propositions that makes the formula true?This was the very first problem shown to be NP-completeLots of research on algorithms for solving itAlgorithms are known for solving all but a small subset in average-case polynomial timeTherefore,Try translating classical planning problems into satisfiability problems, and solving them that wayDana Nau: Lecture slides for Automated PlanningLicensed under the Creative Commons Attribution-NonCommercial-ShareAlike License: http://creativecommons.org/licenses/by-nc-sa/2.0/3OutlineEncoding planning problems as satisfiability problemsExtracting plans from truth valuesSatisfiability algorithmsDavis-PutnamLocal searchGSATCombining satisfiability with planning graphsSatPlanDana Nau: Lecture slides for Automated PlanningLicensed under the Creative Commons Attribution-NonCommercial-ShareAlike License: http://creativecommons.org/licenses/by-nc-sa/2.0/4Overall ApproachA bounded planning problem is a pair (P,n):P is a planning problem; n is a positive integerAny solution for P of length n is a solution for (P,n)Planning algorithm:Do iterative deepening like we did with Graphplan: for n = 0, 1, 2, …,»encode (P,n) as a satisfiability problem  »if  is satisfiable, then•From the set of truth values that satisfies , a solution plan can be constructed, so return it and exitDana Nau: Lecture slides for Automated PlanningLicensed under the Creative Commons Attribution-NonCommercial-ShareAlike License: http://creativecommons.org/licenses/by-nc-sa/2.0/5NotationFor satisfiability problems we need to use propositional logicNeed to encode ground atoms into propositionsFor set-theoretic planning we encoded atoms into propositions by rewriting them as shown here:»Atom: at(r1,loc1)»Proposition: at-r1-loc1For planning as satisfiability we’ll do the same thingBut we won’t bother to do a syntactic rewriteJust use at(r1,loc1) itself as the propositionAlso, we’ll write plans starting at a0 rather than a1π = a0, a1, …, an–1Dana Nau: Lecture slides for Automated PlanningLicensed under the Creative Commons Attribution-NonCommercial-ShareAlike License: http://creativecommons.org/licenses/by-nc-sa/2.0/6FluentsIf π = a0, a1, …, an–1 is a solution for (P,n), it generates these states:s0, s1 =  (s0,a0), s2 =  (s1,a1), …, sn =  (sn–1, an–1)Fluent: proposition saying a particular atom is true in a particular stateat(r1,loc1,i) is a fluent that’s true iff at(r1,loc1) is in si We’ll use li to denote the fluent for literal l in state si»e.g., if l = at(r1,loc1) then li = at(r1,loc1,i) ai is a fluent saying that a is the i’th step of π»e.g., if a = move(r1,loc2,loc1) then ai = move(r1,loc2,loc1,i)Dana Nau: Lecture slides for Automated PlanningLicensed under the Creative Commons Attribution-NonCommercial-ShareAlike License: http://creativecommons.org/licenses/by-nc-sa/2.0/7Encoding Planning ProblemsEncode (P,n) as a formula  such thatπ = a0, a1, …, an–1 is a solution for (P,n) if and only if can be satisfied in a way that makes the fluents a0, …, an–1 trueLetA = {all actions in the planning domain}S = {all states in the planning domain}L = {all literals in the language}  is the conjunct of many other formulas …Dana Nau: Lecture slides for Automated PlanningLicensed under the Creative Commons Attribution-NonCommercial-ShareAlike License: http://creativecommons.org/licenses/by-nc-sa/2.0/8Formulas in 1. Formula describing the initial state: /\{l0 | l  s0}  /\{l0 | l  L – s0 }2. Formula describing the goal: /\{ln | l  g+}  /\{ln | l  g–}3. For every action a in A and for i = 1, …, n, a formula describing what changes a would make if it were the i’th step of the plan: ai  /\{pi | p  Precond(a)}  /\ {ei+1 | e  Effects(a)}4. Complete exclusion axiom:For every pair of actions a and b, and for i = 0, …, n–1, a formula saying they can’t both be the i’th step of the plan  ai   bithis guarantees there can be only one action at a timeIs this enough?Dana Nau: Lecture slides for Automated PlanningLicensed under the Creative Commons Attribution-NonCommercial-ShareAlike License: http://creativecommons.org/licenses/by-nc-sa/2.0/9Frame Axioms5. Frame axioms:Formulas describing what doesn’t changebetween steps i and i+1Several ways to write theseOne way: explanatory frame axiomsFor i = 0, …, n–1, an axiom for every literal l»Says that if l changes between si and si+1, then the action at step i must be responsible: (li  li+1  Va in A{ai | l  effects+(a)})  (li  li+1  Va in A{ai | l  effects–(a)})Dana Nau: Lecture slides for Automated PlanningLicensed under the Creative Commons Attribution-NonCommercial-ShareAlike License: http://creativecommons.org/licenses/by-nc-sa/2.0/10ExamplePlanning domain:one robot r1two adjacent locations l1, l2one planning operator (to move the robot from one location to another)Encode (P,n) where n = 11. Initial state: {at(r1,l1)}Encoding: at(r1,l1,0)  at(r1,l2,0)2. Goal: {at(r1,l2)}Encoding: at(r1,l2,1)  at(r1,l1,1)3. Operator: see next slideDana Nau: Lecture slides for Automated PlanningLicensed under the Creative Commons