15-780: Graduate AILecture 3. Logic, SAT, and CSPs Geoff Gordon (this lecture)Ziv Bar-Joseph TAs Michael Benisch, Yang GuAdminHW1 out today!On course websiteDue Wed 10/4Reminder: Matlab tutorial todayWeH 5409, 4:30PMLast episode, on Grad AITopics coveredC-spaceWays of splitting up C-spaceVisibility graphVoronoiExact, approximate cell decompositionAdaptive cells (quadtree, parti-game)Potential fieldsRRTsMore on searchI defined an “admissible” heuristic as one that underestimates cost-to-goalBetter definition: admissible heuristic is optimistic about futureCovers rewards as well as costsMap still must have absorbing goals and no negative-cost (positive-reward) cyclesMore on searchYou might think from last lecture that search = path planningOther apps: logical problems (robotic grad student, HW1, today’s lecture), planning (coming up soon)IDA*Do a DFS of all nodes with f(node) < kIf no solution, increment k and try againJust like DFID, except that instead of a depth bound, bounds f = g + h8/15 puzzle applethttp://www.cs.ualberta.ca/~aixplore/search/IDA/Applet/SearchApplet.htmlProject ideasPokerPokerHave code which learns a provably near-minimax RI Hold’Em strategy in 40 minCode is easily parallelizable and works on abstractions of larger gamesCan we beat world’s best computer Texas Hold’Em players?More on PokerMinimax strategy for heads-up poker = solving linear program1-card hands, 13-card deck: 52 vars, instantaneousRI Hold’Em: ~1,000,000 vars, 2 weeks / 30GB (exact sol) on CPLEX, 40 min / 1.5GB (approx sol) w/ our algorithmTX Hold’Em: ??? (up to 1017 vars or so)ScrabbleTMCan buy a hand-tweaked, very good computer Scrabble player for $30 or soCan we learn to beat it?Easy: enumerate legal movesHard: which should we take?Learning models for controlMost of this course, we’ll assume we have a good model of the world when we’re trying to planUsually not true in practice—must learn itProject: learn a model for an interesting system, write a planner for learned model, make planner work on original systemLearning models for controlR/C carLearning models for controlModel airplaneLogicWhy logic?Problem-solving: want to find solutions for problems like 8-puzzleReasoning: intelligent agents need knowledge about world to reach good decisions, want them to figure out consequences of their knowledgeAlso, logical inference is a special case of probabilistic inference (Part II)Propositional logicConstants & variables: T or FConnectives: ∧, ∨, ¬Can get by w/ just NANDSometimes also add others: ⊕, ⇒, ⇔, …Terminology: variable or constant with or w/o negation = literalWhole thing = formula or sentenceGeorge Boole1815–1864Propositional logicPrecedence:unary binds tighter than binary∧ has higher precedence than ∨parens: ¬(a∧b) vs. ¬a∧bQuiz:a∧¬b∨cTruth tablesxyx ∧ yTTTTFFFTFFFFxyx ∨ yTTTTFTFTTFFFA note on implication(a ⇒ b) is logically equivalent to (¬a ∨ b)If a is True, b must be True tooIf a False, no requirement on bE.g., “if I go to the movie I will have popcorn”: if no movie, may or may not have popcornaba ⇒ bTTTTFFFTTFFTTruth tables of all sizesx¬xTFTTxyz(x ∨ y) ⇒ zTTTTTFTFTTFFFTTFTFFFTFFFExpressive variable namesRather than names like a, b, x, y, we may use names like “rains” or “happy(John)”For now, “happy(John)” is just a string with no internal structurepropositional logic doesn’t know about John, just about variable happy(John)Later we will assign semanticsWhat can we do with a sentence?Assign values to variables and evaluate itAsk whether it’s true for zero, some, or all assignments to variablesSimplify it to get another, equivalent formula (which might have side effect of helping us test its value)ModelsAn assignment to all variables is called a model: e.g.M = (a: T, b: T, c: F)A sentence has a truth value in each modelFinding this truth value takes linear timeEx: ((a ∧ ¬b) ∨ c) in M is ???DefinitionsA sentence is satisfiable if it is True in some modelIf not satisfiable, it is a contradictionA sentence is valid if it is True in every model (a valid sentence is a tautology)A is a contradiction 󲰜 ¬A is validSATImportant search problem: SATSAT is the problem of determining whether a given propositional logic sentence is satisfiableSAT is a search problem: search nodes are (full or partial) models, neighbors differ in assignment for a single variableWhy is SAT important?Any ordinary* search problem reduces* to SATSo a good SAT solver is a good AI building blockOrdinary search problemOS problem = search graph + start node + solution test functionsearch graph = next-neighbor functionproblem: decide whether a solution node is reachable from startLimit: efficient (poly-time) functionsLimit: polynomial depth, branching factor (exponentially many vertices)Example (ordinary) search problem3-coloring: can we color a map using only 3 colors in a way that keeps neighboring regions from being the same color?ReductionLoosely, “problem A reduces to problem B” means that if we can solve B then we can solve AMore formally, A, B are decision problems (instances ↦ truth values)∃ a poly-time function f so that: given an instance a of A, f(a) is an instance of B, and A(a) = B(f(a))Example reduction=⇒Search and reductionOrdinary search problems reduce to SAT and (usually) vice versaEquivalently, SAT is as hard (in theory at least) as (most) other search problemsProven by S. A. Cook in 1971showed how to simulate poly-size-memory computer w/ (very complicated, but still poly-size) SAT problemCost of reductionComplexity theorists often ignore little things like constant factors (or even polynomial factors!)So, is it a good idea to reduce your search problem to SAT?Answer: sometimes…Cost of reductionSAT is well studied ⇒ fast solversSo, if there is an efficient reduction, ability to use fast SAT solvers can be a wine.g., 3-coloringanother example later (SATplan)Other times, cost of reduction is too highusu. because instance gets biggerwill also see example later (MILP)Working with formulasSimplifying formulasSearching for a model might get a lot easier if we simplify the formula firstBest case: could prove a sentence valid or contradictory without testing any models by simplifying until we get just T/FCatch: in general, about as hard as SAT[A ∈ SAT] = ¬[is (¬A) valid]EquivalenceTwo sentences are equivalent, A ≡ B, if they have same truth value in every model(rains ⇒ pours) ≡ (¬rains ∨