Abstract
Advances in local-search SAT solvers have traditionally been presented in the context of local search solvers only. The most recent and rather comprehensive comparisons between UnitWalk and several versions of WalkSAT demonstrate that neither solver dominates on all benchmarks. QingTing2 (a ‘dragonfly’ in Mandarin) is a SAT solver script that relies on a novel switching strategy to invoke one of the two local search solvers: WalkSAT or QingTing1. The local search solver QingTing1 implements the UnitWalk algorithm with a new unit-propagation technique. The experimental methodology we use not only demonstrates the effectiveness of the switching strategy and the efficiency of the new unit-propagation implementation – it also supports, on the very same instances, statistically significant performance evaluation between local search and other state-of-the-art DPLL-based SAT solvers. The resulting comparisons show a surprising pattern of solver dominance, completely unanticipated when we began this work.
This is a preview of subscription content, log in via an institution.
Buying options
Tax calculation will be finalised at checkout
Purchases are for personal use only
Learn about institutional subscriptionsPreview
Unable to display preview. Download preview PDF.
References
Le Berre, D., Simon, L.: SAT Solver Competition. In: conjunction with 2003 SAT Conference (May 2003), For more information see http://www.satlive.org/SATCompetition/2003/comp03report/index.html
Hoos, H., Stuetzle, T.: SATLIB: An online resource for research on SAT (2000), For more information see http://www.satlib.org
Le Berre, D.: SAT Live! Up-to-date links for the SATisfiability problem (2003), For more information see http://www.satlive.org
Simon, L.: Sat-Ex: The experimentation web site around the satisfiability (2003), For more information see www.lri.fr/~simon/satex/satex.php3
Hoos, H.H., Stützle, T.: Local Search Algorithms for SAT: An Empirical Evaluation. Journal Of Automated Reasoning 24 (2000)
Selman, B., Kautz, H.: WalkSAT Homepage: Stochastic Local Search for Satisfiability (2002), The source code is available at http://www.cs.washington.edu/homes/kautz/walksat/
McAllester, D.A., Selman, B., Kautz, H.A.: Evidence for invariants in local search. In: AAAI/IAAI, pp. 321–326 (1997)
Selman, B., Kautz, H., Cohen, B.: Noise Strategies for Improving Local Search. In: Proceedings of AAAI 1994, pp. 46–51. MIT Press, Cambridge (1994)
Hirsch, E., Kojevnikov, A.: UnitWalk: A new SAT solver that uses local search guided by unit clause elimination. In: Electronic Proceedings of Fifth International Symposium on the Theory and Applications of Satisfiability Testing (2002)
Moskewicz, M., Madigan, C., Zhao, Y., Zhang, L., Malik, S.: Chaff: Engineering an efficient SAT solver. In: IEEE/ACM Design Automation Conference, DAC (2001), Version 1.0 of Chaff is available at www.ee.princeton.edu/~chaff/zchaff/zchaff.2001.2.17.src.tar.gz
Zhang, H., Stickel, M.E.: Implementing the Davis-Putnam method. Kluwer Academic Publishers, Dordrecht (2000)
Brglez, F., Stallmann, M.F., Li, X.Y.: SATbed: An Environment For Reliable Performance Experiments with SAT Instance Classes and Algorithms. In: Proceedings of SAT 2003, Sixth International Symposium on the Theory and Applications of Satisfiability Testing, S. Margherita Ligure - Portofino, Italy, May 5-8 (2003), For a revised version, see http://www.cbl.ncsu.edu/publications/
Brglez, F., Li, X.Y., Stallmann, M.: On SAT Instance Classes and a Method for Reliable Performance Experiments with SAT Solvers. Annals of Mathematics and Artificial Intelligence, Special Issue on Satisfiability Testing (2003); Submitted to AMAI as the revision of the paper published at the Fifth International Symposium on the Theory and Applications of Satisfiability Testing, Cincinnati, Ohio, USA (May 2002), Available at http://www.cbl.ncsu.edu/publications/
Johnson, D.: A Theoretician’s Guide to the Experimental Analysis of Algorithms, pp. 215–250 (2002)
Zhang, H., Stickel, M.E.: An efficient algorithm for unit propagation. In: Proceedings of the Fourth International Symposium on Artificial Intelligence and Mathematics (AI-MATH 1996), Fort Lauderdale, Florida, USA (1996)
Hirsch, E., Kojevnikov, A.: UnitWalk Home Page, See http://logic.pdmi.ras.ru/~arist/UnitWalk/
Lynce, I., Marques-Silva, J.: Efficient data structure for backtrack search sat solvers. In: Fifth International Symposium on the Theory and Applications of Satisfiability Testing (2002)
Zhang, H.: SATO: An efficient propositional prover. In: Conference on Automated Deduction, pp. 272–275 (1997), Version 3.2 of SATO is available at ftp://cs.uiowa.edu/pub/hzhang/sato/sato.tar.gz
Brglez, F., Li, X.Y., Stallmann, M.: The Role of a Skeptic Agent in Testing and Benchmarking of SAT Algorithms. In: Fifth International Symposium on the Theory and Applications of Satisfiability Testing (May 2002), Available at http://www.cbl.ncsu.edu/publications/
Hoos, H.: SATLIB-The Satisfiability Library (2003), See, http://www.satlib.org
Hirsch, E.: Random generator hgen2 of satisfiable formulas in 3-CNF, See http://logic.pdmi.ras.ru/~hirsch/benchmarks/hgen2.html
Velev, M.N.: Benchmark suite SSS1.0., See http://www.ece.cmu.edu/~mvelev
Author information
Authors and Affiliations
Editor information
Editors and Affiliations
Rights and permissions
Copyright information
© 2004 Springer-Verlag Berlin Heidelberg
About this paper
Cite this paper
Li, X.Y., Stallmann, M.F., Brglez, F. (2004). A Local Search SAT Solver Using an Effective Switching Strategy and an Efficient Unit Propagation. In: Giunchiglia, E., Tacchella, A. (eds) Theory and Applications of Satisfiability Testing. SAT 2003. Lecture Notes in Computer Science, vol 2919. Springer, Berlin, Heidelberg. https://doi.org/10.1007/978-3-540-24605-3_5
Download citation
DOI: https://doi.org/10.1007/978-3-540-24605-3_5
Publisher Name: Springer, Berlin, Heidelberg
Print ISBN: 978-3-540-20851-8
Online ISBN: 978-3-540-24605-3
eBook Packages: Springer Book Archive