3/19/2003 copyright Brian Williams 1 and Satisfiability Brian C. Williams 16.410 October 1, 2003 3/19/2003 copyright Brian Williams 2 Reading Assignments: Propositional Logic ? Propositional Logic AIMA Ch. 6 – Propositional Logic 3/19/2003 copyright Brian Williams 3 Outline ? Propositional Satisfiability ? ? Backtrack Search ? Unit Propagation ? DPLL: Unit Propagation + Backtrack Search ? Characteristics of DPLL ? local search using GSAT 3/19/2003 copyright Brian Williams 4 ? Variables: ? Domain: ? Constraints: Clauses that must be true ? Clause (not A or B or E) ? A disjunction of Literals ? Literal: Proposition or its negation ? B ? Negative Literal Propositional Clauses Propositional Clauses Propositions Positive Literal Not A {True, False} 3/19/2003 copyright Brian Williams 5 Propositional Satisfiability ? A truth assignment to all propositions such that all clauses are satisfied. ? A clause is satisfied if and only if at least one literal is true. ? A clause is violated if and only if all literals are false. ? (not A or B or E) 3/19/2003 copyright Brian Williams 6 Propositional Satisfiability Find a truth assignment that satisfies logical sentence T: ? Reduce sentence T to clausal form. ? Perform search similar to Forward Checking Propositional satisfiability testing: 1990: 100 variables / 200 clauses (constraints) 1998: 10,000 - 100,000 vars / 10^6 clauses Novel applications: e.g. diagnosis, planning, software / circuit testing, machine learning, and protein folding 3/19/2003 copyright Brian Williams 7 Outline ? Propositional Satisfiability ? ? Backtrack Search ? Unit Propagation ? DPLL: Unit Propagation + Backtrack Search ? Characteristics of DPLL ? local search using GSAT 3/19/2003 copyright Brian Williams 8 Propositional Satisfiability using Backtrack Search ? Assign true or false to an unassigned proposition. ? Backtrack as soon as a clause is violated. Example: ? C1: Not A or B ? C2: Not C or A ? C3: Not B or C A F F B C F S S S Propositional Clauses 3/19/2003 copyright Brian Williams 9 Propositional Satisfiability using Backtrack Search ? Assign true or false to an unassigned proposition. ? Backtrack as soon as a clause is violated. Example: ? C1: Not A or B ? C2: Not C or A ? C3: Not B or C A F F B C F T S u S 3/19/2003 copyright Brian Williams 10 Propositional Satisfiability using Backtrack Search ? Assign true or false to an unassigned proposition. ? Backtrack as soon as a clause is violated. Example: ? C1: Not A or B ? C2: Not C or A ? C3: Not B or C A F F B C F T T C F S S v 3/19/2003 copyright Brian Williams 11 Propositional Satisfiability using Backtrack Search ? Assign true or false to an unassigned proposition. ? Backtrack as soon as a clause is violated. Example: ? C1: Not A or B ? C2: Not C or A ? C3: Not B or C A F F B C F T T C TF S S v 3/19/2003 copyright Brian Williams 12 Propositional Satisfiability using Backtrack Search ? Assign true or false to an unassigned proposition. ? Backtrack as soon as a clause is violated. Example: ? C1: Not A or B ? C2: Not C or A ? C3: Not B or C A F F B C F T T C TF B T C F S S v 3/19/2003 copyright Brian Williams 13 Propositional Satisfiability using Backtrack Search ? Assign true or false to an unassigned proposition. ? Backtrack as soon as a clause is violated. Example: ? C1: Not A or B ? C2: Not C or A ? C3: Not B or C A F F B C F T T C TF B T C F T C F S S v 3/19/2003 copyright Brian Williams 14 Propositional Satisfiability using Backtrack Search ? Assign true or false to an unassigned proposition. ? Backtrack as soon as a clause is violated. Example: ? C1: Not A or B ? C2: Not C or A ? C3: Not B or C A F F B C F T T C TF B T C F T C TF S S S 3/19/2003 copyright Brian Williams 15 Backtrack Search Procedure BT(phi,A) Input: A cnf theory phi, an assignment A to propositions in phi Output: A decision of whether phi is satisfiable. 1. If a clause is violated return(false); 2. Else if all propositions are assigned return(true); 3. Else Q = some unassigned proposition in phi; 4. Return (BT(phi, A[Q = True]) or 5. BT(phi, A[Q = False]) 3/19/2003 copyright Brian Williams 16 Outline ? Propositional Satisfiability ? ? Backtrack Search ? Unit Propagation ? DPLL: Unit Propagation + Backtrack Search ? Characteristics of DPLL ? local search using GSAT Propositional Clauses 3/19/2003 copyright Brian Williams 17 Unit Propagation Idea: Forward checking on binary clauses (not A or B) {F} {T,F} ? {T} {T,F} ? Unit propagation: If all literals are false, save l then assign true to l: ? (not A) (not B) (A or B or C) C 3/19/2003 copyright Brian Williams 18 Unit Propagation Examples ? C1: Not A or B ? C2: Not C or A ? C3: Not B or C ? C4: A C4 A True C1 B True C3 C True Satisfied Satisfied Satisfied Satisfied 3/19/2003 copyright Brian Williams 19 Unit Propagation Examples ? C1: Not A or B ? C2: Not C or A ? C3: Not B or C ? C4: A ? C4’: Not B C1 C3C4 C1 C2 C4’ A True B True C True A False B False C False C4 A True Satisfied Satisfied Satisfied Satisfied 3/19/2003 copyright Brian Williams 20 C 1 : ?r ? q ? p C 2 :?p ?? t r true q false p t procedure propagate(C) // C is a clause if all literals in C are false except l, and l is unassigned then assign true to l and record C as a support for l and for each clause C’ mentioning “not l”, propagate(C’) end propagate Unit Propagation 3/19/2003 copyright Brian Williams 21 C 1 : ?r ? q ? p C 2 :?p ? t r true q false p t propagate(C) C is a clause if all literals in C are false except l, and l is unassigned then assign true to l and record C as a support for l and for each clause C’ mentioning “not l”, propagate(C’) end propagate Unit Propagation 3/19/2003 copyright Brian Williams 22 C 1 : ?r ? q ? p r q p C 2 :?p ? t true false true t propagate(C) C is a clause if all literals in C are false except l, and l is unassigned then assign true to l and record C as a support for l and for each clause C’ “not l”, propagate(C’) end propagate Unit Propagation procedure procedure mentioning ? // ? // 3/19/2003 copyright Brian Williams 23 C 1 : ?r ? q ? p r q p C 2 :?p ? t true false true t propagate(C) C is a clause if all literals in C are false except l, and l is unassigned then assign true to l and record C as a support for l and for each clause C’ mentioning “not l”, propagate(C’) end propagate Unit Propagation 3/19/2003 copyright Brian Williams 24 r q p true false true propagate(C) C is a clause if all literals in C are false except l, and l is unassigned then assign true to l and record C as a support for l and for each clause C’ “not l”, propagate(C’) end propagate C 2 : ? p ? t t C 1 : ?r ? q ? p Unit Propagation procedure procedure mentioning ? // // ? 3/19/2003 copyright Brian Williams 25 r q p C 2 : ? p ? t true false true t false propagate(C) C is a clause if all literals in C are false except l, and l is unassigned then assign true to l and record C as a support for l and for each clause C’ mentioning “not l”, propagate(C’) end propagate C 1 : ?r ? q ? p Unit Propagation 3/19/2003 copyright Brian Williams 26 Outline ? Propositional Satisfiability ? ? Backtrack Search ? Unit Propagation ? DPLL: Unit Propagation + Backtrack Search ? Characteristics of DPLL ? local search using GSAT procedure Propositional Clauses ? // 3/19/2003 copyright Brian Williams 27 How Do We Combine Resolution and Back Track Search? Backtrack Search ? Assign true or false to an unassigned proposition. ? Backtrack as soon as a clause is violated. ? Example: ? C1: Not A or B ? C2: Not C or A ? C3: Not B or C A F T B F T C F T C F T B F T C C F TF T ? Similar to Forward Checking: ? Perform limited form of inference ? apply inference rule after assigning each variable. 3/19/2003 copyright Brian Williams 28 Propositional Satisfiability by DPLL Initially: ? Unit propagate. Repeat: ? Assign true or false to an unassigned proposition. ? Unit propagate. ? Backtrack as soon as a clause is violated. ? is complete. Propagate: C = F B = F A F Example: ? C1: Not A or B ? C2: Not C or A ? C3: Not B or C S S S Satisfiable if assignment is complete. Satisfiable if assignment 3/19/2003 copyright Brian Williams 29 Propositional Satisfiability by DPLL Initially: ? Unit propagate. Repeat: ? Assign true or false to an unassigned proposition. ? Unit propagate. ? Backtrack as soon as a clause is violated. ? is complete. Propagate: C = F B = F A F T Propagate: B = T C = T Example: ? C1: Not A or B ? C2: Not C or A ? C3: Not B or C S S S 3/19/2003 copyright Brian Williams 30 DPLL Procedure [Davis, Putnam Logmann, Loveland, 1962] DPLL(phi,A) Input: A cnf theory phi, an assignment A to propositions in phi Output: A decision of whether phi is satisfiable. 1. propagate(phi); 2. If a clause is violated return(false); 3. Else if all propositions are assigned return(true); 4. Else Q = some unassigned proposition in phi; 6. Return (DPLL(phi, A[Q = True]) or 7. DPLL(phi, A[Q = False]) Satisfiable if assignment copyright Brian Williams 32 3/19/2003 copyright Brian Williams 31 Outline ? Propositional Satisfiability ? ? Backtrack Search ? Unit Propagation ? DPLL: Unit Propagation + Backtrack Search ? Characteristics of DPLL ? local search using GSAT 3/19/2003 Hardness of 3SAT 0 2 3 4 5 Ratio of Clauses-to-Variables 6 7 8 1000 3000 2000 4000 50 var 40 var 20 var Propositional Clauses s D P C a l l copyright Brian Williams3/19/2003 33 The 4.3 Point 0.0 2 3 4 5 Ratio of Clauses-to-Variables 6 7 8 0.2 0.6 0.4 50 var 40 var 20 var 50% sat Mitchell, Selman, and Levesque 1991 0.8 1.0 0 1000 3000 2000 4000 3/19/2003 copyright Brian Williams 34 P r o b a b i l i t y D P C a l l s 2 UNSAT Phase SA T Phase 20 3/19/2003 copyright Brian Williams 35 Intuition ? At low ratios: ? few clauses (constraints) ? many assignments ? easily found ? At high ratios: ? many clauses ? inconsistencies easily detected 3/19/2003 copyright Brian Williams 36 Fraction of Formulae Unsatisfied 10 0 24 40 50 1 0 3 0. 2 1. 0 0. 4 0. 6 0. 8 M/ N 4 5 6 7 Phase Transitions for Different Numbers of Variables Different Numbers of Variables 3/19/2003 copyright Brian Williams 37 Phase transition 2-, 3-, 4-, 5-, and 6-SAT 3/19/2003 copyright Brian Williams 38 Outline ? Propositional Satisfiability ? Propositional Clauses ? Backtrack Search ? Unit Propagation ? DPLL: Unit Propagation + Backtrack Search ? Characteristics of DPLL ? local search using GSAT 3/19/2003 copyright Brian Williams 39 Incremental Repair (min-conflict heuristic) 1. “near” correct one. 2. Select a variable in conflict and assign it a value that minimizes the number of conflicts (break ties randomly). R,G,B GR, G Graph Coloring Initial Domains V 1 V 2 V 3 Example: Start with all Green, what are the next steps? 3/19/2003 copyright Brian Williams 40 Incremental Repair (min-conflict heuristic) 1. solution “near” correct one. 2. the number of conflicts (break ties randomly). (with good initial guesses) 10 -2 10 10 -1 1 100 10 2 10 1 10 3 10 4 10 5 10 6 Sec ) Spike Hubble Telescope Scheduler [Minton et al.] Initialize a candidate solution using “greedy” heuristic – get solution Different-color constraint Spike Hubble Telescope Scheduler [Minton et al.] Initialize a candidate solution using “greedy” heuristic – get Select a variable in conflict and assign it a value that minimizes Performance on n-queens. Size (n) (Sparc 1 3/19/2003 copyright Brian Williams 41 Problem: Pure hill climbers get stuck in local minima. Solution: Add random moves to get out of minima Randomized hill climber used to solve SAT problems One of the more effective methods found for this problem WalkSAT Min-conflict heuristic 3/19/2003 copyright Brian Williams 42 Search Performance on N Queens ? Standard Search ? Backtracking ? BT with Forward Checking ? Dynamic Variable Ordering ? Iterative Repair ? A handful of queens ? About 15 queens ? About 30 queens ? About 1,000 queens ? About 10,000,000 queens (except truly hard problems) 1 2 3 4 Q Q Q Q 3/19/2003 copyright Brian Williams 43 GSAT Example ? C1: Not A or B ? C2: Not C or Not A ? C3: or B or Not C C1, C2, C3 violated A True B False C True C3 violated False C2 violated True C1 violated False 1. Pick random assignment 2. assignment, counting violated clauses 3. violations. 3/19/2003 copyright Brian Williams 44 GSAT Example ? C1: Not A or B ? C2: Not C or Not A ? C3: or B or Not C C1 violated A True B False C False Satisfied False Satisfied True C1,C2,C3 violated True 1. Pick random assignment 2. assignment, counting violated clauses 3. violations. Pick assignment with fewest Pick assignment with fewest Check effect of flipping each Check effect of flipping each 3/19/2003 copyright Brian Williams 45 GSAT Example ? C1: Not A or B ? C2: Not C or Not A ? C3: or B or Not C Satisfied A True B True C False 1. Pick random assignment 2. Check effect of flipping each assignment, counting violated clauses 3. Pick assignment with fewest violations. 3/19/2003 copyright Brian Williams 46 Satisfiability Testing Procedures ? Reduce to CNF (Clausal Form) then: ? Systematic, complete procedures ? Depth-first backtrack search (Davis, Putnam, & Loveland 1961) ? unit propagation, shortest clause heuristic ? State-of-the-art implementations: ? ntab (Crawford & Auton 1997) ? itms (Nayak & Williams 1997) ? many others! See SATLIB 1998 / Hoos & Stutzle ? Stochastic, incomplete procedures ? GSAT (Selman et. al 1993) ? Walksat (Selman & Kautz 1993) ? greedy local search + noise to escape local minima