SAT: Propositional SatisfiabilitySAT: Propositional Satisfiability22c:145 Artificial IntelligenceRussell & Norvig, Ch. 7.6Validity vs. SatisfiabilityValidity vs. Satisfiabilityz Validity: – A sentence is valid if it is true in every interpretation (every interpretation is a model).– A sentence s is a valid consequence of a set S of sentences if (S => s)is valid.()– Proof methods: True Table and Inference Rulesz Satisfiability:– A set of sentences is satisfiable if there exists an interpretation in which every sentence is true (it has at least one model).– Proof Methods: The Davis-Putnam-Logeman-Loveland procedure (DPLL).SAT: Propositional SatisfiabilitySAT: Propositional Satisfiabilityz An instance of SAT is defined as (X, S)–X: A set of 0-1 (propositional) variables–S: A set of sentences (formulas) on Xz Goal: Find an assignment f: X -> {0, 1} so that every sentence becomes true.z SAT is the first NP-complete problem.– Good News: Thousands of problems can be transformed into SAT– Bad News: There are no efficient algorithms for SATConjunctive Normal Form (CNF)Conjunctive Normal Form (CNF)ϕ = ( a V c ) & ( b V c ) & (¬a V¬b V ¬c )ClausePositive LiteralNegative LiteralPropositional ClausesPropositional Clausesz Every propositional constraint can be converted into a set of equivalent clauses.– S = { C1, C2, …, Cm} = C1 & C2 & … & Cmz A clause is a disjunction of literals.–C = (L1V L2V … V Lk)(12 k)z A literal is either a variable or the negation of a variable.– L = x or L = ¬ xz A set of clauses is also said to be in Conjunctive Normal Form (CNF).Gate CNFGate CNFabdϕd= [d ≡ ¬(a & b )]= [d → ¬(a & b)] & [¬(a & b) → d]= (¬d V ¬a V¬b)[¬d →(a & b)]ϕd= [d ≡ ¬(a & b)]= ¬[d ⊕ ¬(a & b)]= ¬[(¬(a & b) & ¬d)V (a & b & d)]= ¬[¬a ¬d V ¬b ¬d V a b d]= (a V d)(b V d)(¬a V¬b V ¬d)(d ab)[ d→(a & b)]= (a V d)(b V d)(¬a V ¬b V ¬d)DIMACS FormatDIMACS Formatc This is an example ofc an SAT instance in DIMACS formatp cnf 3 5120DIMACS: Discrete Mathematics and Computer Science1 2 01 3 0-1 -2 0-1 -3 0-2 -3 0X1 V X2X1 V X3-X1 V -X2-X1 V -X3-X2 V -X3More on AssignmentsMore on Assignmentsz Assignments: {a = 0, b = 1} = ¬a & b– Partial (some variables still unassigned)– Complete (all variables assigned)– Conflicting (imply ¬ϕ)ϕ = (a V c) & (b V c) & (¬a V ¬b V ¬c)ϕ→(a V c)¬(a V c) → ¬ϕ¬a & ¬c → ¬ϕLiteral & Clause ClassificationLiteral & Clause Classificationϕ = (a V ¬b)(¬a V b V ¬c )(a V c V d )(¬a V ¬b V ¬c )violatedsatisfiedsatisfiedunresolveda assigned 0b assigned 1c and d unassignedz An unresolved clause is unit if it has exactly one unassigned literalϕ= (a V c)(b V c)(¬a V ¬b V ¬c)Unit Clause Rule Unit Clause Rule -- ImplicationsImplicationsϕ()()()z A unit clause has exactly one option for being satisfieda b → ¬ci.e. c must be set to 0.Pure Literal RulePure Literal Rulez A variable is pure if its literals are either all positive or all negativez Satisfiability of a formula is unaffected by assigning pure variables the values that satisfy all the clauses containing themcontaining themϕ = (a V c )(b V c )(b V ¬d)(¬a V ¬b V d)z Set c to 1; if ϕ becomes unsatisfiable, then it is also unsatisfiable when c is set to 0. z General technique for deriving new clausesExample: ω1= (¬a V b V c), ω2= (a V b V d)Resolution:Resolution/ConsensusResolution/Consensusres(ω1, ω2, a) = (b V c V d)z Complete procedure for satisfiability [Davis, JACM’60]z Impractical for real-world problem instancesz Application of restricted forms has been successful!– E.g., always apply restricted resolution• res((¬a V α), (a V α), a) = (α)α is a disjunction of literalsA Taxonomy of SAT AlgorithmsA Taxonomy of SAT AlgorithmsSAT AlgorithmsCompleteIncompleteBacktrack search (DP)Resolution (original DP)Recursive learning (RL)BDDs (Binary Decision Diagram)...Local search (hill climbing)Continuous formulationsGenetic algorithmsSimulated annealing...Tabu searchCan prove unsatisfiability Cannot prove unsatisfiabilityX1 V X2X1 V X3-X1 V -X2-X1 V -X3-X2 V -X31 V X21 V X30 V -X20 V -X3-X2 V -X30 V X20 V X31 V -X21 V -X3-X2 V -X3X1=0X2X3X1=111X2=0SAT: A search problem11-X2 V -X31X3110 V -X31 1110X2=11-X2-X3-X2 V -X3111-X31 V -X31 1111X2=0X3=01 0111X3=0 X3=10 X3111 V –X3X2=0X1 V X2X1 V X3-X1 V -X2-X1 V -X3-X2 V -X311-X2-X3-X2 V-X3X2X311-X2 V-X3X1=0X1=1Simplification Rules: 1 V C = 1, 0 V C = CX2 V X3-X2 V -X311110X2=1, X3=111111X2=0, X3=0Unit Propagation:Make all unit clauses true;No splitting on them.The DavisThe Davis--PutnamPutnam--LogemannLogemann--Loveland Algorithm (1960)Loveland Algorithm (1960)function Satisfiable ( clause set S ) return { 0, 1 }repeat /* unit propagation */ for each unit clause L in S dodelete from S every clause containing Ldelete-Lfrom eachCinSin which-Loccursdelete Lfrom each Cin Sin which Loccursif S is empty then return 1else if a clause in S is empty then return 0 until no more new unit clauses changeschoose a literal L occurring in S /* splitting */if Satisfiable( S U { L } ) then return 1 else if Satisfiable( S U { -L } ) then return 1else return 0DPLL uses DepthDPLL uses Depth--FirstFirst--SearchSearchz DFS with Backtrack: Instead of maintaining a path of nodes, only one node is maintained. The node is modified when going down and everything is undone when going up. yg ggpz The branching factor is dictated by the splitting rule.DPLL uses Backtrack SearchDPLL uses Backtrack Searchz Implicit enumerationz Iterated unit-clause rule– Boolean constraint propagation zPureliteral rulezPure-literal rulez Chronological backtracking in presence of conflictsz The worst-time complexity is exponential in terms of the number of variables.Implementing The DPLL AlgorithmImplementing The DPLL Algorithmz A destructive data structure is needed for clauses: Instead of copying clauses, modify them and then undo modification when backtracking.z Efficient algorithms for unit-propagation.z There are many choices for selecting a literal to split (heuristics are needed). Satbox’s Results on nSatbox’s Results on n--queen prob.queen prob.n solutions 1 soln. all soln.8 92 0.00 0.0110 724 0.00 0.0420 >100,000 0.00 240,40 - 0.16 -60 - 1.30 -80 - 4.30 -100 - 11.20 -• Times are in seconds. • There are 1646800 clauses for n=100Resolution (original DP)Resolution (original DP)z Iteratively apply resolution (consensus) to eliminate one variable each time– i.e., resolution between