CS 188: Artificial IntelligenceSpring 2007Lecture 9: Logical Agents 2 2/13/2007SriniNarayanan –ICSI and UC BerkeleyMany slides over the course adapted from Dan Klein, Stuart Russell or Andrew MoorePDF created with pdfFactory Pro trial version www.pdffactory.comAnnouncements§ PPT slides§ Assignment 3PDF created with pdfFactory Pro trial version www.pdffactory.comInference by enumeration§ Depth-first enumeration of all models is sound and complete § PL-True returns true if the sentence holds within the model§ For n symbols, time complexity is O(2n), space complexity is O(n)PDF created with pdfFactory Pro trial version www.pdffactory.comValidity and satisfiabilityA sentence is valid if it is true in all models,e.g., True, A ∨¬A, A ⇒ A, (A ∧ (A ⇒ B)) ⇒ BValidity is connected to inference via the Deduction Theorem:KB ╞αif and only if (KB ⇒ α) is validA sentence is satisfiableif it is true in some modele.g., A∨ B, CA sentence is unsatisfiableif it is true in no modelse.g., A∧¬ASatisfiabilityis connected to inference via the following:KB ╞αif and only if (KB ∧¬α) is unsatisfiableSatisfiabilityof propositional logic was instrumental in developing thetheory of NP-completeness.PDF created with pdfFactory Pro trial version www.pdffactory.comProof methods§ Proof methods divide into (roughly) two kinds:§ Application of inference rules§ Legitimate (sound) generation of new sentences from old§ Proof = a sequence of inference rule applicationsCan use inference rules as operators in a standard search algorithm§ Typically require transformation of sentences into a normal form§ Model checking§ truth table enumeration (always exponential in n)§ improved backtracking, e.g., Davis--Putnam-Logemann-Loveland (DPLL)§ heuristic search in model space (sound but incomplete)e.g., min-conflicts-like hill-climbing algorithmsPDF created with pdfFactory Pro trial version www.pdffactory.comLogical equivalence§ To manipulate logical sentences we need some rewrite rules.§ Two sentences are logically equivalent iffthey are true in same models: α≡ßiff α╞βand β╞αYou need to know these !PDF created with pdfFactory Pro trial version www.pdffactory.comConversion to CNFB1,1⇔ (P1,2∨ P2,1)1.Eliminate ⇔,replacing α ⇔ β with (α ⇒ β)∧(β ⇒ α).(B1,1⇒ (P1,2∨ P2,1)) ∧ ((P1,2∨ P2,1) ⇒ B1,1)2. Eliminate ⇒, replacing α ⇒ β with ¬α∨ β.(¬B1,1∨ P1,2∨ P2,1) ∧ (¬(P1,2∨ P2,1) ∨ B1,1)3. Move ¬ inwards using de Morgan's rules and double-negation:(¬B1,1 ∨ P1,2∨ P2,1) ∧ ((¬P1,2 ∧¬P2,1) ∨ B1,1)4. Apply distributivitylaw (∧ over ∨) and flatten:(¬B1,1∨ P1,2∨ P2,1) ∧ (¬P1,2 ∨ B1,1) ∧ (¬P2,1∨ B1,1)PDF created with pdfFactory Pro trial version www.pdffactory.comResolutionConjunctive Normal Form (CNF)conjunction of disjunctions of literalsE.g., (A ∨¬B) ∧ (B ∨¬C ∨¬D) : Basic intuition, resolve B, ¬B to get (A) ∨ (¬C ∨¬D) (why?)§ Resolution inference rule (for CNF):li∨… ∨ lk, m1∨ … ∨ mnli∨ … ∨ li-1 ∨ li+1 ∨ … ∨ lk∨ m1∨ … ∨ mj-1 ∨ mj+1∨... ∨ mnwhere liand mjare complementary literals. E.g., P1,3∨ P2,2, ¬P2,2P1,3§ Resolution is sound and complete for propositional logic.§ Basic Use: KB ╞αiff(KB ∧¬α) is unsatisfiablePDF created with pdfFactory Pro trial version www.pdffactory.comResolutionSoundness of resolution inference rule: ¬(li∨ … ∨ li-1 ∨ li+1 ∨ … ∨ lk) ⇒ li¬mj⇒ (m1∨ … ∨ mj-1 ∨ mj+1∨... ∨ mn)¬(li∨ … ∨ li-1 ∨ li+1 ∨ … ∨ lk) ⇒ (m1∨ … ∨ mj-1 ∨ mj+1∨... ∨ mn)PDF created with pdfFactory Pro trial version www.pdffactory.comResolution algorithm§ Proof by contradiction, i.e., show KB∧¬α unsatisfiablePDF created with pdfFactory Pro trial version www.pdffactory.comResolution example§ KB = (B1,1⇔ (P1,2∨ P2,1)) ∧¬ B1,1 α = ¬P1,2Either you get an empty clause as a resolvent(success) or no new resolventsare created (failure)PDF created with pdfFactory Pro trial version www.pdffactory.comEfficient propositional inferenceTwo families of efficient algorithms for propositional inference:Complete backtracking search algorithms§ DPLL algorithm (Davis, Putnam, Logemann, Loveland)§ Incomplete local search algorithms§ WalkSAT algorithmPDF created with pdfFactory Pro trial version www.pdffactory.comThe DPLL algorithmDetermine if an input propositional logic sentence (in CNF) is satisfiable.Improvements over truth table enumeration:1.Early terminationA clause is true if any literal is true.A sentence is false if any clause is false.2.Pure symbol heuristicPure symbol: always appears with the same "sign" in all clauses.e.g., In the three clauses (A ∨¬B), (¬B ∨¬C), (C ∨ A), A and B are pure, C is impure. Make a pure symbol literal true.3.Unit clause heuristicUnit clause: only one literal in the clauseThe only literal in a unit clause must be true.PDF created with pdfFactory Pro trial version www.pdffactory.comThe WalkSAT algorithm§ Incomplete, local search algorithm§ Evaluation function: The min-conflict heuristic of minimizing the number of unsatisfied clauses§ Balance between greediness and randomnessPDF created with pdfFactory Pro trial version www.pdffactory.comThe WalkSAT algorithmMin ConflictsRandom walkPDF created with pdfFactory Pro trial version www.pdffactory.comHard satisfiabilityproblems§ Consider random 3-CNF sentences. e.g.,(¬D ∨¬B ∨ C) ∧ (B ∨¬A ∨¬C) ∧ (¬C ∨¬B ∨ E) ∧ (E ∨¬D ∨ B) ∧ (B ∨ E ∨¬C)m = number of clauses n = number of symbols§ Hard problems seem to cluster near m/n = 4.3 (critical point)PDF created with pdfFactory Pro trial version www.pdffactory.comHard satisfiabilityproblemsPDF created with pdfFactory Pro trial version www.pdffactory.comHard satisfiabilityproblems§ Median runtime for 100 satisfiablerandom 3-CNF sentences, n = 50PDF created with pdfFactory Pro trial version www.pdffactory.comInference-based agents in the wumpusworldA wumpus-world agent using propositional logic:¬P1,1¬W1,1Bx,y⇔ (Px,y+1∨ Px,y-1∨ Px+1,y∨ Px-1,y) Sx,y⇔ (Wx,y+1∨ Wx,y-1∨ Wx+1,y∨ Wx-1,y)W1,1∨ W1,2∨ … ∨ W4,4¬W1,1∨¬W1,2¬W1,1∨¬W1,3…⇒ 64 distinct proposition symbols, 155 sentencesPDF created with pdfFactory Pro trial version www.pdffactory.comPDF created with pdfFactory Pro trial version www.pdffactory.comSummary§ Logical agents apply inference to a knowledge base to derive new information and
View Full Document
Unlocking...