{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2026,3,31]],"date-time":"2026-03-31T07:09:12Z","timestamp":1774940952226,"version":"3.50.1"},"reference-count":18,"publisher":"Springer Science and Business Media LLC","issue":"1-4","license":[{"start":{"date-parts":[[2004,12,31]],"date-time":"2004-12-31T00:00:00Z","timestamp":1104451200000},"content-version":"tdm","delay-in-days":0,"URL":"http:\/\/www.springer.com\/tdm"}],"content-domain":{"domain":[],"crossmark-restriction":false},"short-container-title":["Ann Math Artif Intell"],"published-print":{"date-parts":[[2005,1]]},"DOI":"10.1007\/s10472-005-0425-5","type":"journal-article","created":{"date-parts":[[2005,3,2]],"date-time":"2005-03-02T19:19:42Z","timestamp":1109791182000},"page":"137-152","source":"Crossref","is-referenced-by-count":10,"title":["Efficient data structures for backtrack search SAT solvers"],"prefix":"10.1007","volume":"43","author":[{"given":"In\u00eas","family":"Lynce","sequence":"first","affiliation":[]},{"given":"Jo\u00e3o","family":"Marques-Silva","sequence":"additional","affiliation":[]}],"member":"297","published-online":{"date-parts":[[2004,12,31]]},"reference":[{"key":"425_CR1","unstructured":"F. Bacchus, Exploiting the computational tradeoff of more reasoning and less searching, in: Proceedings of Fifth International Symposium on Theory and Applications of Satisfiability Testing (2002) pp. 7\u201316."},{"key":"425_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, ed. R. Dechter, Lecture Notes in Computer Science, Vol. 1894 (2000) pp. 489\u2013494.","DOI":"10.1007\/3-540-45349-0_36"},{"key":"425_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 (1997) pp. 203\u2013208."},{"key":"425_CR4","doi-asserted-by":"crossref","unstructured":"O. Coudert, On solving covering problems, in: Proceedings of the ACM\/IEEE Design Automation Conference (1996) pp. 197\u2013202.","DOI":"10.1145\/240518.240555"},{"key":"425_CR5","doi-asserted-by":"crossref","first-page":"394","DOI":"10.1145\/368273.368557","volume":"5","author":"M. Davis","year":"1996","unstructured":"M. Davis, G. Logemann and D. Loveland, A machine program for theorem-proving, Communications of the Association for Computing Machinery 5 (1996) 394\u2013397.","journal-title":"Communications of the Association for Computing Machinery"},{"key":"425_CR6","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 (1960) 201\u2013215.","journal-title":"Journal of the Association for Computing Machinery"},{"key":"425_CR7","unstructured":"A.V. Gelder and Y.K. Tsuji, Satisfiability testing with more reasoning and less guessing, in: Second DIMACS Implementation Challenge, eds. D.S. Johnson and M.A. Trick (American Mathematical Society, 1993)."},{"key":"425_CR8","unstructured":"C.P. Gomes, B. Selman and H. Kautz, Boosting combinatorial search through randomization, in: Proceedings of the National Conference on Artificial Intelligence (1998) pp. 431\u2013437."},{"key":"425_CR9","unstructured":"J.F. Groote and J.P. Warners, The propositional formula Checker Heerhugo, in: Proceedings of SAT 2000, eds. I. Gent, H. van Maaren and T. Walsh (IOS Press, 2000) pp. 261\u2013281."},{"key":"425_CR10","unstructured":"C.M. Li and Anbulagan, Look-ahead versus look-back for satisfiability problems, in: Proceedings of the International Conference on Principles and Practice of Constraint Programming (1997) pp. 341\u2013355."},{"key":"425_CR11","doi-asserted-by":"crossref","unstructured":"J.P. Marques-Silva, Algebraic simplification techniques for propositional satisfiability, in: International Conference on Principles and Practice of Constraint Programming, ed. R. Dechter, Lecture Notes in Computer Science, Vol. 1894 (2000) pp. 537\u2013542.","DOI":"10.1007\/3-540-45349-0_45"},{"key":"425_CR12","doi-asserted-by":"crossref","unstructured":"J.P. Marques-Silva and K.A. Sakallah, GRASP: A new search algorithm for satisfiability, in: Proceedings of the ACM\/IEEE International Conference on Computer-Aided Design (1996) pp. 220\u2013227.","DOI":"10.1109\/ICCAD.1996.569607"},{"key":"425_CR13","doi-asserted-by":"crossref","unstructured":"J.P. Marques-Silva and K.A. Sakallah Boolean satisfiability in electronic design automation, in: Proceedings of the ACM\/IEEE Design Automation Conference (2000) pp. 675\u2013680.","DOI":"10.1145\/337292.337611"},{"key":"425_CR14","unstructured":"N. Moskewicz, C. Madigan, Y. Zhao, L. Zhang and S. Malik, Engineering an efficient SAT solver, in: Proceedings of the Design Automation Conference (2001) pp. 530\u2013535."},{"key":"425_CR15","unstructured":"B. Selman and H. Kautz, Domain-independent extensions to GSAT: Solving large structured satisfiability problems, in: Proceedings of the International Joint Conference on Artificial Intelligence (1993) pp. 290\u2013295."},{"key":"425_CR16","unstructured":"R. Zabih and D.A. McAllester, A rearrangement search strategy for determining propositional satisfiability, in: Proceedings of the National Conference on Artificial Intelligence (1988) pp. 155\u2013160."},{"key":"425_CR17","doi-asserted-by":"crossref","unstructured":"H. Zhang, SATO: An efficient propositional prover, in: Proceedings of the International Conference on Automated Deduction (1997) pp. 272\u2013275.","DOI":"10.1007\/3-540-63104-6_28"},{"key":"425_CR18","unstructured":"H. Zhang and M. Stickel, Implementing the Davis-Putnam method, in: Proceedings of SAT 2000, eds. I. Gent, H. van Maaren and T. Walsh (IOS Press, 2000) pp. 309\u2013326."}],"container-title":["Annals of Mathematics and Artificial Intelligence"],"original-title":[],"language":"en","link":[{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/s10472-005-0425-5.pdf","content-type":"application\/pdf","content-version":"vor","intended-application":"text-mining"},{"URL":"http:\/\/link.springer.com\/article\/10.1007\/s10472-005-0425-5\/fulltext.html","content-type":"text\/html","content-version":"vor","intended-application":"text-mining"},{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/s10472-005-0425-5","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2019,5,29]],"date-time":"2019-05-29T17:51:48Z","timestamp":1559152308000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/s10472-005-0425-5"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2004,12,31]]},"references-count":18,"journal-issue":{"issue":"1-4","published-print":{"date-parts":[[2005,1]]}},"alternative-id":["425"],"URL":"https:\/\/doi.org\/10.1007\/s10472-005-0425-5","relation":{},"ISSN":["1012-2443","1573-7470"],"issn-type":[{"value":"1012-2443","type":"print"},{"value":"1573-7470","type":"electronic"}],"subject":[],"published":{"date-parts":[[2004,12,31]]}}}