Recursion and Induction: BooleanSatisfiability; Davis-Putnam ProcedureGreg PlaxtonTheory in Programming Practice, Fall 2005Department of Computer ScienceUniversity of Texas at AustinProgram Design: Boolean Satisfiability• In this lecture and the next one, we consider the design andimplementation of a Haskell program for solving the “booleansatisfiability” problem• Input: A propositional formula– Example: (p ∨ q) ∧ (¬p ∨ ¬q) ∧ (p ∨ ¬q)• Such a formula is satisfiable if there exists an assignment of (boolean)values to the variables in the formula such that the formula evaluatesto true– Example: The above formula is satisfied by setting p to true and qto false• Goal: Determine whether the given formula is satisfiable– The satisfiability solver that we develop produces a satisfyingassignment when the given formula is satisfiableTheory in Programming Practice, Plaxton, Fall 2005Conjunctive Normal Form (CNF)• A propositional formula is said to be in CNF if it is the conjunction(AND) of a number of clauses, where each clause is the disjunction(OR) of a number of literals, and each literal is either a variable or itsnegation– Example: (p ∨ q) ∧ (¬p ∨ ¬q) ∧ (p ∨ ¬q)• Theorem: Any boolean formula of length n can be converted to alogically equivalent CNF formula of length that is polynomial (in fact,linear) in n• Henceforth, we assume that the input formula is in CNFTheory in Programming Practice, Plaxton, Fall 2005Complexity of the Boolean Satisfiability Problem• The boolean satisfiability problem is NP-complete– Thousands of such NP-complete problems have been identified inthe literature– A polynomial-time algorithm for one NP-complete problem impliespolynomial-time algorithms for all of them– It is widely believed that NP-complete problems requiresuperpolynomial (e.g., exponential) time to solve• In practice, heuristic satisfiability solvers such as Chaff are able to solvefairly large problem instances– Such solvers are applied in a wide variety of application domainsTheory in Programming Practice, Plaxton, Fall 2005The Davis-Putnam Procedure• Let f denote the input formula, and let p denote a variable in f• Let fpdenote f with all occurrences of the literal ¬p removed, andwith all clauses containing the literal p removed– There is a satisfying assignment for f with p set to true if and onlyif fpis satisfiable• Let f¬pbe defined similarly– There is a satisfying assignment for f with p set to false if and onlyif f¬pis satisfiable• The formula f is satisfiable if and only if fpor f¬pis satisfiable• This suggests a recursive procedure– Heuristics may be used to select p and to prioritize the set ofremaining recursive subproblemsTheory in Programming Practice, Plaxton, Fall
View Full Document
Unlocking...