Unformatted text preview:

15-780: Graduate AILecture 5. Logic, Planning Geoff Gordon (this lecture)Ziv Bar-Joseph TAs Geoff Hollinger, Henry LinReviewReviewCSPs (definition, examples)Sudoku, jobshop schedulingOver-, under-, critically-constrainedBasic search for SAT & CSPsSearch in SAT, CSPsConstraint propagation / unit resolutionConstraint learning from conflict clausesVariable orderingactivity, most-constrained variableValue orderingleast-constraining valueCitation for MiniSAThttp://www.cs.chalmers.se/Cs/Research/FormalMethods/MiniSat/cgi/MiniSat.ps.gz.cgiAlso, the map-coloring applet that I linked last class appears to be offlineRandomizationRandom restarts for DFS-based (DPLL) searchavoiding doldrumsWalkSATTseitin transformationPut the following formula in CNF:(a ∧ b) ∨ ((c ∨ d) ∧ e)Parse tree:Tseitin transformationIntroduce temporary variablesx = (a ∧ b)y = (c ∨ d)z = (y ∧ e)Tseitin transformationTo ensure x = (a ∧ b), wantx ⇒ (a ∧ b)(a ∧ b) ⇒ xTseitin transformationx ⇒ (a ∧ b)(¬x ∨ (a ∧ b))(¬x ∨ a) ∧ (¬x ∨ b)Tseitin transformation(a ∧ b) ⇒ x(¬(a ∧ b) ∨ x)(¬a ∨ ¬b ∨ x)Tseitin transformationTo ensure y = (c ∨ d), wanty ⇒ (c ∨ d)(c ∨ d) ⇒ yTseitin transformationy ⇒ (c ∨ d)(¬y ∨ c ∨ d)(c ∨ d) ⇒ y((¬c ∧ ¬d) ∨ y) (¬c ∨ y) ∧ (¬d ∨ y)Tseitin transformationFinally, z = (y ∧ e)z ⇒ (y ∧ e) ≡ (¬z ∨ y) ∧ (¬z ∨ e)(y ∧ e) ⇒ z ≡ (¬y ∨ ¬e ∨ z)Tseitin end result(a ∧ b) ∨ ((c ∨ d) ∧ e) ≡(¬x ∨ a) ∧ (¬x ∨ b) ∧ (¬a ∨ ¬b ∨ x) ∧(¬y ∨ c ∨ d) ∧ (¬c ∨ y) ∧ (¬d ∨ y) ∧(¬z ∨ y) ∧ (¬z ∨ e) ∧ (¬y ∨ ¬e ∨ z) ∧(x ∨ z)HW questions3(a) asks you to implement an “opaque” data structure for nodesThis just means that there is a well-defined interface, and data structure is accessed only through interfaceE.g., definitions of pq_init, pq_set, pq_pop, pq_test are such an interface, so the priqueue we gave is opaqueState numbering in maze \ x 1 2 3 4 5y \ ___________________________1 | 1 6 11 16 212 | 2 7 12 17 223 | 3 8 13 18 234 | 4 9 14 19 245 | 5 10 15 20 25This contradicts description in the text, but matches the code—updated text on webHW questionsStoring backpointers in A*, BFS, etc.Generic searchS = { start } M = ∅While (S ≠ ∅)x ← some element of S, S ← S \ xCheckSolution(x)For y ∈ neighbors(x) \ MS ← S ∪ {y} , backpointer(y) ← xM = M ∪ {x}HW questionsMore questions?First-order logicPredicates and objectsInterpret happy(John) or likes(Joe, pizza) as a predicate applied to some objectsObject = an object in the worldPredicate = boolean-valued function of objectsZero-argument predicate plays same role that Boolean variable did beforeFunctionsFunctions map zero or more objects to another objecte.g., professor(15-780), last-common-ancestor(John, Mary)Zero-argument function is the same as an object—John v. John()DefinitionsTerm = expression referring to an objectJohnleft-leg-of(father-of(president-of(USA)))Atom = predicate applied to objectshappy(John)rainingat(robot, Wean-5409, 11AM-Wed)DefinitionsLiteral = possibly-negated atomhappy(John), ¬happy(John)Sentence = literals joined by connectives like ∧∨¬⇒rainingdone(slides(780)) ⇒ happy(professor)ModelsMeaning of sentence: model ↦ {T, F}Models are now much more complicatedList of objectsTable of function values for each function mentioned in formulaTable of predicate values for each predicate mentioned in formulaFor exampleKB describing examplealive(cat)ear-of(cat) = earin(cat, box) ∧ in(ear, box)¬in(box, cat) ∧ ¬in(cat, nil) …ear-of(box) = ear-of(ear) = ear-of(nil) = nilcat ≠ box ∧ cat ≠ ear ∧ cat ≠ nil …Model of exampleObjects: C, B, E, NAssignments:cat: C, box: B, ear: E, nil: Near-of(C): E, ear-of(B): N, ear-of(E): N, ear-of(N): NPredicate values:in(C, B), ¬in(C, C), ¬in(C, N), …Failed modelObjects: C, E, NFails because there’s no way to satisfy inequality constraints with only 3 objectsAnother possible modelObjects: C, B, E, N, XExtra object X could have arbitrary properties since it’s not mentioned in KBE.g., X could be its own earAn embarrassment of modelsIn general, can be infinitely many modelsunless KB limits number somehowJob of KB is to rule out models that don’t match our idea of the worldAside: typed variablesKB illustrates need for data typesDon’t want to have to specify ear-of(box) or ¬in(cat, nil) Could design a type systemargument of happy() is of type animateFunction instances which disobey type rules have value nilQuantifiersSo far, still can’t say “all men are mortal”Add quantifiers and object variables∀x. man(x) ⇒ mortal(x)¬∃x. lunch(x) ∧ free(x)∀: no matter how we fill in object variables, formula is still true∃: there is some way to fill in object variables to make formula trueQuantificationNow we have atoms with free variablesAdding quantifier for x is called binding xIn (∀x. likes(x, y)), x is bound, y is freeCan add quantifiers and apply logical operations like ∧∨¬ in any orderBut must wind up with ground formula (no free variables)Scoping rulesPortion of formula where quantifier applies = scopeVariable is bound by innermost enclosing scope with matching nameTwo variables in different scopes can have same name—they are still different varsScoping examples(∀x. happy(x)) ∨ (∃x. ¬happy(x))Either everyone’s happy, or someone’s unhappy∀x. (raining ∧ outside(x) ⇒ (∃x. wet(x)))The x who is outside may not be the one who is wetSemantics of ∀Write (M / x: obj) for the model which is just like M except that variable x is assigned to the object objM / x: obj is a refinement of MA sentence (∀x. S) is true in M if S is true in (M / x: obj) for any object obj in MExampleM has objects (A, B, C) and predicate happy(x) which is true for A, B, CSentence ∀x. happy(x) is satisfied in Msince happy(A) is satisfied in M/x:A, happy(B) in M/x:B, happy(C) in M:x/CSemantics of ∃A sentence (∃x. S) is true in M if there is some object obj in M such that S is true in model (M / x: obj)ExampleM has objects (A, B, C) and predicatehappy(A) = happy(B) = Truehappy(C) = FalseSentence ∃x. happy(x) is satisfied in MSince happy(x) is satisfied in, e.g., M/x:BQuantifier nestingEnglish sentence “everybody loves somebody” is ambiguousTranslates to logical sentences∀x. ∃y. loves(x, y)∃y. ∀x.


View Full Document

CMU CS 15780 - lecture

Download lecture
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 lecture 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 lecture 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?