Abstract
In this work, we improve on existing work that studied the relationship between the proof system of modern SAT solvers and general resolution. Previous contributions such as those by Beame et al (2004), Hertel et al (2008), and Buss et al (2008) demonstrated that variations on modern clause-learning SAT solvers were as powerful as general resolution. However, the models used in these studies required either extra degrees of non-determinism or a preprocessing step that are not utilized by any state-of-the-art SAT solvers in practice. In this paper, we prove that modern SAT solvers that learn asserting clauses indeed p-simulate general resolution without the need for any additional techniques.
This is a preview of subscription content, log in via an institution to check access.
Preview
Unable to display preview. Download preview PDF.
Similar content being viewed by others
References
Atserias, A., Fichte, J.K., Thurley, M.: Clause-learning algorithms with many restarts and bounded-width resolution. In: SAT 2009 (to appear, 2009)
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)
Bayardo, R.J.J., Schrag, R.C.: Using CSP look-back techniques to solve real-world SAT instances. In: Proceedings of AAAI 1997, pp. 203–208 (1997)
Beame, P., Kautz, H., Sabharwal, A.: Towards understanding and harnessing the potential of clause learning. JAIR 22, 319–351 (2004)
Buss, S.R., Hoffmann, J., Johannsen, J.: Resolution trees with lemmas: Resolution refinements that characterize DLL algorithms with clause learning. Logical Methods in Computer Science 4, 4 (2008)
Cook, S.A., Reckhow, R.A.: The relative efficiency of propositional proof systems. J. Symb. Log. 44(1), 36–50 (1979)
Davis, M., Logemann, G., Loveland, D.: A machine program for theorem-proving. Commun. ACM 5(7), 394–397 (1962)
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)
Gomes, C.P., Selman, B., Crato, N.: Heavy-tailed distributions in combinatorial search. In: Smolka, G. (ed.) CP 1997. LNCS, vol. 1330, pp. 121–135. Springer, Heidelberg (1997)
Hertel, A.P., Bacchus, F., Pitassi, T., Van Gelder, A.: Clause learning can effectively p-simulate general propositional resolution. In: Proc. of AAAI 2008, pp. 283–290 (2008)
Huang, J.: The effect of restarts on the efficiency of clause learning. In: Proc. of IJCAI 2007, pp. 2318–2323 (2007)
Marques-Silva, J.P., Sakallah, K.A.: GRASP - A New Search Algorithm for Satisfiability. In: Proceedings of ICCAD 1996, pp. 220–227 (1996)
Moskewicz, M., Madigan, C., Zhao, Y., Zhang, L., Malik, S.: Chaff: Engineering an efficient sat solver. In: Proceedings of DAC 2001 (June 2001)
Pipatsrisawat, K., Darwiche, A.: Width-based restart policies for clause-learning satisfiability solvers. In: Proceedings of SAT 2009 (to appear, 2009)
Pipatsrisawat, K., Darwiche, A.: Rsat 2.0: Sat solver description. Tech. Rep. D–153, Automated Reasoning Group, Comp. Sci. Department, UCLA (2007)
Pipatsrisawat, K., Darwiche, A.: A new clause learning scheme for efficient unsatisfiability proofs. In: Proceedings of AAAI 2008, pp. 1481–1484 (2008)
Robinson, J.A.: A machine-oriented logic based on the resolution principle. J. ACM 12(1), 23–41 (1965)
Sang, T., Beame, P., Kautz, H.: Heuristics for fast exact model counting. In: Bacchus, F., Walsh, T. (eds.) SAT 2005. LNCS, vol. 3569, pp. 226–240. Springer, Heidelberg (2005)
Van Gelder, A.: Pool resolution and its relation to regular resolution and dpll with clause learning. In: Sutcliffe, G., Voronkov, A. (eds.) LPAR 2005. LNCS (LNAI), vol. 3835, pp. 580–594. Springer, Heidelberg (2005)
Zhang, L., Madigan, C.F., Moskewicz, M.W., Malik, S.: Efficient conflict driven learning in boolean satisfiability solver. In: ICCAD 2001, pp. 279–285 (2001)
Author information
Authors and Affiliations
Editor information
Editors and Affiliations
Rights and permissions
Copyright information
© 2009 Springer-Verlag Berlin Heidelberg
About this paper
Cite this paper
Pipatsrisawat, K., Darwiche, A. (2009). On the Power of Clause-Learning SAT Solvers with Restarts. In: Gent, I.P. (eds) Principles and Practice of Constraint Programming - CP 2009. CP 2009. Lecture Notes in Computer Science, vol 5732. Springer, Berlin, Heidelberg. https://doi.org/10.1007/978-3-642-04244-7_51
Download citation
DOI: https://doi.org/10.1007/978-3-642-04244-7_51
Publisher Name: Springer, Berlin, Heidelberg
Print ISBN: 978-3-642-04243-0
Online ISBN: 978-3-642-04244-7
eBook Packages: Computer ScienceComputer Science (R0)