Planning and roboticsGeoff GordonA search problem•3-coloringOther important search problems•Minesweeper (image courtesy Andrew Moore)“Minesweeper” CSPV = { v1 , v2 , v3 , v4 , v5 , v6 , v7 , v8 }, D = { B (bomb) , S (space) }C = { (v1,v2) : { (B , S) , (S,B) } ,(v1,v2,v3) : { (B,S,S) , (S,B,S) , (S,S,B)},...}0 0000 0111211v1v2v3v4v5v6v7v8v1v2v3v4v5v6v7v8The Waltz algorithmOne of the earliest examples of a computation posed as a CSP.The Waltz algorithm is for interpreting line drawings of solid polyhedra.Adjacent intersections impose constraints on each other. Use CSP to find a unique set of labelings. Important step to “understanding” the image.Look at all intersections.What kind of intersection could thisbe? A concave intersection of threefaces? Or an external convex intersection?Waltz Alg. on simple scenesAssume all objects:• Have no shadows or cracks• Three-faced vertices• “General position”: no junctions change with small movements of the eye.Then each line on image is one of the following:• Boundary line (edge of an object) (<) with right hand of arrow denoting “solid” and left hand denoting “space”• Interior convex edge (+)• Interior concave edge (-)++++ 18 legal kinds of junctionsGiven a representation of the diagram, label each junction in one of the above manners.The junctions must be labelled so that lines are labelled consistently at both ends.Can you formulate that as a CSP? FUN FACT : Constraint Propagation always works perf ec tly.++++++++++------------•Sudokuhttp://www.cs.qub.ac.uk/~I.Spence/SuDoku/SuDoku.htmlOther important search problemsOther important search problems•Scheduling (e.g., of factory production)•Facility location•Circuit layout•Multi-robot planningOther important search problemsPropositional logicGeorge Boole1815–1864The meaning of truth•Model:•Valid:•Satisfiable (SAT):(a ∨ b ∨ c) ∧ (b ∨ -d)(a ∨ -a)Ex: planninginit: have(cake)goal: have(cake), eaten(cake)eat(cake):! pre: have(cake)! eff: -have(cake), eaten(cake)bake(cake):! pre: -have(cake)! eff: have(cake)have¬eateneathave¬eateneaten¬haveeathave¬eateneaten¬havebakePlan graphPlanning as logichave¬eateneathave¬eateneaten¬haveeathave¬eateneaten¬havebakePlan searchhave¬eateneathave¬eateneaten¬haveeathave¬eateneaten¬havebakePlan searchhave¬eateneathave¬eateneaten¬haveeathave¬eateneaten¬havebakePlan searchhave¬eateneathave¬eateneaten¬haveeathave¬eateneaten¬havebakePlan searchhave¬eateneathave¬eateneaten¬haveeathave¬eateneaten¬havebakePlan searchhave¬eateneathave¬eateneaten¬haveeathave¬eateneaten¬havebakePlan searchhave¬eateneathave¬eateneaten¬haveeathave¬eateneaten¬havebakePlan searchSAT is general•S. A. Cook (1971) proved that many useful search problems are “equivalent” to SAT•showed how to simulate a computer running “guess & check” search w/ (very complicated, but still poly-size) SAT problem•Equivalently, SAT is exactly as hard (in theory) as other search problems•In practice: SAT & MILP (below) go a long wayWorking with logic210 Chapter 7. Logical Agents(α ∧ β) ≡ (β ∧ α) commutativity of ∧(α ∨ β) ≡ (β ∨ α) commutativity of ∨((α ∧ β) ∧ γ) ≡ (α ∧ (β ∧ γ)) associativity of ∧((α ∨ β) ∨ γ) ≡ (α ∨ (β ∨ γ)) associativity of ∨¬(¬α) ≡ α double-negation elimination(α ⇒ β) ≡ (¬β ⇒ ¬α) contraposition(α ⇒ β) ≡ (¬α ∨ β) implication elimination(α ⇔ β) ≡ ((α ⇒ β) ∧ (β ⇒ α)) biconditional elimination¬(α ∧ β) ≡ (¬α ∨ ¬β) de Morgan¬(α ∨ β) ≡ (¬α ∧ ¬β) de Morgan(α ∧ (β ∨ γ)) ≡ ((α ∧ β) ∨ (α ∧ γ)) distr ibutivity of ∧ over ∨(α ∨ (β ∧ γ)) ≡ ((α ∨ β) ∧ (α ∨ γ)) distr ibutivity of ∨ over ∧Figure 7.11 Standard logical equivalences. The s ymbols α, β, and γ stand for arbitrarysentences of propositional logic.chapter, we will see algorithms that are much more efficient in practice. Unfortunately, everyknown inference algor ithm for propositional logi c has a worst-c as e c omplexity that is expo-nential in the size of the input. We do not expect to do better than this bec a us e propositionalentail ment is co-NP-complete. (See Appendix A.)Equivalence, validity, and satisfiabilityBefore we plunge into the deta ils of logical inference algorit hms, we will need some addi-tional concepts rel a ted to entail ment. Like entai lment, thes e concepts apply to a ll forms oflogic, but they are best illus trated for a par ticular logic, suc h as proposit ional logic.The first concept is logic al equivalence : two sentences α and β are l ogically equivalentLOGICALEQUIVALENCEif they ar e true in the same s e t of models. We write this as α ⇔ β. For example, wecan easily s how (using truth t a bles) tha t P ∧ Q and Q ∧ P are logically equivalent; otherequivalenc e s are shown in Figur e 7.11. They play much the same role in logic as arithmeticidentities do in ordinary mathematics . An alt e rnative de fini tion of equivalenc e is as f ollows:for a ny two sentence s α and β,α ≡ β if and onl y if α |= β and β |= α .(Recall that |= means entai lment.)The second concept we will need is validi ty. A se ntence is valid if it is true in allVALIDITYmodels. For example, the sente nc e P ∨ ¬P is valid. Valid sentences are also known a stautologie s — they are necessari ly true and hence vacuous. Because the sentence True is trueTAUTOLOGYin all models, every valid sentenc e i s logically equivalent to True.What good are valid s e ntences? From our definition of ent a ilment, we can derive thededuction theorem, whic h was known to the a nc ient Greeks:DEDUCTIONTHEOREMFor any sentences α and β, α |= β if and only i f the se ntence ( α ⇒ β) is vali d.(Exer c ise 7.4 asks for a proof.) We can think of the inference algori thm in Figure 7.10 asα, β, γ are arbitrary formulas210 Chapter 7. Logical Agents(α ∧ β) ≡ ( β ∧ α) commutativity of ∧(α ∨ β) ≡ ( β ∨ α) commutativity of ∨((α ∧ β) ∧ γ) ≡ (α ∧ (β ∧ γ)) ass oc iativity of ∧((α ∨ β) ∨ γ) ≡ (α ∨ (β ∨ γ)) ass oc iativity of ∨¬(¬α) ≡ α double-negation e limination(α ⇒ β) ≡ (¬β ⇒ ¬α) contraposition(α ⇒ β) ≡ (¬α ∨ β) implicat ion elimination(α ⇔ β) ≡ (( α ⇒ β) ∧ (β ⇒ α)) biconditional el imination¬(α ∧ β) ≡ (¬α ∨ ¬β) de Morgan¬(α ∨ β) ≡ (¬α ∧
View Full Document