UMD CMSC 722 - Chapter 7 Propositional Satisfiability Techniques

Unformatted text preview:

Dana Nau: Lecture slides for Automated Planning Licensed under the Creative Commons Attribution-NonCommercial-ShareAlike License: http://creativecommons.org/licenses/by-nc-sa/2.0/ 1 Chapter 7 Propositional Satisfiability Techniques Dana S. Nau University of Maryland 12:58 PM February 15, 2012 Lecture slides for Automated Planning: Theory and PracticeDana Nau: Lecture slides for Automated Planning Licensed under the Creative Commons Attribution-NonCommercial-ShareAlike License: http://creativecommons.org/licenses/by-nc-sa/2.0/ 2 Motivation ● 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 Planning Licensed under the Creative Commons Attribution-NonCommercial-ShareAlike License: http://creativecommons.org/licenses/by-nc-sa/2.0/ 3 Outline ● 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 Planning Licensed under the Creative Commons Attribution-NonCommercial-ShareAlike License: http://creativecommons.org/licenses/by-nc-sa/2.0/ 4 Overall 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 Planning Licensed under the Creative Commons Attribution-NonCommercial-ShareAlike License: http://creativecommons.org/licenses/by-nc-sa/2.0/ 5 Notation ● 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 Planning Licensed under the Creative Commons Attribution-NonCommercial-ShareAlike License: http://creativecommons.org/licenses/by-nc-sa/2.0/ 6 Fluents ● 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 Planning Licensed under the Creative Commons Attribution-NonCommercial-ShareAlike License: http://creativecommons.org/licenses/by-nc-sa/2.0/ 7 Encoding 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 Planning Licensed under the Creative Commons Attribution-NonCommercial-ShareAlike License: http://creativecommons.org/licenses/by-nc-sa/2.0/ 8 Formulas 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 Planning Licensed under the Creative Commons Attribution-NonCommercial-ShareAlike License: http://creativecommons.org/licenses/by-nc-sa/2.0/ 9 Frame Axioms 5. Frame axioms: ◆ Formulas describing what doesn’t change between 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 Planning Licensed under the Creative Commons Attribution-NonCommercial-ShareAlike License: http://creativecommons.org/licenses/by-nc-sa/2.0/ 10 Example ● 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 = 1 1. 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


View Full Document
Download Chapter 7 Propositional Satisfiability Techniques
Our administrator received your request to download this document. We will send you the file to your email shortly.
Loading Unlocking...
Login

Join to view Chapter 7 Propositional Satisfiability Techniques and access 3M+ class-specific study document.

or
We will never post anything without your permission.
Don't have an account?
Sign Up

Join to view Chapter 7 Propositional Satisfiability Techniques 2 2 and access 3M+ class-specific study document.

or

By creating an account you agree to our Privacy Policy and Terms Of Use

Already a member?