{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2025,10,28]],"date-time":"2025-10-28T03:09:36Z","timestamp":1761620976643},"publisher-location":"Berlin, Heidelberg","reference-count":15,"publisher":"Springer Berlin Heidelberg","isbn-type":[{"type":"print","value":"9783540430308"},{"type":"electronic","value":"9783540453291"}],"content-domain":{"domain":[],"crossmark-restriction":false},"short-container-title":[],"published-print":{"date-parts":[[2001]]},"DOI":"10.1007\/3-540-45329-6_35","type":"book-chapter","created":{"date-parts":[[2007,10,26]],"date-time":"2007-10-26T02:44:33Z","timestamp":1193366673000},"page":"363-370","source":"Crossref","is-referenced-by-count":3,"title":["Towards Provably Complete Stochastic Search Algorithms for Satisfiability"],"prefix":"10.1007","author":[{"given":"In\u00eas","family":"Lynce","sequence":"first","affiliation":[]},{"given":"Lu\u00eds","family":"Baptista","sequence":"additional","affiliation":[]},{"given":"Jo\u00e3o","family":"Marques-Silva","sequence":"additional","affiliation":[]}],"member":"297","published-online":{"date-parts":[[2002,4,23]]},"reference":[{"key":"35_CR1","unstructured":"L. Baptista, I. Lynce, and J. Marques-Silva. Complete search restart strategies for satisfiability. In IJCAI Workshop on Stochastic Search Algorithms, August 2001."},{"key":"35_CR2","doi-asserted-by":"crossref","unstructured":"L. Baptista and J. P. Marques-Silva. Using randomization and learning to solve hard real-world instances of satisfiability. In International Conference on Principles and Practice of Constraint Programming, pages 489\u2013494, September 2000.","DOI":"10.1007\/3-540-45349-0_36"},{"key":"35_CR3","unstructured":"R. Bayardo Jr. and R. Schrag. Using CSP look-back techniques to solve real-world SAT instances. In Proceedings of the National Conference on Artificial Intelligence, pages 203\u2013208, 1997."},{"key":"35_CR4","doi-asserted-by":"crossref","first-page":"394","DOI":"10.1145\/368273.368557","volume":"5","author":"M. Davis","year":"1962","unstructured":"M. Davis, G. Logemann, and D. Loveland. A machine program for theoremproving. Communications of the Association for Computing Machinery, 5:394\u2013397, July 1962.","journal-title":"Communications of the Association for Computing Machinery"},{"key":"35_CR5","doi-asserted-by":"crossref","first-page":"201","DOI":"10.1145\/321033.321034","volume":"7","author":"M. Davis","year":"1960","unstructured":"M. Davis and H. Putnam. A computing procedure for quantification theory. Journal of the Association for Computing Machinery, 7:201\u2013215, 1960.","journal-title":"Journal of the Association for Computing Machinery"},{"key":"35_CR6","doi-asserted-by":"crossref","unstructured":"M. Ginsberg and D. McAllester. GSAT and dynamic backtracking. In Proceedings of the International Conference on Principles of Knowledge and Reasoning, pages 226\u2013237, 1994.","DOI":"10.1016\/B978-1-4832-1452-8.50117-2"},{"key":"35_CR7","unstructured":"C. P. Gomes, B. Selman, and H. Kautz. Boosting combinatorial search through randomization. In Proceedings of the National Conference on Artificial Intelligence, July 1998."},{"key":"35_CR8","doi-asserted-by":"crossref","unstructured":"I. Lynce, L. Baptista, and J. Marques-Silva. Stochastic systematic search algorithms for satisfiability. In LICS Workshop on Theory and Applications of Satisfiability Testing, June 2001.","DOI":"10.1016\/S1571-0653(04)00322-1"},{"issue":"5","key":"35_CR9","doi-asserted-by":"publisher","first-page":"506","DOI":"10.1109\/12.769433","volume":"48","author":"J. P. Marques-Silva","year":"1999","unstructured":"J. P. Marques-Silva and K. A. Sakallah. GRASP-A search algorithm for propositional satisfiability. IEEE Transactions on Computers, 48(5):506\u2013521, May 1999.","journal-title":"IEEE Transactions on Computers"},{"key":"35_CR10","unstructured":"D. McAllester, B. Selman, and H. Kautz. Evidence of invariants in local search. In Proceedings of the National Conference on Artificial Intelligence, pages 321\u2013326, August 1997."},{"key":"35_CR11","unstructured":"M. Moskewicz, C. Madigan, Y. Zhao, L. Zhang, and S. Malik. Engineering an efficient SAT solver. In Proceedings of the Design Automation Conference, 2001."},{"key":"35_CR12","doi-asserted-by":"crossref","unstructured":"S. Prestwich. A hybrid search architecture applied to hard random 3-sat and lowautocorrelation binary sequences. In Proceedings of the International Conference on Principles and Practice of Constraint Programming, pages 337\u2013352, September 2000.","DOI":"10.1007\/3-540-45349-0_25"},{"key":"35_CR13","unstructured":"E. T. Richards and B. Richards. Restart-repair and learning: An empirical study of single solution 3-sat problems. In CP Workshop on the Theory and Practice of Dynamic Constraint Satisfaction, 1997."},{"key":"35_CR14","series-title":"Lect Notes Comput Sci","first-page":"37","volume-title":"Superscalar processor verification using efficient reductions from the logic of equality with uninterpreted functions to propositional logic","author":"M. N. Velev","year":"1999","unstructured":"M. N. Velev and R. E. Bryant. Superscalar processor verification using efficient reductions from the logic of equality with uninterpreted functions to propositional logic. In Proceedings of Correct Hardware Design and Verification Methods, LNCS 1703, pages 37\u201353, September 1999."},{"key":"35_CR15","doi-asserted-by":"crossref","unstructured":"H. Zhang. SATO: An efficient propositional prover. In Proceedings of the International Conference on Automated Deduction, pages 272\u2013275, July 1997.","DOI":"10.1007\/3-540-63104-6_28"}],"container-title":["Lecture Notes in Computer Science","Progress in Artificial Intelligence"],"original-title":[],"link":[{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/3-540-45329-6_35","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2019,5,4]],"date-time":"2019-05-04T01:06:46Z","timestamp":1556932006000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/3-540-45329-6_35"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2001]]},"ISBN":["9783540430308","9783540453291"],"references-count":15,"URL":"https:\/\/doi.org\/10.1007\/3-540-45329-6_35","relation":{},"ISSN":["0302-9743"],"issn-type":[{"type":"print","value":"0302-9743"}],"subject":[],"published":{"date-parts":[[2001]]}}}