{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2025,10,28]],"date-time":"2025-10-28T03:10:41Z","timestamp":1761621041712},"publisher-location":"Berlin, Heidelberg","reference-count":23,"publisher":"Springer Berlin Heidelberg","isbn-type":[{"type":"print","value":"9783540208518"},{"type":"electronic","value":"9783540246053"}],"content-domain":{"domain":[],"crossmark-restriction":false},"short-container-title":[],"published-print":{"date-parts":[[2004]]},"DOI":"10.1007\/978-3-540-24605-3_5","type":"book-chapter","created":{"date-parts":[[2010,7,29]],"date-time":"2010-07-29T08:50:35Z","timestamp":1280393435000},"page":"53-68","source":"Crossref","is-referenced-by-count":6,"title":["A Local Search SAT Solver Using an Effective Switching Strategy and an Efficient Unit Propagation"],"prefix":"10.1007","author":[{"given":"Xiao Yu","family":"Li","sequence":"first","affiliation":[]},{"given":"Matthias F.","family":"Stallmann","sequence":"additional","affiliation":[]},{"given":"Franc","family":"Brglez","sequence":"additional","affiliation":[]}],"member":"297","reference":[{"key":"5_CR1","unstructured":"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"},{"key":"5_CR2","unstructured":"Hoos, H., Stuetzle, T.: SATLIB: An online resource for research on SAT (2000), For more information see http:\/\/www.satlib.org"},{"key":"5_CR3","unstructured":"Le Berre, D.: SAT Live! Up-to-date links for the SATisfiability problem (2003), For more information see http:\/\/www.satlive.org"},{"key":"5_CR4","unstructured":"Simon, L.: Sat-Ex: The experimentation web site around the satisfiability (2003), For more information see www.lri.fr\/~simon\/satex\/satex.php3"},{"key":"5_CR5","doi-asserted-by":"crossref","unstructured":"Hoos, H.H., St\u00fctzle, T.: Local Search Algorithms for SAT: An Empirical Evaluation. Journal Of Automated Reasoning\u00a024 (2000)","DOI":"10.1023\/A:1006350622830"},{"key":"5_CR6","unstructured":"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\/"},{"key":"5_CR7","unstructured":"McAllester, D.A., Selman, B., Kautz, H.A.: Evidence for invariants in local search. In: AAAI\/IAAI, pp. 321\u2013326 (1997)"},{"key":"5_CR8","first-page":"46","volume-title":"Proceedings of AAAI 1994","author":"B. Selman","year":"1994","unstructured":"Selman, B., Kautz, H., Cohen, B.: Noise Strategies for Improving Local Search. In: Proceedings of AAAI 1994, pp. 46\u201351. MIT Press, Cambridge (1994)"},{"key":"5_CR9","unstructured":"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)"},{"key":"5_CR10","doi-asserted-by":"crossref","unstructured":"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","DOI":"10.1145\/378239.379017"},{"key":"5_CR11","volume-title":"Implementing the Davis-Putnam method","author":"H. Zhang","year":"2000","unstructured":"Zhang, H., Stickel, M.E.: Implementing the Davis-Putnam method. Kluwer Academic Publishers, Dordrecht (2000)"},{"key":"5_CR12","unstructured":"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\/"},{"key":"#cr-split#-5_CR13.1","doi-asserted-by":"crossref","unstructured":"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);","DOI":"10.1007\/s10472-005-0417-5"},{"key":"#cr-split#-5_CR13.2","unstructured":"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\/"},{"key":"5_CR14","doi-asserted-by":"crossref","unstructured":"Johnson, D.: A Theoretician\u2019s Guide to the Experimental Analysis of Algorithms, pp. 215\u2013250 (2002)","DOI":"10.1090\/dimacs\/059\/11"},{"key":"5_CR15","unstructured":"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)"},{"key":"5_CR16","unstructured":"Hirsch, E., Kojevnikov, A.: UnitWalk Home Page, See http:\/\/logic.pdmi.ras.ru\/~arist\/UnitWalk\/"},{"key":"5_CR17","unstructured":"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)"},{"key":"5_CR18","doi-asserted-by":"crossref","unstructured":"Zhang, H.: SATO: An efficient propositional prover. In: Conference on Automated Deduction, pp. 272\u2013275 (1997), Version 3.2 of SATO is available at ftp:\/\/cs.uiowa.edu\/pub\/hzhang\/sato\/sato.tar.gz","DOI":"10.1007\/3-540-63104-6_28"},{"key":"5_CR19","unstructured":"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\/"},{"key":"5_CR20","unstructured":"Hoos, H.: SATLIB-The Satisfiability Library (2003), See, http:\/\/www.satlib.org"},{"key":"5_CR21","unstructured":"Hirsch, E.: Random generator hgen2 of satisfiable formulas in 3-CNF, See http:\/\/logic.pdmi.ras.ru\/~hirsch\/benchmarks\/hgen2.html"},{"key":"5_CR22","unstructured":"Velev, M.N.: Benchmark suite SSS1.0., See http:\/\/www.ece.cmu.edu\/~mvelev"}],"container-title":["Lecture Notes in Computer Science","Theory and Applications of Satisfiability Testing"],"original-title":[],"link":[{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/978-3-540-24605-3_5","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2021,11,2]],"date-time":"2021-11-02T07:56:01Z","timestamp":1635839761000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/978-3-540-24605-3_5"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2004]]},"ISBN":["9783540208518","9783540246053"],"references-count":23,"URL":"https:\/\/doi.org\/10.1007\/978-3-540-24605-3_5","relation":{},"ISSN":["0302-9743","1611-3349"],"issn-type":[{"type":"print","value":"0302-9743"},{"type":"electronic","value":"1611-3349"}],"subject":[],"published":{"date-parts":[[2004]]}}}