Unformatted text preview:

15-780: Graduate AILecture 4. SAT, CSPs, and FOL Geoff Gordon (this lecture)Ziv Bar-Joseph TAs Geoff Hollinger, Henry LinAdminQuestions on HW?ReviewWhat you should knowPropositional logicsyntax, truth tablesmodels, satisfiability, validity, entailment, etc.equivalence rules (e.g., De Morgan)inference rules (e.g., resolution)What you should knowNormal forms (e.g., CNF)Structure of a theorem proverproof trees, knowledge basesSAT problemits search graph(s)reductions (e.g., 3-coloring to SAT)CSPsConstraint satisfactionRecall 3-coloringTurned map into SAT problem (constant factor blowup)Did we have to do that?CSP definitionNo: represent as CSP insteadCSP = (variables, domains, constraints)Variable: aDomain: (R, G, B)Constraint: a, b ∈ (RG, RB, GR, GB, BR, BG)Constraints usually represented compactlyExamplehttp://ocw.mit.edu/OcwWeb/Electrical-Engineering-and-Computer-Science/6-034Artificial-IntelligenceFall2002/Tools/detail/mapresalloc.htmAppears to be offline nowOther important CSPsMinesweeper (courtesy Andrew Moore)“Minesweeper” CSPV = { v1 , v2 , v3 , v4 , v5 , v6 , v7 , v8 }, D = { B (bomb) , S (space) }C = { (v1,v2) : { (B , S) , (S,B) } ,(v1,v2,v3) : { (B,S,S) , (S,B,S) , (S,S,B)},...}0 0000 0111211v1v2v3v4v5v6v7v8v1v2v3v4v5v6v7v8The Waltz algorithmOne of the earliest examples of a computation posed as a CSP.The Waltz algorithm is for interpreting line drawings of solid polyhedra.Adjacent intersections impose constraints on each other. Use CSP to find a unique set of labelings. Important step to “understanding” the image.Look at all intersections.What kind of intersection could thisbe? A concave intersection of threefaces? Or an external convex intersection?Waltz Alg. on simple scenesAssume all objects:• Have no shadows or cracks• Three-faced vertices• “General position”: no junctions change with small movements of the eye.Then each line on image is one of the following:• Boundary line (edge of an object) (<) with right hand of arrow denoting “solid” and left hand denoting “space”• Interior convex edge (+)• Interior concave edge (-)++++ 18 legal kinds of junctionsGiven a representation of the diagram, label each junction in one of the above manners.The junctions must be labelled so that lines are labelled consistently at both ends.Can you formulate that as a CSP? FUN FACT: Constraint Propagation al wa ys works perf ec tl y.++++++++++------------Other important CSPsSudokuhttp://www.cs.qub.ac.uk/~I.Spence/SuDoku/SuDoku.htmlOther important CSPsJob-shop schedulingA bunch of jobseach job is a sequence of operationsdrill, polish, paintA bunch of resourceseach operation needs several resourcesIs there a schedule of length ≤ k?Solving SAT&CSPSAT & CSP solversSearch algorithms routinely handle SAT or CSP problems with 1,000,000 variablesSuch a solver is a subroutine in one of the planning algorithms we’ll discuss soonHard instancesSAT, CSP are NP-complete! How can we do problems with 1,000,000 variables?!?NP-complete doesn’t mean runtime has to be exponential for all examplese.g., (a ∨ b) ∧ (c ∨ d) ∧ (e ∨ f ∨ g)Many practical examples are apparently not all that hardSo where are the hard examples?Why are some practical examples easy?They are over- or under-constrainedunder-constrained ⇒ succeed quicklyover-constrained ⇒ fail quicklyWhere are the hard examples?“critically constrained”Aside: random 3CNF formulasIt turns out that random formulas can be quite hard to solveRandomly select variables to be in each clause, randomize +ve vs. -veIf we generate too few clauses, formula is under-constrainedToo many: over-constrainedJust rightRandom formulas w/ n=50 vars, m clausesClauses have 3 distinct literals, 50% negatedSection 7.7. Agents Based on Propositional Logic 22500.20.40.60.810 1 2 3 4 5 6 7 8P(satisfiable)Clause/symbol ratio m/n02004006008001000120014001600180020000 1 2 3 4 5 6 7 8RuntimeClause/symbol ratio m/nDPLLWalkSAT(a) (b)Figure 7.18 (a) Graph showing the probability that a random 3-CNF sentence with n = 50symbols is satisfiable, as a function of the clause/symbol ratio m/n. (b) Graph of the medianruntime of DPLL and WALKSAT on 100 satisfiable random 3-CNF sentences with n = 50,for a narrow range of m/n around the critical point.7.7 AGENTS BASED ON PROPOSITIONAL LOGICIn this section, we bring together what we have lear ne d so far in order to cons truct agentsthat operate using propositional logic. We will look at two kinds of agents: those whichuse inference algorithms and a knowledge base, like the generic knowledge-based agent inFigure 7.1, and thos e which evaluate logical expressions directly in the form of circuits . Wewill demonstrate bot h kinds of agents in the wumpus world, and will find that both sufferfrom serious dr awbacks.Finding pits and wumpuses u sing logical inferenceLet us begin with an agent that reasons logically about the l oc a tion of pits, wumpuses, andsafe squares . It begins with a knowledge base that states the “physics” of the wumpus world.It knows that [1,1] doe s not cont a in a pit or a wumpus; that is, ¬P1,1and ¬W1,1. For everysquare [x, y], it knows a sentence s tating how a breeze arises:Bx,y⇔ (Px,y+1∨ Px,y−1∨ Px+1,y∨ Px−1,y) . (7.1)For every squa re [x, y], it knows a sentence stating how a stench aris e s :Sx,y⇔ (Wx,y+1∨ Wx,y−1∨ Wx+1,y∨ Wx−1,y) . (7.2)Finally, it knows that there is exactly one wumpus. This is expressed i n two parts. First , wehave to say that ther e is at least one wumpus:W1,1∨ W1,2∨ · · · ∨ W4,3∨ W4,4.Then, we have to say that there is at most one wumpus. One way to do this i s to say thatfor any two squares, one of them must be wumpus-free. With n squares, we get n(n − 1)/24.3It turns out m/n = 4.3 (and change) is the hard area, for any sufficiently large nWhat’s special about 4.3? I don’t know.Unfortunately real formulas don’t look like random ones, so it’s not so easy to check whether they are critically constrainedSAT & CSP as search problemsSearch space: models or partial modelsNeighbors: change assignment to one variableSearch space may also include changes to constraints / clausesadd a new constraint / clausesimplify existing onesSearch in a CSPLet’s try DFS using partial assignmentstop to bottom, RGBDFS looks stupidOK, that wasn’t the right wayBlindingly obvious: consistency checkingDon’t assign a variable to a value that conflicts with a neighborSearch in a CSPDFS with consistency checkingWell,


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?