Abstract
The restart strategy can improve the effectiveness of SAT solvers for satisfiable problems. In 2002, we proposed the so-called random jump strategy, which outperformed the restart strategy in most experiments. One weakness shared by both the restart strategy and the random jump strategy is the ineffectiveness for unsatisfiable problems: A job which can be finished by a SAT solver in one day cannot not be finished in a couple of days if either strategy is used by the same SAT solver. In this paper, we propose a simple and effective technique which makes the random jump strategy as effective as the original SAT solvers. The technique works as follows: When we jump from the current position to another position, we remember the skipped search space in a simple data structure called “guiding path”. If the current search runs out of search space before running out of the allotted time, the search can be recharged with one of the saved guiding paths and continues. Because the overhead of saving and loading guiding paths is very small, the SAT solvers is as effective as before for unsatisfiable problems when using the proposed technique.
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
Baptista, L., Margues-Silva, J.P.: Using Randomization and Learning to Solve Hard Real-World Instances of Satisfiability. In: Dechter, R. (ed.) CP 2000. LNCS, vol. 1894, Springer, Heidelberg (2000)
Baptista, L., Lynce, I., Marques-Silva, J.P.: Complete Search Restart Strategies for Satisfiability. In: IJCAI 2001 Workshop on Stochastic Search Algorithms (IJCAI-SSA) (August 2001)
Bayardo, R., Schrag, R.: Using CSP look-back techniques to solve exceptionally hard SAT instances. In: Proceedings of CP 1996 (1996)
Bennett, F.E., Du, B., Zhang, H.: Conjugate orthogonal diagonal latin squares with missing subsquares. In: Wallis, W. (ed.) Designs 2002: Further Computational and Constructive Design Theory, ch. 2, Kluwer Academic Publishers, Boston (2003)
Bennett, F.E., Zhang, H.: Latin squares with self-orthogonal conjugates. Discrete Mathematics 284, 45–55 (2004)
Bohm, M., Speckenmeyer, E.: A fast parallel SAT-solver – Efficient Workload Balancing (1994), URL: http://citeseer.ist.psu.edu/51782.html
Davis, M., Putnam, H.: A computing procedure for quantification theory. Journal of the ACM 7, 201–215 (1960)
Davis, M., Logemann, G., Loveland, D.: A machine program for theorem-proving. Communications of the Association for Computing Machinery 5(7), 394–397 (1962)
Feldman, Y., Dershowitz, N., Hanna, Z.: Parallel Multithreaded Satisfiability Solver: Design and Implementation. Electronic Notes in Theoretical Computer Science 128, 75–90 (2005)
Lynce, I., Baptista, L., Marques-Silva, J.P.: Stochastic Systematic Search Algorithms for Satisfiability. In: LICS Workshop on Theory and Applications of Satisfiability Testing (LICS-SAT) (June 2001)
Gomes, C.P., Selman, B., Crato, C.: Heavy-tailed Distributions in Combinatorial Search. In: Smolka, G. (ed.) CP 1997. LNCS, vol. 1330, pp. 121–135. Springer, Heidelberg (1997)
Marques-Silva, J.P., Sakallah, K.A.: GRASP: A Search Algorithm for Propositional Satisfiability. IEEE Transactions on Computers 48(5), 506–521 (1999)
Xu, Y., Zhang, H.: Frame self-orthogonal Mendelsohn triple systems. Acta Mathematica Sinica 20(5), 913–924 (2004)
Zhang, H.: Specifying Latin squares in propositional logic. In: Veroff, R. (ed.) Automated Reasoning and Its Applications, Essays in honor of Larry Wos, ch. 6, MIT Press, Cambridge (1997)
Zhang, H.: SATO: An efficient propositional prover. In: McRobbie, M.A., Slaney, J.K. (eds.) CADE 1996. LNCS, vol. 1104, pp. 308–312. Springer, Heidelberg (1996)
Zhang, H.: A random jump strategy for combinatorial search. In: Proc. of Sixth International Symposium on Artificial Intelligence and Mathematics, Fort Lauderdale, FL (2002)
Zhang, H.: A complete random jump strategy with guiding paths (full version) (2006), http://www.cs.uiowa.edu/~hzhang/crandomjump.pdf
Zhang, H., Bonacina, M.P., Hsiang, H.: PSATO: a distributed propositional prover and its application to quasigroup problems. Journal of Symbolic Computation 21, 543–560 (1996)
Zhang, H., Bennett, F.E.: Existence of some (3,2,1)–HCOLS and (3,2,1)–HCOLS. J. of Combinatoric Mathematics and Combinatoric Computing 22, 13–22 (1996)
Zhang, H., Stickel, M.: Implementing the Davis-Putnam method. J. of Automated Reasoning 24, 277–296 (2000)
Zhu, L., Zhang, H.: Completing the spectrum of r-orthogonal latin squares. Discrete Mathematics 258 (2003)
Author information
Authors and Affiliations
Editor information
Editors and Affiliations
Rights and permissions
Copyright information
© 2006 Springer-Verlag Berlin Heidelberg
About this paper
Cite this paper
Zhang, H. (2006). A Complete Random Jump Strategy with Guiding Paths. In: Biere, A., Gomes, C.P. (eds) Theory and Applications of Satisfiability Testing - SAT 2006. SAT 2006. Lecture Notes in Computer Science, vol 4121. Springer, Berlin, Heidelberg. https://doi.org/10.1007/11814948_12
Download citation
DOI: https://doi.org/10.1007/11814948_12
Publisher Name: Springer, Berlin, Heidelberg
Print ISBN: 978-3-540-37206-6
Online ISBN: 978-3-540-37207-3
eBook Packages: Computer ScienceComputer Science (R0)