Efficient local search for very large-scale satisfiability problems

ABSTRACT

The satisfiability problem (SAT) is a fundamental problem in mathematical logic, inference, automated reasoning, and computing theory. In this correspondence, we report the results of applying local search techniques to solve the satisfiability problem. While a traditional resolution-based algorithm is not able to handle even moderately sized inference problems, a local search algorithm, tested through years of real program execution, is capable of computing very large-scale inference problems with fast, robust convergence. On a workstation computer, for example, it is able to solve a satisfiability problem with 50,000 clauses and 5,000 variables in a few seconds.

REFERENCES

• 1: Stephen A. Cook, The complexity of theorem-proving procedures, Proceedings of the third annual ACM symposium on Theory of computing, p.151-158, May 03-05, 1971, Shaker Heights, Ohio, United States [doi>10.1145/800157.805047]
• 2: Thomas T. Cormen , Charles E. Leiserson , Ronald L. Rivest, Introduction to algorithms, MIT Press, Cambridge, MA, 1990
• 3: V. Cêrny. A thermodynamical approach to the travelling salesman problem: An efficient simulation algorithm. Technical report, Institute of Physics and Biophysics, Comenius University, Bratislava, 1982.
• 4: Martin Davis , Hilary Putnam, A Computing Procedure for Quantification Theory, Journal of the ACM (JACM), v.7 n.3, p.201-215, July 1960 [doi>10.1145/321033.321034]
• 5: N. Dershowitz, J. Hsiang, N. Josephson, and D. Plaisted. Associative-commutative rewriting. In <i>Proceedings of IJCAI,</i> pages 940--944, 1983.
• 6: Michael R. Garey , David S. Johnson, Computers and Intractability: A Guide to the Theory of NP-Completeness, W. H. Freeman & Co., New York, NY, 1979
• 7: A. Goldberg, P. W. Purdom, and C. A. Brown, Average time analysis of simplified davis-putnam procedures. <i>Information Processing Letters,</i> 15(2):72--75, 6 Sept. 1982.
• 8: David E. Goldberg, Genetic Algorithms in Search, Optimization and Machine Learning, Addison-Wesley Longman Publishing Co., Inc., Boston, MA, 1989
• 9: J. Gu. How to solve Very Large-Scale Satisfiability (VLSS) problems. 1988.
• 10: J. Gu. Benchmarking SAT algorithms. Technical Report UCECE-TR-90--002, Oct. 1990.
• 11: J. Gu and X. Huang. Implementation and performance of the SAT14 algorithm. Submitted for publication. Feb. 1991.
• 12: Jieh Hsiang, Refutational theorem proving using term-rewriting systems, Artificial Intelligence, v.25 n.3, p.255-300, March 1985 [doi>10.1016/0004-3702(85)90074-8]
• 13: X. Huang and J. Gu. A quantitative solution for constraint satisfaction. Submitted for publication. March 1991.
• 14: P.C. Jackson Jr. Heuristic search algorithms for the satisfiability problem. Submitted to the third IEEE TAI Conference, Jul. 1991.
• 15: S. Kirkpatrick, Jr. C.D. Gelat, and M.P. Vecchi. Optimization by simulated annealing. <i>Science,</i> 220:671--680, 1983.
• 16: S. Minton, M.D. Johnston, A.B. Philips, and P. Laird. Solving large-scale constraint satisfaction and scheduling problems using a heuristic repair method. In <i>Proceedings of AAA190,</i> pages 17--24, Aug. 1990.
• 17: N. J. Nilsson, Principles of artificial intelligence, Morgan Kaufmann Publishers Inc., San Francisco, CA, 1980
• 18: B.M. Schwartzschild. Statistical mechanics algorithm for monte carlo optimization. <i>Physics Today,</i> 35:17--19, 1982.
• 19: M.J. Shensa. A computational structure for the propositional calculus. In <i>Proceedings of IJCAI,</i> pages 384--388, 1989.
• 20: P. Siegel. <i>Representation et Utilization de la Connaissances en Calcul Propositionel.</i> PhD thesis, University Aix-Marseille 11, 1987.
• 21: R. Sosic and J. Gu. How to search for million queens. Technical Report UUCS-TR-88--008, Dept. of Computer Science, Univ. of Utah, Feb. 1988.
• 22: Rok Sosic , Jun Gu, A polynomial time algorithm for the N-Queens problem, ACM SIGART Bulletin, v.1 n.3, p.7-11, Oct. 1990 [doi>10.1145/101340.101343]
• 23: Rok Sosic , Jun Gu, 3,000,000 Queens in less than one minute, ACM SIGART Bulletin, v.2 n.2, p.22-24, April 1991 [doi>10.1145/122319.122325]
• 24: Patrick Henry Winston, Artificial intelligence (2nd ed.), Addison-Wesley Longman Publishing Co., Inc., Boston, MA, 1984

INDEX TERMS

Primary Classification:
  F. Theory of Computation
  F.2 ANALYSIS OF ALGORITHMS AND PROBLEM COMPLEXITY
      F.2.2 Nonnumerical Algorithms and Problems
          Subjects: Sorting and searching

Additional Classification:
  I. Computing Methodologies
  I.2 ARTIFICIAL INTELLIGENCE
      I.2.8 Problem Solving, Control Methods, and Search
          Subjects: Heuristic methods; Graph and tree search strategies

General Terms:
Algorithms, Design, Experimentation, Measurement, Performance