Date of Award

Spring 1-1-2011

Document Type

Dissertation

Degree Name

Doctor of Philosophy (PhD)

Department

Electrical, Computer & Energy Engineering

First Advisor

Fabio Somenzi

Second Advisor

Aaron Bradley

Third Advisor

Michael Lightner

Abstract

The satisfiability (SAT) of a propositional formula is the decision problem to determine whether there is a satisfying assignment that can make the formula true or not. In the past few years, many successful SAT solvers based on the David-Putnam-Logemann-Loveland (DPLL) procedure [DP60, DLL62, MS99, MMZ+01, ES03] for formulae in conjunctive normal form (CNF) have been developed. Since the deduction procedure of DPLL is sound but not complete, its effects depend on which formula is selected to represent the input function. CNF transformations are among the most effective techniques to improve quality of the input formula by either simplifying clauses [ES03, EB05,|SE05, ZKKSV06, HS07, HS09] or learning new ones [MS99]. Specifically, effective CNF transformations can help SAT solvers to be sped up by allowing them to do more deductions and less enumerations.

In my dissertation, I characterize existing transformations in terms of their impact on the deductive power of the formula and their effects on the proof conciseness, that is, the sizes of the implication graphs. I also present two new techniques that try to increase deductive power. The first is a check performed during the computation of resolvents. The second is a new preprocessing algorithm based on distillation that combines simplification and increase of deductive power. Most current SAT solvers apply resolution at various stages to derive new clauses or simplify existing ones. The former happens during conflict analysis, while the latter is usually done during preprocessing. I show how subsumption of the operands by the resolvent can be inexpensively detected during resolution; I then discuss how this detection is used to improve three stages of the SAT solver: variable elimination, clause distillation, and conflict analysis. The on-the-fly subsumption check is easily integrated in a SAT solver. In particular, it is compatible with strong conflict analysis and the generation of unsatisfiability proofs. Experiments show the effectiveness of the new techniques.

SAT solvers also benefit from clauses learned by the DPLL procedure, even though they are by definition redundant. In addition to those derived from conflicts, the clauses learned by dominator analysis during the deduction procedure tend to produce smaller implication graphs and sometimes increase the deductive power of the input CNF formula. I extend dominator analysis with an efficient self-subsumption check. I also show how the information collected by dominator analysis can be used to detect redundancies in the satisfied clauses and, more importantly, how it can be used to produce supplemental conflict clauses. I characterize these transformations in terms of deductive power and proof conciseness. Experiments show that the main advantage of dominator analysis and its extensions lies in improving proof conciseness.

Share

COinS