{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2025,3,19]],"date-time":"2025-03-19T15:19:58Z","timestamp":1742397598506},"reference-count":21,"publisher":"Elsevier BV","license":[{"start":{"date-parts":[[2001,6,1]],"date-time":"2001-06-01T00:00:00Z","timestamp":991353600000},"content-version":"tdm","delay-in-days":0,"URL":"https:\/\/www.elsevier.com\/tdm\/userlicense\/1.0\/"}],"content-domain":{"domain":[],"crossmark-restriction":false},"short-container-title":["Electronic Notes in Discrete Mathematics"],"published-print":{"date-parts":[[2001,6]]},"DOI":"10.1016\/s1571-0653(04)00322-1","type":"journal-article","created":{"date-parts":[[2005,4,9]],"date-time":"2005-04-09T13:34:04Z","timestamp":1113053644000},"page":"190-204","source":"Crossref","is-referenced-by-count":13,"special_numbering":"C","title":["Stochastic Systematic Search Algorithms for Satisfiability"],"prefix":"10.1016","volume":"9","author":[{"given":"I.","family":"Lynce","sequence":"first","affiliation":[]},{"given":"L.","family":"Baptista","sequence":"additional","affiliation":[]},{"given":"J.","family":"Marques-Silva","sequence":"additional","affiliation":[]}],"member":"78","reference":[{"key":"10.1016\/S1571-0653(04)00322-1_BIB1","article-title":"Complete search restart strategies for satisfiability","author":"Baptista","year":"2001","journal-title":"IJCAI Workshop on Stochastic Search Algorithms (IJACI-SSA)"},{"key":"10.1016\/S1571-0653(04)00322-1_BIB2","article-title":"Using randomization and learning to solve hard real-world instances of satisfiability","author":"Baptista","year":"2000","journal-title":"Proceedings of the International Conference on Principles and Practice of Constraint Programming"},{"key":"10.1016\/S1571-0653(04)00322-1_BIB3","first-page":"203","article-title":"Using CSP look-back techniques to solve real-world SAT instances","author":"Bayardo","year":"1997","journal-title":"Proceedings of the National Conference on Artificial Intelligence"},{"key":"10.1016\/S1571-0653(04)00322-1_BIB4","doi-asserted-by":"crossref","first-page":"394","DOI":"10.1145\/368273.368557","article-title":"A machine program for theorem-proving","volume":"5","author":"Davis","year":"1962","journal-title":"Communications of the Association for Computing Machinery"},{"key":"10.1016\/S1571-0653(04)00322-1_BIB5","doi-asserted-by":"crossref","first-page":"201","DOI":"10.1145\/321033.321034","article-title":"A computing procedure for quantification theory","volume":"7","author":"Davis","year":"1960","journal-title":"Journal of the Association for Computing Machinery"},{"key":"10.1016\/S1571-0653(04)00322-1_BIB6","doi-asserted-by":"crossref","first-page":"25","DOI":"10.1613\/jair.1","article-title":"Dynamic backtracking","volume":"1","author":"Ginsberg","year":"1993","journal-title":"Journal of Artificial Intelligence Research"},{"key":"10.1016\/S1571-0653(04)00322-1_BIB7","doi-asserted-by":"crossref","first-page":"226","DOI":"10.1016\/B978-1-4832-1452-8.50117-2","article-title":"GSAT and dynamic backtracking","author":"Ginsberg","year":"1994","journal-title":"Proceedings of the International Conference on Principles of Knowledge and Reasoning"},{"key":"10.1016\/S1571-0653(04)00322-1_BIB8","article-title":"Boosting combinatorial search through randomization","author":"Gomes","year":"1998","journal-title":"Proceedings of the National Conference on Artificial Intelligence"},{"key":"10.1016\/S1571-0653(04)00322-1_BIB9","unstructured":"D.S. Johnson and M.A. Trick, editors. Second DIMACS Implementation Challenge. American Mathematical Society, 1993. (DIMACS SAT instances available from URL ftp:\/\/Dimacs.Rutgers.EDU\/pub\/challenge\/sat\/benchmarks\/cnf)."},{"key":"10.1016\/S1571-0653(04)00322-1_BIB10","doi-asserted-by":"crossref","DOI":"10.1007\/BFb0017450","article-title":"Look-ahead versus look-back for satisfiability problems","author":"Li","year":"1997","journal-title":"Proceedings of International Conference on Principles and Practice of Constraint Programming"},{"key":"10.1016\/S1571-0653(04)00322-1_BIB11","article-title":"Unrestricted backtracking algorithms for satisfiability","author":"Lynce","year":"2001","journal-title":"AAAI 2001 Fall Symposium \u2014 Using Uncertainty within Computation"},{"key":"10.1016\/S1571-0653(04)00322-1_BIB12","doi-asserted-by":"crossref","first-page":"220","DOI":"10.1109\/ICCAD.1996.569607","article-title":"GRASP: A new search algorithm for satisfiability","author":"Marques-Silva","year":"1996","journal-title":"Proceedings of the ACM\/IEEE International Conference on Computer-Aided Design"},{"issue":"5","key":"10.1016\/S1571-0653(04)00322-1_BIB13","doi-asserted-by":"crossref","first-page":"506","DOI":"10.1109\/12.769433","article-title":"GRASP-A search algorithm for prepositional satisfiability","volume":"48","author":"Marques-Silva","year":"1999","journal-title":"IEEE Transactions on Computers"},{"key":"10.1016\/S1571-0653(04)00322-1_BIB14","first-page":"321","article-title":"Evidence of invariants in local search","author":"McAllester","year":"1997","journal-title":"Proceedings of the National Conference on Artificial Intelligence"},{"key":"10.1016\/S1571-0653(04)00322-1_BIB15","article-title":"Engineering an efficient SAT solver","author":"Moskewicz","year":"2001","journal-title":"Proceedings of the Design Automation Conference"},{"key":"10.1016\/S1571-0653(04)00322-1_BIB16","first-page":"337","article-title":"A hybrid search architecture applied to hard random 3-sat and low-autocorrelation binary sequences","author":"Prestwich","year":"2000","journal-title":"Proceedings of the International Conference on Principles and Practice of Constraint Programming"},{"key":"10.1016\/S1571-0653(04)00322-1_BIB17","article-title":"Restart-repair and learning: An empirical study of single solution 3-sat problems","author":"Richards","year":"1997","journal-title":"CP Workshop on the Theory and Practice of Dynamic Constraint Satisfaction"},{"key":"10.1016\/S1571-0653(04)00322-1_BIB18","first-page":"290","article-title":"Domain-independent extensions to GSAT: Solving large structured satisfiability problems","author":"Selman","year":"1993","journal-title":"Proceedings of the International Joint Conference on Artificial Intelligence"},{"key":"10.1016\/S1571-0653(04)00322-1_BIB19","doi-asserted-by":"crossref","first-page":"37","DOI":"10.1007\/3-540-48153-2_5","article-title":"Superscalar processor verification using efficient reductions from the logic of equality with uninterpreted functions to prepositional logic","author":"Velev","year":"1999","journal-title":"Proceedings of Correct Hardware Design and Verification Methods, LNCS 1703"},{"key":"10.1016\/S1571-0653(04)00322-1_BIB20","first-page":"155","article-title":"A rearrangement search strategy for determining prepositional satisfiability","author":"Zabih","year":"1988","journal-title":"Proceedings of the National Conference on Artificial Intelligence"},{"key":"10.1016\/S1571-0653(04)00322-1_BIB21","first-page":"272","article-title":"SATO: An efficient prepositional prover","author":"Zhang","year":"1997","journal-title":"Proceedings of the International Conference on Automated Deduction"}],"container-title":["Electronic Notes in Discrete Mathematics"],"original-title":[],"language":"en","link":[{"URL":"https:\/\/api.elsevier.com\/content\/article\/PII:S1571065304003221?httpAccept=text\/xml","content-type":"text\/xml","content-version":"vor","intended-application":"text-mining"},{"URL":"https:\/\/api.elsevier.com\/content\/article\/PII:S1571065304003221?httpAccept=text\/plain","content-type":"text\/plain","content-version":"vor","intended-application":"text-mining"}],"deposited":{"date-parts":[[2019,2,10]],"date-time":"2019-02-10T15:48:49Z","timestamp":1549813729000},"score":1,"resource":{"primary":{"URL":"https:\/\/linkinghub.elsevier.com\/retrieve\/pii\/S1571065304003221"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2001,6]]},"references-count":21,"alternative-id":["S1571065304003221"],"URL":"https:\/\/doi.org\/10.1016\/s1571-0653(04)00322-1","relation":{},"ISSN":["1571-0653"],"issn-type":[{"type":"print","value":"1571-0653"}],"subject":[],"published":{"date-parts":[[2001,6]]}}}