{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2025,10,27]],"date-time":"2025-10-27T20:30:38Z","timestamp":1761597038645,"version":"3.40.3"},"publisher-location":"Berlin, Heidelberg","reference-count":26,"publisher":"Springer Berlin Heidelberg","isbn-type":[{"type":"print","value":"9783540009863"},{"type":"electronic","value":"9783540366072"}],"license":[{"start":{"date-parts":[[2003,1,1]],"date-time":"2003-01-01T00:00:00Z","timestamp":1041379200000},"content-version":"tdm","delay-in-days":0,"URL":"https:\/\/www.springernature.com\/gp\/researchers\/text-and-data-mining"},{"start":{"date-parts":[[2003,1,1]],"date-time":"2003-01-01T00:00:00Z","timestamp":1041379200000},"content-version":"vor","delay-in-days":0,"URL":"https:\/\/www.springernature.com\/gp\/researchers\/text-and-data-mining"}],"content-domain":{"domain":["link.springer.com"],"crossmark-restriction":false},"short-container-title":[],"published-print":{"date-parts":[[2003]]},"DOI":"10.1007\/3-540-36607-5_11","type":"book-chapter","created":{"date-parts":[[2007,7,3]],"date-time":"2007-07-03T15:21:25Z","timestamp":1183476085000},"page":"144-158","update-policy":"https:\/\/doi.org\/10.1007\/springer_crossmark_policy","source":"Crossref","is-referenced-by-count":5,"title":["The Effect of Nogood Recording in DPLL-CBJ SAT Algorithms"],"prefix":"10.1007","author":[{"given":"In\u00eas","family":"Lynce","sequence":"first","affiliation":[]},{"given":"Jo\u00e3o","family":"Marques-Silva","sequence":"additional","affiliation":[]}],"member":"297","published-online":{"date-parts":[[2003,4,15]]},"reference":[{"key":"11_CR1","doi-asserted-by":"crossref","unstructured":"K. Apt. Some remarks on boolean constraint propagation. In New Trends in Constraints, number 1865 in Lecture Notes in Artificial Intelligence, pages 91\u2013107. Springer, 2000.","DOI":"10.1007\/3-540-44654-0_5"},{"key":"11_CR2","doi-asserted-by":"crossref","unstructured":"R. Bayardo Jr. and R. Schrag. Using CSP look-back techniques to solve exceptionally hard SAT instances. In Proceedings of the International Conference on Principles and Practice of Constraint Programming, pages 46\u201360, August 1996.","DOI":"10.1007\/3-540-61551-2_65"},{"key":"11_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, July 1997."},{"key":"11_CR4","doi-asserted-by":"crossref","unstructured":"C. Bessi\u00e8re and J. C. R\u00e9gin. MAC and combined heuristics: two reasons to forsake FC (and CBJ?) on hard problems. In Proceedings of the International Conference on Principles and Practice of Constraint Programming, pages 61\u201375, August 1996.","DOI":"10.1007\/3-540-61551-2_66"},{"key":"11_CR5","doi-asserted-by":"crossref","first-page":"53","DOI":"10.1613\/jair.788","volume":"14","author":"X. Chen","year":"2001","unstructured":"X. Chen and P. van Beek. Conflict-directed backjumping revisited. Journal of Artificial Intelligence Research, 14:53\u201381, 2001.","journal-title":"Journal of Artificial Intelligence Research"},{"key":"11_CR6","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 theorem-proving. Communications of the Association for Computing Machinery, 5:394\u2013397, July 1962.","journal-title":"Communications of the Association for Computing Machinery"},{"key":"11_CR7","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, July 1960.","journal-title":"Journal of the Association for Computing Machinery"},{"issue":"3","key":"11_CR8","doi-asserted-by":"publisher","first-page":"273","DOI":"10.1016\/0004-3702(90)90046-3","volume":"41","author":"R. Dechter","year":"1990","unstructured":"R. Dechter. Enhancement schemes for constraint processing: backjumping, learning, and cutset decomposition. Artificial Intelligence, 41(3):273\u2013312, January 1990.","journal-title":"Artificial Intelligence"},{"key":"11_CR9","volume-title":"Performance Measurement and Analysis of Certain Search Algorithms","author":"J. Gaschnig","year":"1979","unstructured":"J. Gaschnig. Performance Measurement and Analysis of Certain Search Algorithms. PhD thesis, Carnegie-Mellon University, Pittsburgh, PA, May 1979."},{"key":"11_CR10","unstructured":"I. Gent. Arc consistency in SAT. In Proceedings of the European Conference on Artificial Intelligence, pages 121\u2013125, July 2002."},{"key":"11_CR11","doi-asserted-by":"crossref","unstructured":"E. Goldberg and Y. Novikov. BerkMin: a fast and robust sat-solver. In Proceedings of the Design and Test in Europe Conference, pages 142\u2013149, March 2002.","DOI":"10.1109\/DATE.2002.998262"},{"key":"11_CR12","doi-asserted-by":"crossref","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, pages 341\u2013355, October 1997.","DOI":"10.1007\/BFb0017450"},{"key":"11_CR13","doi-asserted-by":"crossref","unstructured":"I. Lynce and J. P. Marques-Silva. The effect of nogood recording in MAC-CBJ SAT algorithms. Technical Report RT\/04\/2002, INESC, April 2002.","DOI":"10.1007\/3-540-36607-5_11"},{"issue":"3","key":"11_CR14","doi-asserted-by":"publisher","first-page":"307","DOI":"10.1023\/A:1021264516079","volume":"37","author":"I. Lynce","year":"2003","unstructured":"I. Lynce and J. P. Marques-Silva. An overview of backtrack search satisfiability algorithms. Annals of Mathematics and Artificial Intelligence, 37(3):307\u2013326, March 2003.","journal-title":"Annals of Mathematics and Artificial Intelligence"},{"issue":"1","key":"11_CR15","doi-asserted-by":"publisher","first-page":"99","DOI":"10.1016\/0004-3702(77)90007-8","volume":"8","author":"A. K. Mackworth","year":"1977","unstructured":"A. K. Mackworth. Consistency in networks of relations. Artificial Intelligence, 8(1):99\u2013118, 1977.","journal-title":"Artificial Intelligence"},{"key":"11_CR16","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, pages 220\u2013227, November 1996.","DOI":"10.1109\/ICCAD.1996.569607"},{"key":"11_CR17","doi-asserted-by":"crossref","unstructured":"M. Moskewicz, C. Madigan, Y. Zhao, L. Zhang, and S. Malik. Engineering an efficient SAT solver. In Proceedings of the Design Automation Conference, pages 530\u2013535, June 2001.","DOI":"10.1145\/378239.379017"},{"key":"11_CR18","unstructured":"P. Prosser. Domain filtering can degrade intelligent backjumping search. In Proceedings of the International Joint Conference on Artificial Intelligence, pages 262\u2013267, August 1993."},{"issue":"3","key":"11_CR19","doi-asserted-by":"publisher","first-page":"268","DOI":"10.1111\/j.1467-8640.1993.tb00310.x","volume":"9","author":"P. Prosser","year":"1993","unstructured":"P. Prosser. Hybrid algorithms for the constraint satisfaction problems. Computational Intelligence, 9(3):268\u2013299, August 1993.","journal-title":"Computational Intelligence"},{"key":"11_CR20","series-title":"Technical Report","volume-title":"MAC-CBJ: maintaining arc consistency with conflict-directed backjumping","author":"P. Prosser","year":"1995","unstructured":"P. Prosser. MAC-CBJ: maintaining arc consistency with conflict-directed backjumping. Technical Report 177, University of Strathclyde, Glasgow, Scotland, May 1995."},{"key":"11_CR21","doi-asserted-by":"crossref","unstructured":"D. Sabin and E. Freuder. Contradicting conventional wisdom in constraint satisfaction. In Proceedings of the European Conference on Artificial Intelligence, pages 125\u2013129, August 1994.","DOI":"10.1007\/3-540-58601-6_86"},{"key":"11_CR22","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, pages 290\u2013295, August 1993."},{"key":"11_CR23","doi-asserted-by":"crossref","first-page":"135","DOI":"10.1016\/0004-3702(77)90029-7","volume":"9","author":"R. M. Stallman","year":"1977","unstructured":"R. M. Stallman and G. J. Sussman. Forward reasoning and dependency-directed backtracking in a system for computer-aided circuit analysis. Artificial Intelligence, 9:135\u2013196, October 1977.","journal-title":"Artificial Intelligence"},{"key":"11_CR24","doi-asserted-by":"crossref","unstructured":"T. Walsh. SAT v CSP. In Proceedings of the International Conference on Principles and Practice of Constraint Programming, pages 441\u2013456, September 2000.","DOI":"10.1007\/3-540-45349-0_32"},{"key":"11_CR25","unstructured":"R. Zabih and D. A. McAllester. A rearrangement search strategy for determining propositional satisfiability. In Proceedings of the National Conference on Artificial Intelligence, pages 155\u2013160, July 1988."},{"key":"11_CR26","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","Recent Advances in Constraints"],"original-title":[],"language":"en","link":[{"URL":"https:\/\/link.springer.com\/content\/pdf\/10.1007\/3-540-36607-5_11","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2025,1,18]],"date-time":"2025-01-18T03:58:31Z","timestamp":1737172711000},"score":1,"resource":{"primary":{"URL":"https:\/\/link.springer.com\/10.1007\/3-540-36607-5_11"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2003]]},"ISBN":["9783540009863","9783540366072"],"references-count":26,"URL":"https:\/\/doi.org\/10.1007\/3-540-36607-5_11","relation":{},"ISSN":["0302-9743"],"issn-type":[{"type":"print","value":"0302-9743"}],"subject":[],"published":{"date-parts":[[2003]]},"assertion":[{"value":"15 April 2003","order":1,"name":"first_online","label":"First Online","group":{"name":"ChapterHistory","label":"Chapter History"}}]}}