Abstract
In this paper we generalize a heuristic that we have introduced previously for solving efficiently random 3-SAT formulae. Our heuristic is based on the notion of backbone, searching variables belonging to local backbones of a formula. This heuristic was limited to 3-SAT formulae. In this paper we generalize this heuristic by introducing a sub-heuristic called a re-normalization heuristic in order to handle formulae with various clause lengths and particularly hard random k-sat formulae with k ≥ 3 . We implemented this new general heuristic in our previous program cnfs, a classical dpll algorithm, renamed kcnfs. We give experimental results which show that kcnfs outperforms by far the best current complete solvers on any random k-SAT formula for k ≥ 3.
This is a preview of subscription content, log in via an institution to check access.
Access this chapter
Tax calculation will be finalised at checkout
Purchases are for personal use only
Preview
Unable to display preview. Download preview PDF.
References
Dubois, O., Dequen, G.: A Backbone Search Heuristic for Efficient Solving of Hard 3-SAT Formulae. In: Proc. of the 17th Internat. Joint Conf. on Artificial Intelligence, Seattle, 248–253 (2001)
Monasson, R., Zecchina, R., Kirkpatrick, S., Selman, B., Troyansky, L.: Determining Computational Complexity from Characteristic ‘Phase Transitions’. Nature 400, 133–137 (1999)
Davis, M., Putnam, H.: A Computing Procedure for Quantification Theory. Journal Association for Computing Machine, 201–215 (1960)
Davis, M., Logemann, G., Loveland, D.: A Machine Program for Theorem- Proving. Journal Association for Computing Machine, 394–397 (1962)
Li, C.M., Anbulagan: Heuristics Based on Unit Propagation for Satisfiability Problems. In: Proc. of the 15th Internat. Joint Conf. on Artificial Intelligence, Nagoya (Japan), IJCAI, 366–371 (1997)
Freeman, J.W.: Hard Random 3-SAT Problems and the Davis-Putnam Procedure. Artificial Intelligence 81, 183–198 (1996)
Dubois, O., Andre, P., Boufkhad, Y., Carlier, J.: SAT versus UNSAT. DIMACS Series in Discr. Math. and Theor. Computer Science, pp. 415–436 (1993)
Li, C.M.: A Constraint-Based Approach to Narrow Search Trees for Satisfiability. Information Processing Letters 71, 75–80 (1999)
Kullman, O.: Heuristics for SAT algorithms: A systematic study. In: Extended abstract for the Second workshop on the satisfiability problem, SAT 1998 (1998)
Moskewicz, M.W., Madigan, C.F., Zhao, Y., Zhang, L., Malik, S.: Chaff: Engineering an Efficient SAT Solver. In: Proceedings of the 38th Design Automation Conference, DAC 2001 (2001)
Zhang, H.: SATO. An Efficient Propositional Prover. In: McCune, W. (ed.) CADE 1997. LNCS, vol. 1249, pp. 272–275. Springer, Heidelberg (1997)
Selman, B., Kautz, H.A., Cohen, B.: Noise Strategies for Improving Local Search. In: Proc. of the 12th National Conf. on Artificial Intelligence, Menlo Park, CA, USA, vol. 1, pp. 337–343. AAAI Press, Menlo Park (1994)
Braunstein, A., Mezard, M., Zecchina. R.: Survey propagation: an algorithm for satisfiability. arXiv - cond-mat/0207194 (2002)
Li, C.M., Gerard, S.: On the Limit of Branching Rules for Hard Random Unsatisfiable 3-SAT. In: Proc. of European Conf. on Artificial Intelligence, ECAI, pp. 98–102 (2000)
Biroli, G., Monasson, R., Weigt, M.: A variational description of the ground state structure in random satisfiability problems. Eur. Phys. J. B 14 551 (2000)
Mezard, M., Parisi, G., Zecchina, R.: Analytic and algorithmic solutions of random satisfiability problems. Science 297 (2002)
Author information
Authors and Affiliations
Editor information
Editors and Affiliations
Rights and permissions
Copyright information
© 2004 Springer-Verlag Berlin Heidelberg
About this paper
Cite this paper
Dequen, G., Dubois, O. (2004). kcnfs: An Efficient Solver for Random k-SAT Formulae. In: Giunchiglia, E., Tacchella, A. (eds) Theory and Applications of Satisfiability Testing. SAT 2003. Lecture Notes in Computer Science, vol 2919. Springer, Berlin, Heidelberg. https://doi.org/10.1007/978-3-540-24605-3_36
Download citation
DOI: https://doi.org/10.1007/978-3-540-24605-3_36
Publisher Name: Springer, Berlin, Heidelberg
Print ISBN: 978-3-540-20851-8
Online ISBN: 978-3-540-24605-3
eBook Packages: Springer Book Archive