PowerPoint PresentationPlanning as SatisfiabilityArchitecture of a SAT-based PlannerPropositional LogicPropositional Logic: CNFPropositional logic: SemanticsPropositional SatisfiabilitySlide 8Complexity of Planning RevisitedEncoding Planning as Satisfiability: Basic IdeaOverall ApproachExample of Complete Formula for (P,1)Fluents (will be used as propositons)Pictorial View of FluentsEncoding Planning ProblemsFormulas in Slide 17Frame AxiomsExampleExample (continued)Slide 21Complete Formula for (P,1)Extracting a PlanSupporting Layered PlansSAT AlgorithmsDPLL [Davis, Putnam, Loveland & Logemann 1962]Basic ObservationsDPLL Davis – Putnam – Loveland – LogemannWalkSatPlanning Benchmark Test SetScaling Up Logistics PlanningWhat SATPLAN ShowsDiscussionBlackBox (GraphPlan + SatPlan)BlackboxTranslation of Plan GraphBlackbox ResultsSlide 381Planning as SatisfiabilityAlan Fern ** Based in part on slides by Stuart Russell and Dana NauReview of propositional logic (see chapter 7)Planning as propositional satisfiabilitySatisfiability techniques (see chapter 7)Combining satisfiability techniques with planning graphs2Planning as SatisfiabilityThe “planning as satisfiability” framework lead to large improvements when it was first introducedEspecially in the area of optimal planningAt that time there was much recent progress in satisfiability solversThis work was an attempt to leverage that work by reducing planning to satisfiabilityPlanners in this framework are still very competitive in terms of optimal planning3Architecture of a SAT-based PlannerCompiler(encoding)satisfyingmodelPlanIncrement plan lengthIf unsatisfiablePlanning Problem • Init State• Goal• ActionsCNFSimplifier(polynomial inference)Solver(SAT engine/s)DecoderCNFPropositional formula in conjunctive normal form (CNF)4Propositional LogicWe use logic as a formal representation for knowledgePropositional logic is the simplest logic – illustrates basic ideasSyntax:We are given a set of primitive propositions {P1, …, Pn}These are the basic statements we can make about the “world”From basic propositions we can construct formulasA primitive proposition is a formulaIf F is a formula, F is a formula (negation)If F1 and F2 are formulas, F1  F2 is a formula (conjunction)If F1 and F2 are formulas, F1  F2 is a formula (disjunction)If F1 and F2 are formula s, F1  F2 is a formula (implication)If F1 and F2 are formulas, F1  F2 is a formula (biconditional)Really all we need is negation and disjunction or conjunction, but the other connectives are useful shorthandE.g. F1  F2 is equivalent to F1  F25Propositional Logic: CNFA literal is either a proposition or the negation of a propositionA clause is a disjunction of literalsA formula is in conjunctive normal form (CNF) if it is the conjunction of clauses(R  P  Q)  (P  Q)  (P  R)Any formula can be represented in conjunctive normal form (CNF)Though sometimes there may be an exponential blowup in size of CNF encoding compared to original formulaCNF is used as a canonical representation of formulas in many algorithms6Propositional logic: Semantics• A truth assignment is an assignment of true or false to each proposition: e.g. p1 = false, p2 = true, p3 = false• A formula is either true or false wrt a truth assignment• The truth of a formula is evaluated recursively as given below: (P and Q are formulas)The base case is when the formulas are single propositionswhere the truth is given by the truth assignment.7Propositional SatisfiabilityA formula is satisfiable if it is true for some truth assignmente.g. A B, CA formula is unsatisfiable if it is never true for any truth assignmente.g. A ATesting satisfiability of CNF formulas is a famous NP-complete problem8Propositional SatisfiabilityMany problems (such as planning) can be naturally encoded as instances of satisfiabilityThus there has been much work on developing powerful satisfiability solvers these solvers work amazingly well in practice9Complexity of Planning RevisitedRecall that PlanSAT for propositional STRIPS is PSPACE-complete(Chapman 1987; Bylander 1991; Backstrom 1993, Erol et al. 1994)How then it is possible to encode STRIPS planning as SAT, which is only an NP-complete problem?Bounded PlanSAT is NP-complete(Chenoweth 1991; Gupta and Nau 1992)So bounded PlanSAT can be encoded as propositional satisfiabilityBounded PlanSAT Given: a STRIPS planning problem, and positive integer n Output: “yes” if problem is solvable in n steps or less, otherwise “no”10Encoding Planning as Satisfiability: Basic IdeaBounded planning problem (P,n):P is a planning problem; n is a positive integerFind a solution for P of length nCreate a propositional formula that represents:Initial stateGoal Action Dynamics for n time stepsWe will define the formula for (P,n) such that: 1) any satisfying truth assignment of the formula represent a solution to (P,n) 2) if (P,n) has a solution then the formula is satisfiable11Overall Approach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 exitWith a complete satisfiability tester, this approach will produce optimal layered plans for solvable problemsWe can use a GraphPlan analysis to determine an upper bound on n, giving a way to detect unsolvability12Example of Complete Formula for (P,1)[ at(r1,l1,0)  at(r1,l2,0) ] at(r1,l2,1) [ move(r1,l1,l2,0)  at(r1,l1,0) ]  [ move(r1,l1,l2,0)  at(r1,l2,1) ] [ move(r1,l1,l2,0)  at(r1,l1,1) ] [ move(r1,l2,l1,0)  at(r1,l2,0) ] [ move(r1,l2,l1,0)  at(r1,l1,1) ] [ move(r1,l2,l1,0)  at(r1,l2,1) ] [ move(r1,l1,l2,0)  move(r1,l2,l1,0) ] [ at(r1,l1,0)  at(r1,l1,1)  move(r1,l2,l1,0) ]  [ at(r1,l2,0)  at(r1,l2,1)  move(r1,l1,l2,0) ]  [ at(r1,l1,0)   at(r1,l1,1)  move(r1,l1,l2,0) ]  [ at(r1,l2,0)   at(r1,l2,1)  move(r1,l2,l1,0) ] Lets see how to construct such a formulaFormula has propositions for actions and states variablesat each possible timestep13Fluents (will be used as propositons) If plan