Abstract
Randomized algorithms for deciding satisfiability were shown to be effective in solving problems with thousands of variables. However, these algorithms are not complete. That is, they provide no guarantee that a satisfying assignment, if one exists, will be found. Thus, when studying randomized algorithms, there are two important characteristics that need to be considered: the running time and, even more importantly, the accuracy — a measure of likelihood that a satisfying assignment will be found, provided one exists. In fact, we argue that without a reference to the accuracy, the notion of the running time for randomized algorithms is not well-defined. In this paper, we introduce a formal notion of accuracy. We use it to define a concept of the running time. We use both notions to study the random walk strategy GSAT algorithm. We investigate the dependence of accuracy on properties of input formulas such as clause-to-variable ratio and the number of satisfying assignments. We demonstrate that the running time of GSAT grows exponentially in the number of variables of the input formula for randomly generated 3-CNF formulas and for the formulas encoding 3- and 4-colorability of graphs.
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
S. Arnborg and A. Proskurowski. Linear time algorithms for NP-hard problems restricted to partial k-trees. Discrete Appl. Math., 23:11–24, 1989.
James M. Crawford and Larry D. Auton. Experimental results on the crossover point in satisfiability problems. In AAAI-93, 1993.
[CFG+96]_Dave Clark, Jeremy Frank, Ian Gent, Ewan MacIntyre, Neven Tomov, and Toby Walsh. Local search and the number of solutions. In Proceeding of CP-96, 1996.
Cyungki Cha and Kazuo Iwama. Performance test of local search algorithms using new types of random CNF formulas. In Proceedings of IJCAI, 1995.
O. Dubois, P. Andre, Y. Boufkhad, and J. Carlier. SAT versus UNSAT. DIMACS Cliques, Coloring and Satisfiability, 26, 1996.
M. Davis and H. Putnam. A computing procedure for quantification theory. Journal of Association for Computing Machines, 7, 1960.
Jon W. Freeman. Hard random 3-SAT problems and the davis-putnam procedure. Artificial Intelligence, 81, 1996.
Ian P. Gent and Toby Walsh. Unsatisfied variables in local search. In Proceedings of AISB-95, 1995.
David Johnson, Cecilia Aragon, Lyle McGeoch, and Catherine Schevon. Optimization by simulated annealing: An experimental evaluation; part ii, graph coloring and number partitioning. Operations Research, 39(3), May–June 1991.
Henry A. Kautz and Bart Selman. Planning as satisfiability. In Proceedings of the 10th European Conference on Artificial Intelligence, Vienna, Austria, 1992.
Bertrand Mazure, Lakhdar Saís, and Éric Grégoire. Tabu search for SAT. In Proceedings of the Fourteenth National Conference on Artificial Intelligence (AAAI-97). MIT Press, July 1997.
David Mitchell, Bart Selman, and Hector Levesque. Hard and easy distributions of SAT problems. In Proceedings of the Tenth National Conference on Artificial Intelligence (AAAI-92), July 1992.
Andrew J. Parkes and Joachim P. Walser. Tuning local search for satisfiability testing. In Proceeding of the Thirteen National Conference on Artificial Intelligence(AAAI-96), pages 356–362, 1996.
Bart Selman and Henry A. Kautz. Domain-independent extensions to GSAT: Solving large structured satisfiability problems. In Proceedings of IJCAI-93, 1993.
Bart Selman, Henry A. Kautz, and Bram Cohen. Noise strategies for improving local search. In Proceedings of the Twelfth National Conference on Artificial Intelligence (AAAI-94), 1994.
Bart Selman, Henry A. Kautz, and Bram Cohen. Local search strategies for satisfiability. DIMACS Cliques, Coloring and Satisfiability, 26, 1996.
Bart Selman, Hector Levesque, and David Mitchell. A new method for solving hard satisfiability problems. In Proccedings of the Tenth National Conference on Artificial Intelligence (AAAI-92), July 1992.
William M. Spears. Simulated annealing for hard satisfiability problems. DIMACS Cliques, Coloring and Satisfiability, 26, 1996.
Author information
Authors and Affiliations
Editor information
Editors and Affiliations
Rights and permissions
Copyright information
© 1999 Springer-Verlag Berlin Heidelberg
About this paper
Cite this paper
East, D., Truszczyński, M. (1999). On the Accuracy and Running Time of GSAT. In: Barahona, P., Alferes, J.J. (eds) Progress in Artificial Intelligence. EPIA 1999. Lecture Notes in Computer Science(), vol 1695. Springer, Berlin, Heidelberg. https://doi.org/10.1007/3-540-48159-1_4
Download citation
DOI: https://doi.org/10.1007/3-540-48159-1_4
Published:
Publisher Name: Springer, Berlin, Heidelberg
Print ISBN: 978-3-540-66548-9
Online ISBN: 978-3-540-48159-1
eBook Packages: Springer Book Archive