Abstract
The dominant propositional satisfiability solvers of the past decade use a technique often called conflict-driven clause learning (cdcl), although nomenclature varies. The first half of the decade concentrated on deriving the best clause from the conflict graph that the technique constructs, also with much emphasis on speed. In the second half of the decade efforts have emerged to exploit other information that is derived by the technique as a by-product of generating the conflict graph and learning a conflict clause. The main thrust has been to strengthen the conflict clause by eliminating some of its literals, a process often called conflict-clause minimization, but more accurately described as conflict-clause width reduction, or strengthening.
This paper first introduces implication sequences as a general framework to represent all the information derived by the CDCL technique, some of which is not represented in the conflict graph. Then the paper analyzes the structure of this information. The first main result is that any conflict clause that is a logical consequence of an implication sequence may be derived by a particularly simple form of resolution, known as linear input regular. A key observation needed for this result is that the set of clauses in any implication sequence is Horn-renamable. The second main result is that, given an implication sequence, and a clause C derived (learned) from it, it is NP-hard to find a minimum-cardinality subset of C that is also derivable. This is in sharp contrast to the known fact that such a minimum subset can be found quickly if the derivation is restricted to using only clauses in the conflict graph.
This is a preview of subscription content, log in via an institution.
Buying options
Tax calculation will be finalised at checkout
Purchases are for personal use only
Learn about institutional subscriptionsPreview
Unable to display preview. Download preview PDF.
References
Audemard, G., Bordeaux, L., Hamadi, Y., Jabbour, S., Sais, L.: A generalized framework for conflict analysis. In: Kleine Büning, H., Zhao, X. (eds.) SAT 2008. LNCS, vol. 4996, pp. 21–27. Springer, Heidelberg (2008)
Biere, A.: Picosat essentials. J. Satisfiability, Boolean Modeling and Comp. 4, 75–97 (2008)
Beame, P., Kautz, H., Sabharwal, A.: Towards understanding and harnessing the potential of clause learning. J. Artificial Intelligence Research 22 (2004)
Chang, C.-L., Lee, R.C.-T.: Symbolic Logic and Mechanical Theorem Proving (1973)
Davis, M., Logemann, G., Loveland, D.: A machine program for theorem-proving. Communications of the ACM 5, 394–397 (1962)
Davis, M., Putnam, H.: A computing procedure for quantification theory. Journal of the Association for Computing Machinery 7, 201–215 (1960)
Eén, N., Sörensson, N.: An extensible SAT-solver. In: Giunchiglia, E., Tacchella, A. (eds.) SAT 2003. LNCS, vol. 2919, pp. 502–518. Springer, Heidelberg (2004)
Eén, N., Sörensson, N.: MiniSat v.1.13 – a SAT solver with conflict-clause minimization. Poster at SAT (2005)
Han, H., Somenzi, F.: On-the-fly clause improvement. In: Kullmann, O. (ed.) SAT 2009. LNCS, vol. 5584, pp. 209–222. Springer, Heidelberg (2009)
Henschen, L.J., Wos, L.: Unit refutations and Horn sets. JACM 21 (1974)
Kleine Büning, H., Lettmann, T.: Propositional Logic: Deduction and Algorithms (1999)
Loveland, D.W.: Automated Theorem Proving: a Logical Basis. North-Holland, Amsterdam (1978)
Moskewicz, M., Madigan, C., Zhao, Y., Zhang, L., Malik, S.: Chaff: Engineering an efficient SAT solver. In: 39th Design Automation Conference (June 2001)
Marques-Silva, J.P., Sakallah, K.A.: GRASP–a search algorithm for propositional satisfiability. IEEE Transactions on Computers 48, 506–521 (1999)
Pipatsrisawat, K., Darwiche, A.: A new clause learning scheme for efficient unsatisfiability proofs. In: AAAI (2008)
Sörensson, N., Biere, A.: Minimizing learned clauses. In: Kullmann, O. (ed.) SAT 2009. LNCS, vol. 5584, pp. 237–243. Springer, Heidelberg (2009)
Van Gelder, A.: Improved conflict-clause minimization leads to improved propositional proof traces. In: Kullmann, O. (ed.) SAT 2009. LNCS, vol. 5584, pp. 141–146. Springer, Heidelberg (2009)
Zhang, L., Madigan, C., Moskewicz, M., Malik, S.: Efficient conflict driven learning in a boolean satisfiability solver. In: ICCAD (November 2001)
Author information
Authors and Affiliations
Editor information
Editors and Affiliations
Rights and permissions
Copyright information
© 2011 Springer-Verlag Berlin Heidelberg
About this paper
Cite this paper
Van Gelder, A. (2011). Generalized Conflict-Clause Strengthening for Satisfiability Solvers. In: Sakallah, K.A., Simon, L. (eds) Theory and Applications of Satisfiability Testing - SAT 2011. SAT 2011. Lecture Notes in Computer Science, vol 6695. Springer, Berlin, Heidelberg. https://doi.org/10.1007/978-3-642-21581-0_26
Download citation
DOI: https://doi.org/10.1007/978-3-642-21581-0_26
Publisher Name: Springer, Berlin, Heidelberg
Print ISBN: 978-3-642-21580-3
Online ISBN: 978-3-642-21581-0
eBook Packages: Computer ScienceComputer Science (R0)