Abstract
We study an algorithm for the SAT problem which is based on the Davis and Putnam procedure. The main idea is to increase the application of the unit clause rule during the search. When there is no unit clause in the set of clauses, our method tries to produce one occuring in the current subset of binary clauses. A literal deduction algorithm is implemented and applied at each branching node of the search tree. This method AVAL is a combination of the Davis and Putnam principle and of the mono-literal deduction procedure. Its efficiency comes from the average complexity of the literal deduction procedure which is linear in the number of variables. The method is called “AVAL” (avalanch) because of its behaviour on hard random SAT problems. When solving these instances, an avalanche of mono-literals is deduced after the first success of literal production and from that point, the search effort is reduced to unit propagations, thus completing the remaining part of enumeration in polynomial time.
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.
Similar content being viewed by others
References
Y. Boufkhad. Aspects probabilistes et algorithmiques du problème de satisfaisabilité. PhD thesis, Univertsité de Jussieu, 1996.
V. Chvátal and B. Reed. Mick Gets Some (the odds are on this side). In 33rd IEEE Symposium on Foundation of Computers Science, 1992.
M. Davis and H. Putnam. A computing procedure for quantification theory. JACM, 1960.
O. Dubois, P. André, Y. Boufkhad, and J. Carlier. Sat versus unsat. AMS, DIMACS Series in Discrete Mathematics and Theoretical Computer Science, 26, 1996.
O. Dubois and Y. Boufkhad. A General Upper Bound for the Satisfiability Threshold of random r-sat formulae. Journal of Algorithms, 1996.
J.W. Freeman. Improvements to Propositionnai Satisfiability Search Algorithms. PhD thesis, Univ. of Pennsylvania, Philadelphia, 1995.
J.W. Freeman. Hard random 3-SAT problems and the Davis-Putnam procedure. Artificial Intelligence, 81(2):183–198, 1996.
E. Friegut. Necessary and sufficient conditions for sharp threholds of graphs properties and the k-sat problem. Technical report, Institute of Mathematics, The Hebrew University of Jerusalem, 1997.
A. Goerdt. A threshold for unsatisfiability. In Mathematical Foundations of Computer Science, volume 629, pages 264–274. Springer, 1992.
Chu Min Li and Anbulagan. Heuristics based on unit propagation for satisfiability problem. In proceedings of IJCAI 97, 1997.
Chu Min Li and Anbulagan. Look-Ahead Versus Look-Back for Satisfiability Problems. In proceedings of CP97, pages 341–355, 1997.
W.V. Quine. Methods of logics. Henry Holt, New York, 1950.
B. Selman, H. Levesque, and D. Mitchell. A New Method for Solving Hard Satisfiability Problems. In Proceedings of the 10th National Conference on Artificial Intelligence AAAI’94, 1994.
H. Zhang. SATO: An efficient prepositional prover. In Proceedings of the 14th International Conference on Automated deduction, 1997.
Author information
Authors and Affiliations
Editor information
Editors and Affiliations
Rights and permissions
Copyright information
© 2000 Springer-Verlag Berlin Heidelberg
About this paper
Cite this paper
Audemard, G., Benhamou, B., Siegel, P. (2000). AVAL: An Enumerative Method for SAT. In: Lloyd, J., et al. Computational Logic — CL 2000. CL 2000. Lecture Notes in Computer Science(), vol 1861. Springer, Berlin, Heidelberg. https://doi.org/10.1007/3-540-44957-4_25
Download citation
DOI: https://doi.org/10.1007/3-540-44957-4_25
Published:
Publisher Name: Springer, Berlin, Heidelberg
Print ISBN: 978-3-540-67797-0
Online ISBN: 978-3-540-44957-7
eBook Packages: Springer Book Archive