15-780: Graduate AILecture 2. Proofs & FOLGeoff Gordon (this lecture)Tuomas SandholmTAs Erik Zawadzki, Abe Othman1AdminRecitations: Fri. 3PM here (GHC 4307)Vote: useful to have one tomorrow?would cover propositional & FO logicDraft schedule of due dates up on websubject to change with notice2Course email list15780students AT cs.cmu.eduEveryone’s official email should be in the list—we’ve sent a test message, so if you didn’t get it, let us know3Review4What is AI?Lots of examples: poker, driving robots, flying birds, RoboCupThings that are easy for humans/animals to do, but no obvious algorithmSearch / optimization / summationHandling uncertaintySequential decisions5Propositional logicSyntaxvariables, constants, operatorsliterals, clauses, sentencesSemantics (model ! {T, F})Truth tables, how to evaluate formulasSatisfiable, valid, contradictionRelationship to CSPs6Propositional logicManipulating formulas (e.g., de Morgan)Normal forms (e.g., CNF)Tseitin transformation to CNFHandling uncertainty (independent Nature choices + logical consequences)Compositional semanticsHow to translate informally-specified problems into logic (e.g., 3-coloring)7NP8SatisfiabilitySAT: determine whether a propositional logic sentence has a satisfying modelA decision problem: instance ! yes or noFundamental problem in CSmany decision problems reduce to SATinformally, if we can solve SAT, we can solve these other problemsA SAT solver is a good AI building block9Example decision problemk-coloring: can we color a map using only k colors in a way that keeps neighboring regions from being the same color?10ReductionLoosely, “A reduces to B” means that if we can solve B then we can solve AFormally, let A, B be decision problems (instances ! Y or N)A reduction is a poly-time function f such that, given an instance a of Af(a) is an instance of B, and A(a) = B(f(a))11Reduction picture12Reduction picture13Reduction picture14Reducing k-coloring ! SAT(ar " ag " ab) # (br " bg " bb) # (cr " cg " cb) #(dr " dg " db) # (er " eg " eb) # (zr " zg " zb) #(¬ar " ¬br) # (¬ag " ¬bg) # (¬ab " ¬bb) #(¬ar " ¬zr) # (¬ag " ¬zg) # (¬ab " ¬zb) #…15Direction of reductionWhen A reduces to B:if we can solve B, we can solve Aso B must be at least as hard as ATrivially, can take an easy problem and reduce it to a hard one16Not-so-useful reductionPath planning reduces to SATVariables: is edge e in path?Constraints:exactly 1 path-edge touches startexactly 1 path-edge touches goaleither 0 or 2 touch each other node17More useful: SAT ! CNF-SATGiven any propositional formula, Tseitin transformation produces (in poly time) an equivalent CNF formulaSo, given a CNF-SAT solver, we can solve SAT with general formulas18More useful: CNF-SAT ! 3SATCan reduce even further, to 3SATis 3CNF formula satisfiable?3CNF: at most 3 literals per clauseUseful if reducing SAT/3SAT to another problem (to show other problem hard)19CNF-SAT ! 3SATMust get rid of long clausesE.g., (a " ¬b " c " d " e " ¬f)Replace with(a " ¬b " x) # (¬x " c " y) # (¬y " d " z) # (¬z " e " ¬f)20NPA decision problem is in NP if it reduces to SATE.g., TSP, k-coloring, propositional planning, integer programming (decision versions)E.g., path planning, solving linear equations21NP-completeMany decision problems reduce back and forth to SAT: they are NP-completeCook showed how to simulate any poly-time nondeterministic computation w/ (very complicated, but still poly-size) SAT problemEquivalently, SAT is exactly as hard (in theory at least) as these other problemsS. A. Cook. The complexity of theorem-proving procedures, Proceedings of ACM STOC'71, pp. 151-158, 1971.22Open question: P = NPP = there is a poly-time algorithm to solveNP = reduces to SATWe know of no poly-time algorithm for SAT, but we also can’t prove that SAT requires more than about linear time!23Cost of reductionComplexity theorists often ignore little things like constant factors (or even polynomial factors!)So, is it a good idea to reduce your decision problem to SAT?Answer: sometimes…24Cost 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)25Choosing a reductionMay be many reductions from problem A to problem BMay have wildly different propertiese.g., solving transformed instance may take seconds vs. days26Proofs27EntailmentSentence A entails sentence B, A " B, if B is true in every model where A issame as saying that (A $ B) is valid28Proof treeA tree with a formula at each nodeAt each internal node, children " parentLeaves: assumptions or premisesRoot: consequenceIf we believe assumptions, we should also believe consequence29Proof tree example30Proof by contradictionAssume opposite of what we want to prove, show it leads to a contradiction Suppose we want to show KB " SWrite KB’ for (KB # ¬S)Build a proof tree withassumptions drawn from clauses of KB’conclusion = Fso, (KB # ¬S) " F (contradiction)31Proof by contradiction32Proof by contradiction33Inference rules34Inference ruleTo make a proof tree, we need to be able to figure out new formulas entailed by KBMethod for finding entailed formulas = inference ruleWe’ve implicitly been using one already35Modus ponensProbably most famous inference rule: all men are mortal, Socrates is a man, therefore Socrates is mortalQuantifier-free version: man(Socrates) # (man(Socrates) $ mortal(Socrates))d(a # b # c $ d) a b c36Another inference ruleModus tollensIf it’s raining the grass is wet; the grass is not wet, so it’s not raining¬a(a $ b) ¬b37One more…Resolution!, " are arbitrary subformulasCombines two formulas that contain a literal and its negationNot as commonly known as modus ponens / tollens(! " c) (¬c " ")! " "38Resolution exampleModus ponens / tollens are special casesModus tollens:(¬raining " grass-wet) # ¬grass-wet " ¬raining39Resolution examplerains $ pourspours # outside $ rustyCan we conclude rains # outside $ rusty?40Resolution examplerains $ pourspours # outside $ rustyCan we conclude rains # outside $ rusty?¬rains " pours¬pours " ¬outside " rusty40Resolution examplerains $ pourspours # outside $ rustyCan we conclude rains # outside $ rusty?¬rains " pours¬pours " ¬outside " rusty¬rains " ¬outside " rusty40ResolutionSimple proof by case analysisConsider separately