CS 4700: Foundations of Artificial IntelligenceProof methodsSatisfiabilityPropositional Satisfiability problemSatisfiability as an Encoding LanguageEncoding Latin Square Problems in Propositional Logic3D Encoding or Full EncodingDimacs formatExtended Latin Square 2x2Significant progress in Satisfiability MethodsModel CheckingTuring AwardA “real world” exampleSlide 14Slide 15Slide 16Slide 17Effective propositional inferenceSlide 19The DPLL algorithmSlide 21DPLLLearning in SatThe WalkSAT algorithmSlide 25Slide 26Computational Complexity of SATSAT ComplexityHard satisfiability problemsSlide 30Typical-Case ComplexityTypical Case Analysis: 3 SAT All clauses have 3 literalsSlide 33Slide 351CS 4700:Foundations of Artificial IntelligenceCarla P. [email protected]: Satisfiability (Reading R&N: Chapter 7)2Proof methodsProof 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•Different types of proofs –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 algorithms•(including some inference rules)Intro to logicCurrentmodulePrevious module3SatisfiabilityPropositional Satisfiability problemSatifiability (SAT): Given a formula in propositional calculus, is there a model(i.e., a satisfying interpretation, an assignment to its variables) making it true?We consider clausal form, e.g.:( a  b   c ) AND ( b   c) AND ( a  c)n2possible assignmentsSAT: prototypical hard combinatorial search and reasoning problem. Problem is NP-Complete. (Cook 1971)Surprising “power” of SAT for encoding computational problems.5Satisfiability as an Encoding LanguageEncoding Latin Square Problems in Propositional LogicVariables:Each variables represents a color assigned to a cell.Clauses:•Some color must be assigned to each cell •No color is repeated in the same row •No color is repeated in the same column 3n)21(ijnxijxijxij....,,2,1,,;, nkjikcolorhasjicellijkx ))1(()1()31()21(inkxknixinkxkixkixkixkixkixik))1(()1()31()21(njkxjknxnjkxjkxjkxjkxjkxjkxjk)4(nO}1,0{ijkx(exampleRow i Color k)(exampleColum j Color k)(clause of length n); n2(sets of negative binary clauses); n(n-1)/2 n n(sets of negative binary clauses); n(n-1)/2 n n3D Encoding or Full EncodingThis encoding is based on the cubic representation of the quasigroup: each line of the cube contains exactly one true variable; Variables:Same as 2D encoding.Clauses:•Same as the 2 D encoding plus:–Each color must appear at least once in each row;–Each color must appear at least once in each column;–No two colors are assigned to the same cell;))1(()1()31()21(nijxijnxijnxijxijxijxijxijxij)4(nO)21(inkxkixkixik)21(njkxjkxjkxjk8Dimacs formatAt the top of the file is a simple header.p cnf <variables> <clauses>Each variable should be assigned an integer index. Start at 1, as 0 is used to indicate the end of a clause. The positive integer a positive literal, whereas a negative interger represents a negative literal.Example-1 7 0  ( x1  x7)9Extended Latin Square 2x2p cnf 8 24 -1 -2 0 -3 -4 0 -5 -6 0 -7 -8 0 -1 -5 0 -2 -6 0 -3 -7 0 -4 -8 0 -1 -3 0 -2 -4 0 -5 -7 0 -6 -8 0 1 2 0 3 4 0 5 6 0 7 8 0 1 5 0 2 6 0 3 7 0 4 8 0 1 3 0 2 4 0 5 7 0 6 8 0order 2 -1 -1 -1 -11/2 3/45/6 7/8A cell gets at most a colorNo repetition of color in a column No repetition of color in a row A cell gets a colorA given color goes in each columnA given color goes in each row1 – cell 11 is red2 – cell 11 is green 3 – cell 12 is red4 – cell 12 is green5 – cell 21 is red6 – cell 21 is green7 – cell 22 is red8 – cell 22 is green10Significant progress in Satisfiability Methods Software and hardware verification – complete methods are critical - e.g. for verifying the correctness of chip design, using SAT encodingsCurrent methods can verify automatically the correctness of > 1/7 of a Pentium IV. Going from 50 variable, 200 constraints to 1,000,000 variables and 5,000,000 constraints in the last 10 years Applications: Hardware and Software Verification Planning, Protocol Design, etc.11Model CheckingTuring AwardSource: Slashdot13A “real world” examplei.e. ((not x1) or x7) and ((not x1) or x6)and … etc.Bounded Model Checking instance:(x177 or x169 or x161 or x153 … or x17 or x9 or x1 or (not x185)) clauses / constraints are getting more interesting…10 pages later: …164000 pages later: …!!!!!!a 59-cnf clause…Finally, 15,000 pages later:MiniSAT solver solves this instance in less than one minute.Note that: … !!!18Effective propositional inference19Effective propositional inferenceTwo families of algorithms for propositional inference (checking satisfiability) based on model checking (which are quite effective in practice):Complete backtracking search algorithmsDPLL algorithm (Davis, Putnam, Logemann, Loveland)Incomplete local search algorithms–WalkSAT algorithm–20The 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 of its literals 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.»The DPLL algorithmEarly terminationPure SymbolUnit PropagationBranch, recursive