Abstract
In this paper, an efficient heuristic allowing one to localize inconsistent kernels in propositional knowledge‐bases is described. Then, it is shown that local search techniques can boost the performance of logically complete methods for SAT. More precisely, local search techniques can be used to guide the branching strategy of logically complete techniques like Davis and Putnam's one, giving rise to significant performance improvements, in particular when addressing locally inconsistent problems. Moreover, this approach appears very competitive in the context of consistent SAT instances, too.
Similar content being viewed by others
Explore related subjects
Discover the latest articles, news and stories from top researchers in related subjects.References
P. Cheeseman, B. Kanefsky and W.M. Taylor, Where the really hard problems are, in: Proc. IJCAI-91(1991) pp. 163-169.
V. Chvátal and E. Szemerédi, Many hard examples for resolution, Journal of the ACM 33(4) (1988) 759-768.
S. Cook, The complexity of theorem-proving procedures, in: Proc. 3rd Ann. ACM Symp. on Theory of Computing(1971) pp. 151-158.
S. Cook, A short proof of the pigeon hole principle using extended resolution, SIGACT News 8 (1976) 28-32.
J.M. Crawford, Solving satisfiability problems using a combination of systematic and local search, in: Working Notes of the DIMACS Workshop on Maximum Clique, Graph Coloring, and Satisfiability(1993).
M. Davis and H. Putnam, A computing procedure for quantification theory, Journal of the ACM 7 (1960) 201-215.
DIMACS, Second challenge organized by the Center for Discrete Mathematics and Computer Science of Rutgers University (1993). The benchmarks used in our tests can be obtained by anonymous ftp from Rutgers University DIMACS Center: ftp://dimacs.rutgers.edu/pub/challenge/ sat/benchmarks/cnf.
O. Dubois, P. André, Y. Boufkhad and J. Carlier, SAT versus UNSAT, in: Working Notes of the DIMACS Workshop on Maximum Clique, Graph Coloring, and Satisfiability(1993).
O. Dubois and J. Carlier, Probabilistic approach to the satisfiability problem, Theoretical Computer Science 81 (1991) 65-75.
J. Franco and M. Paull, Probabilistic analysis of the Davis and Putnam procedure for solving the satisfiability problem, Discrete Applied Mathematics 5 (1983) 77-87.
I.P. Gent and T. Walsh, Towards an understanding of hill-climbing procedures for SAT, in: Proc. AAAI-93(1993) pp. 28-33.
I.P. Gent and T. Walsh, The SAT phase transition, in: Proc. ECAI-94(1994) pp. 105-109.
K. Iwama and E. Miyano, Test-case generation with proved securities, in: Working Notes of the DIMACS Workshop on Maximum Clique, Graph Coloring, and Satisfiability(1993).
B. Mazure, L. Saïs and É. Grégoire, Tabu search for SAT, in: Proc. AAAI-97(July 1997) pp. 281-285. A preliminary version appeared as: TWSAT: a new local search algorithm for SAT. Performance and analysis, in: CP95 Workshop on Studying and Solving Really Hard Problems, Cassis, France, September 1995.
D. Mitchell, B. Selman and H. Levesque, Hard and easy distributions of SAT problems, in: Proc. AAAI-92(1992) pp. 459-465.
A. Rauzy, On the complexity of the Davis and Putnam's procedure on some polynomial sub-classes of SAT, LaBRI Technical Report 806-94, Université de Bordeaux 1 (1994).
B. Selman, H. Levesque and D. Mitchell, A new method for solving hard satisfiability problems, in: Proc. AAAI-92(1992) pp. 440-446.
B. Selman, H.A. Kautz and B. Cohen, Local search strategies for satisfiability testing, in: Working Notes of the DIMACS Workshop on Maximum Clique, Graph Coloring, and Satisfiability(1993).
G.S. Tseitin, On the complexity of derivations in propositional calculus, in: Structures in Constructive Mathematics, Part II, ed. A.O. Slisenko (1968) pp. 115-125.
Author information
Authors and Affiliations
Rights and permissions
About this article
Cite this article
Mazure, B., Saïs, L. & Grégoire, É. Boosting complete techniques thanks to local search methods. Annals of Mathematics and Artificial Intelligence 22, 319–331 (1998). https://doi.org/10.1023/A:1018999721141
Issue Date:
DOI: https://doi.org/10.1023/A:1018999721141