ITCS 3153 Artificial IntelligencePropositional LogicBacktrackingSearching for variable valuesSlide 5Slide 6WalkSAT terminationSo how well do these work?What about more clauses?What about more clausesCombining it allWumpus WorldITCS 3153Artificial IntelligenceLecture 12Lecture 12Logical AgentsLogical AgentsChapter 7Chapter 7Lecture 12Lecture 12Logical AgentsLogical AgentsChapter 7Chapter 7Propositional LogicWe’re still emphasizing Propositional LogicWe’re still emphasizing Propositional LogicVery important question with this methodVery important question with this method•Does knowledge base of propositional logic Does knowledge base of propositional logic satisfysatisfy a a particular proposition?particular proposition?–Can we generate some sequence of resolutions that prove Can we generate some sequence of resolutions that prove a proposition is possible?a proposition is possible?We’re still emphasizing Propositional LogicWe’re still emphasizing Propositional LogicVery important question with this methodVery important question with this method•Does knowledge base of propositional logic Does knowledge base of propositional logic satisfysatisfy a a particular proposition?particular proposition?–Can we generate some sequence of resolutions that prove Can we generate some sequence of resolutions that prove a proposition is possible?a proposition is possible?BacktrackingAnother way (representation) for searchingAnother way (representation) for searching•Problem to solve is in CNFProblem to solve is in CNF–Is Marvin a Martian given --- M == 1 (true)?Is Marvin a Martian given --- M == 1 (true)?Marvin is green --- G=1Marvin is green --- G=1Marvin is little --- L=1Marvin is little --- L=1(little and green) implies Martian --- (L ^ G) => M(little and green) implies Martian --- (L ^ G) => M ~(L^G) V M ~(L^G) V M ~L V ~G V M = 1 ~L V ~G V M = 1–Proof by contradiction… are there true/false values for G, L, and M that are Proof by contradiction… are there true/false values for G, L, and M that are consistent with knowledge base and Marvin not being a Martian?consistent with knowledge base and Marvin not being a Martian?G ^ L ^ (~L V ~G V M) ^ ~M == 0? G ^ L ^ (~L V ~G V M) ^ ~M == 0? Another way (representation) for searchingAnother way (representation) for searching•Problem to solve is in CNFProblem to solve is in CNF–Is Marvin a Martian given --- M == 1 (true)?Is Marvin a Martian given --- M == 1 (true)?Marvin is green --- G=1Marvin is green --- G=1Marvin is little --- L=1Marvin is little --- L=1(little and green) implies Martian --- (L ^ G) => M(little and green) implies Martian --- (L ^ G) => M ~(L^G) V M ~(L^G) V M ~L V ~G V M = 1 ~L V ~G V M = 1–Proof by contradiction… are there true/false values for G, L, and M that are Proof by contradiction… are there true/false values for G, L, and M that are consistent with knowledge base and Marvin not being a Martian?consistent with knowledge base and Marvin not being a Martian?G ^ L ^ (~L V ~G V M) ^ ~M == 0? G ^ L ^ (~L V ~G V M) ^ ~M == 0? Make sure youunderstand thislogicSearching for variable valuesWant to find values such that:Want to find values such that:•Randomly consider all true/false assignments to variables Randomly consider all true/false assignments to variables until we exhaust them all or find matchuntil we exhaust them all or find match–(G, L, M) = (1, 0, 0)… no(G, L, M) = (1, 0, 0)… no = (0, 1, 0)… no = (0, 1, 0)… no = (0, 0, 0)… no = (0, 0, 0)… no = (1, 1, 0)… no = (1, 1, 0)… no •Alternatively…Alternatively…Want to find values such that:Want to find values such that:•Randomly consider all true/false assignments to variables Randomly consider all true/false assignments to variables until we exhaust them all or find matchuntil we exhaust them all or find match–(G, L, M) = (1, 0, 0)… no(G, L, M) = (1, 0, 0)… no = (0, 1, 0)… no = (0, 1, 0)… no = (0, 0, 0)… no = (0, 0, 0)… no = (1, 1, 0)… no = (1, 1, 0)… no •Alternatively…Alternatively…G ^ L ^ (~L V ~G V M) ^ ~M == 0G ^ L ^ (~L V ~G V M) ^ ~M == 0Searching for variable valuesDavis-Putnam Algorithm (DPLL)Davis-Putnam Algorithm (DPLL)•Search through possible assignments to (G, L, M) via depth first search Search through possible assignments to (G, L, M) via depth first search (0, 0, 0) to (0, 0, 1) to (0, 1, 0)…(0, 0, 0) to (0, 0, 1) to (0, 1, 0)…–Each clause of CNF must be trueEach clause of CNF must be trueTerminate consideration when clause evaluates to falseTerminate consideration when clause evaluates to false–Use heuristics to reduce repeated computation of propositionsUse heuristics to reduce repeated computation of propositionsEarly terminationEarly terminationPure symbol heuristicPure symbol heuristicUnit clause heuristicUnit clause heuristicDavis-Putnam Algorithm (DPLL)Davis-Putnam Algorithm (DPLL)•Search through possible assignments to (G, L, M) via depth first search Search through possible assignments to (G, L, M) via depth first search (0, 0, 0) to (0, 0, 1) to (0, 1, 0)…(0, 0, 0) to (0, 0, 1) to (0, 1, 0)…–Each clause of CNF must be trueEach clause of CNF must be trueTerminate consideration when clause evaluates to falseTerminate consideration when clause evaluates to false–Use heuristics to reduce repeated computation of propositionsUse heuristics to reduce repeated computation of propositionsEarly terminationEarly terminationPure symbol heuristicPure symbol heuristicUnit clause heuristicUnit clause heuristicGLMSearching for variable valuesOther ways to find (G, L, M) assignments for:Other ways to find (G, L, M) assignments for: G ^ L ^ (~L V ~G V M) ^ ~M == 0G ^ L ^ (~L V ~G V M) ^ ~M == 0•Simulated Annealing (WalkSAT)–Start with initial guess (0, 1, 1)–Evaluation metric is the number of clauses that evaluate to true–Move “in direction” of guesses that cause more clauses to be true–Many local mins, use lots of randomnessWalkSAT terminationHow do you know when simulated annealing is How do you know when simulated annealing is done?done?•No way to know