Research Note Decomposing SAT Problems into Connected Components.pdfVIP

Journal on Satisfiability, Boolean Modeling and Computation 2 (2006) 191-198 Research Note Decomposing SAT Problems into Connected Components Armin Biere armin.biere@jku.at Carsten Sinz carsten.sinz@jku.at Institute for Formal Models and Verification, Johannes Kepler University, Linz, Austria Abstract Many SAT instances can be decomposed into connected components either initially after preprocessing or during the solution phase when new unit conflict clauses are learned. This observation allows components to be solved individually. We present a technique to handle components within a GRASP like SAT solver without requiring much change to the solver. Results obtained when applying our implementation in the SAT solver COMPSAT to a number of realistic examples show that components really do occur in practice. We also provide some evidence that component structure can be used to improve performance. Keywords: SAT, connected components Submitted October 2005; revised January 2006; published February 2006 Introduction It has often been observed that an analysis of the graph structure of a SAT problem may help to speed up SAT solving [1, 5, 13, 14]. The most basic type of structure is connectivity, where we view the variables of a formula in CNF as nodes of the graph and the clauses act as hyper edges. If a CNF can be decomposed into connected components according to this definition, then the components form independent SAT problems, and accordingly the whole CNF becomes satisfiable if and only if each component is satisfiable individually. In this paper we substantiate the hypothesis brought forward in [15, 16] that connected compon