{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2025,3,25]],"date-time":"2025-03-25T14:33:38Z","timestamp":1742913218069,"version":"3.40.3"},"publisher-location":"Cham","reference-count":25,"publisher":"Springer International Publishing","isbn-type":[{"type":"print","value":"9783319180076"},{"type":"electronic","value":"9783319180083"}],"license":[{"start":{"date-parts":[[2015,1,1]],"date-time":"2015-01-01T00:00:00Z","timestamp":1420070400000},"content-version":"tdm","delay-in-days":0,"URL":"http:\/\/www.springer.com\/tdm"},{"start":{"date-parts":[[2015,1,1]],"date-time":"2015-01-01T00:00:00Z","timestamp":1420070400000},"content-version":"vor","delay-in-days":0,"URL":"http:\/\/www.springer.com\/tdm"}],"content-domain":{"domain":["link.springer.com"],"crossmark-restriction":false},"short-container-title":[],"published-print":{"date-parts":[[2015]]},"DOI":"10.1007\/978-3-319-18008-3_15","type":"book-chapter","created":{"date-parts":[[2015,4,15]],"date-time":"2015-04-15T07:32:51Z","timestamp":1429083171000},"page":"215-230","update-policy":"https:\/\/doi.org\/10.1007\/springer_crossmark_policy","source":"Crossref","is-referenced-by-count":1,"title":["BDD-Guided Clause Generation"],"prefix":"10.1007","author":[{"given":"Brian","family":"Kell","sequence":"first","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Ashish","family":"Sabharwal","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Willem-Jan","family":"van Hoeve","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]}],"member":"297","published-online":{"date-parts":[[2015,4,16]]},"reference":[{"issue":"1","key":"15_CR1","doi-asserted-by":"publisher","first-page":"4","DOI":"10.1016\/j.disopt.2006.10.006","volume":"4","author":"T Achterberg","year":"2007","unstructured":"Achterberg, T.: Conflict analysis in mixed integer programming. Discrete Optimization 4(1), 4\u201320 (2007)","journal-title":"Discrete Optimization"},{"key":"15_CR2","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"118","DOI":"10.1007\/978-3-540-74970-7_11","volume-title":"Principles and Practice of Constraint Programming \u2013 CP 2007","author":"HR Andersen","year":"2007","unstructured":"Andersen, H.R., Hadzic, T., Hooker, J.N., Tiedemann, P.: A constraint store based on multivalued decision diagrams. In: Bessi\u00e8re, C. (ed.) CP 2007. LNCS, vol. 4741, pp. 118\u2013132. Springer, Heidelberg (2007)"},{"key":"15_CR3","doi-asserted-by":"publisher","first-page":"353","DOI":"10.1613\/jair.3152","volume":"40","author":"A Atserias","year":"2011","unstructured":"Atserias, A., Fichte, J.K., Thurley, M.: Clause-learning algorithms with many restarts and bounded-width resolution. Journal of Artificial Intelligence Research 40, 353\u2013373 (2011)","journal-title":"Journal of Artificial Intelligence Research"},{"key":"15_CR4","doi-asserted-by":"publisher","first-page":"319","DOI":"10.1613\/jair.1410","volume":"22","author":"P Beame","year":"2004","unstructured":"Beame, P., Kautz, H., Sabharwal, A.: Understanding and harnessing the potential of clause learning. Journal of Artificial Intelligence Research 22, 319\u2013351 (2004)","journal-title":"Journal of Artificial Intelligence Research"},{"key":"15_CR5","doi-asserted-by":"publisher","first-page":"107","DOI":"10.1007\/s10878-007-9123-z","volume":"16","author":"M Behle","year":"2008","unstructured":"Behle, M.: On threshold BDDs and the optimal variable ordering problem. Journal of Combinatorial Optimization 16, 107\u2013118 (2008)","journal-title":"Journal of Combinatorial Optimization"},{"issue":"2","key":"15_CR6","doi-asserted-by":"publisher","first-page":"253","DOI":"10.1287\/ijoc.2013.0561","volume":"26","author":"B Bergman","year":"2014","unstructured":"Bergman, B., Cire, A., van Hoeve, W.-J., Hooker, J.:  Optimization bounds from binary decision diagrams. INFORMS Journal on Computing 26(2), 253\u2013268 (2014)","journal-title":"INFORMS Journal on Computing"},{"issue":"2","key":"15_CR7","doi-asserted-by":"publisher","first-page":"211","DOI":"10.1007\/s10732-014-9238-1","volume":"20","author":"D Bergman","year":"2014","unstructured":"Bergman, D., Cire, A.A., van Hoeve, W.-J., Yunes, T.: BDD-based heuristics for binary optimization. Journal of Heuristics 20(2), 211\u2013234 (2014)","journal-title":"Journal of Heuristics"},{"key":"15_CR8","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"20","DOI":"10.1007\/978-3-642-21311-3_5","volume-title":"Integration of AI and OR Techniques in Constraint Programming for Combinatorial Optimization Problems","author":"D Bergman","year":"2011","unstructured":"Bergman, D., van Hoeve, W.-J., Hooker, J.N.: Manipulating MDD relaxations for combinatorial optimization. In: Achterberg, T., Beck, J.C. (eds.) CPAIOR 2011. LNCS, vol. 6697, pp. 20\u201335. Springer, Heidelberg (2011)"},{"issue":"9","key":"15_CR9","doi-asserted-by":"publisher","first-page":"993","DOI":"10.1109\/12.537122","volume":"45","author":"B Bollig","year":"1996","unstructured":"Bollig, B., Wegener, I.: Improving the variable ordering of OBDDs is NP-complete. IEEE Transactions on Computers 45(9), 993\u20131002 (1996)","journal-title":"IEEE Transactions on Computers"},{"issue":"8","key":"15_CR10","doi-asserted-by":"publisher","first-page":"677","DOI":"10.1109\/TC.1986.1676819","volume":"35","author":"RE Bryant","year":"1986","unstructured":"Bryant, R.E.: Graph-based algorithms for Boolean function manipulation. IEEE Transactions on Computers 35(8), 677\u2013691 (1986)","journal-title":"IEEE Transactions on Computers"},{"issue":"6","key":"15_CR11","doi-asserted-by":"publisher","first-page":"1411","DOI":"10.1287\/opre.2013.1221","volume":"61","author":"A Cire","year":"2013","unstructured":"Cire, A., van Hoeve, W.-J.:  Multivalued decision diagrams for sequencing problems. Operations Research 61(6), 1411\u20131428 (2013)","journal-title":"Operations Research"},{"key":"15_CR12","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"146","DOI":"10.1007\/978-3-642-29828-8_10","volume-title":"Integration of AI and OR Techniques in Contraint Programming for Combinatorial Optimzation Problems","author":"N Downing","year":"2012","unstructured":"Downing, N., Feydy, T., Stuckey, P.: Explaining flow-based propagation. In: Beldiceanu, N., Jussien, N., Pinson, \u00c9. (eds.) CPAIOR 2012. LNCS, vol. 7298, pp. 146\u2013162. Springer, Heidelberg (2012)"},{"key":"15_CR13","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"448","DOI":"10.1007\/978-3-540-85958-1_30","volume-title":"Principles and Practice of Constraint Programming","author":"T Hadzic","year":"2008","unstructured":"Hadzic, T., Hooker, J., O\u2019Sullivan, B., Tiedemann, P.: Approximate compilation of constraints into multivalued decision diagrams. In: Stuckey, P.J. (ed.) CP 2008. LNCS, vol. 5202, pp. 448\u2013462. Springer, Heidelberg (2008)"},{"key":"15_CR14","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"266","DOI":"10.1007\/978-3-642-15396-9_23","volume-title":"Principles and Practice of Constraint Programming \u2013 CP 2010","author":"S Hoda","year":"2010","unstructured":"Hoda, S., van Hoeve, W.-J., Hooker, J.: A systematic approach to MDD-based constraint programming. In: Cohen, D. (ed.) CP 2010. LNCS, vol. 6308, pp. 266\u2013280. Springer, Heidelberg (2010)"},{"unstructured":"Katsirelos, G.: Nogood Processing in CSPs. PhD thesis, University of Toronto (2008)","key":"15_CR15"},{"key":"15_CR16","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"128","DOI":"10.1007\/978-3-642-38171-3_9","volume-title":"Integration of AI and OR Techniques in Constraint Programming for Combinatorial Optimization Problems","author":"B Kell","year":"2013","unstructured":"Kell, B., van Hoeve, W.-J.: An MDD approach to multidimensional bin\u00a0packing. In: Gomes, C., Sellmann, M. (eds.) CPAIOR 2013. LNCS, vol. 7874, pp. 128\u2013143. Springer, Heidelberg (2013)"},{"issue":"4","key":"15_CR17","doi-asserted-by":"publisher","first-page":"249","DOI":"10.1007\/s12532-009-0009-1","volume":"1","author":"F Kilin\u00e7-Karzan","year":"2009","unstructured":"Kilin\u00e7-Karzan, F., Nemhauser, G., Savelsbergh, M.: Information-based branching schemes for binary linear mixed integer problems. Mathematical Programming Computation 1(4), 249\u2013293 (2009)","journal-title":"Mathematical Programming Computation"},{"unstructured":"Knuth, D.E.: The Art of Computer Programming, vol. 4, fascicle 1: Bitwise Tricks & Techniques; Binary Decision Diagrams. Addison-Wesley (2009)","key":"15_CR18"},{"issue":"4","key":"15_CR19","doi-asserted-by":"publisher","first-page":"985","DOI":"10.1002\/j.1538-7305.1959.tb01585.x","volume":"38","author":"CY Lee","year":"1959","unstructured":"Lee, C.Y.: Representation of switching circuits by binary-decision programs. Bell System Technical Journal 38(4), 985\u2013999 (1959)","journal-title":"Bell System Technical Journal"},{"unstructured":"Marques-Silva, J.P., Lynce, I., Malik, S.: CDCL solvers. In: Biere, A., Heule, M., van Maaren, H., Walsh, T., (eds.), Handbook of Satisfiability, chapter 4, pp. 131\u2013154. IOS Press (2009)","key":"15_CR20"},{"key":"15_CR21","doi-asserted-by":"publisher","first-page":"357","DOI":"10.1007\/s10601-008-9064-x","volume":"14","author":"O Ohrimenko","year":"2009","unstructured":"Ohrimenko, O., Stuckey, P., Codish, M.: Propagation via lazy clause generation. Constraints 14, 357\u2013391 (2009)","journal-title":"Constraints"},{"issue":"2","key":"15_CR22","doi-asserted-by":"publisher","first-page":"512","DOI":"10.1016\/j.artint.2010.10.002","volume":"175","author":"K Pipatsrisawat","year":"2011","unstructured":"Pipatsrisawat, K., Darwiche, A.: On the power of clause-learning SAT solvers as resolution engines. Artificial Intelligence 175(2), 512\u2013525 (2011)","journal-title":"Artificial Intelligence"},{"unstructured":"SAT Challenge 2012. SAT Challenge 2012: Downloads, November 23, 2014. http:\/\/baldur.iti.kit.edu\/SAT-Challenge-2012\/downloads.html","key":"15_CR23"},{"key":"15_CR24","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"5","DOI":"10.1007\/978-3-642-13520-0_3","volume-title":"Integration of AI and OR Techniques in Constraint Programming for Combinatorial Optimization Problems","author":"P Stuckey","year":"2010","unstructured":"Stuckey, P.: Lazy clause generation: combining the power of SAT and CP (and MIP?) solving. In: Lodi, A., Milano, M., Toth, P. (eds.) CPAIOR 2010. LNCS, vol. 6140, pp. 5\u20139. Springer, Heidelberg (2010)"},{"key":"15_CR25","series-title":"SIAM Monographs on Discrete Mathematics and Applications","doi-asserted-by":"publisher","DOI":"10.1137\/1.9780898719789","volume-title":"Branching Programs and Binary Decision Diagrams: Theory and Applications","author":"I Wegener","year":"2000","unstructured":"Wegener, I.: Branching Programs and Binary Decision Diagrams: Theory and Applications. SIAM Monographs on Discrete Mathematics and Applications. SIAM, Philadelphia (2000)"}],"container-title":["Lecture Notes in Computer Science","Integration of AI and OR Techniques in Constraint Programming"],"original-title":[],"language":"en","link":[{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/978-3-319-18008-3_15","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2020,12,30]],"date-time":"2020-12-30T20:05:43Z","timestamp":1609358743000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/978-3-319-18008-3_15"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2015]]},"ISBN":["9783319180076","9783319180083"],"references-count":25,"URL":"https:\/\/doi.org\/10.1007\/978-3-319-18008-3_15","relation":{},"ISSN":["0302-9743","1611-3349"],"issn-type":[{"type":"print","value":"0302-9743"},{"type":"electronic","value":"1611-3349"}],"subject":[],"published":{"date-parts":[[2015]]},"assertion":[{"value":"16 April 2015","order":1,"name":"first_online","label":"First Online","group":{"name":"ChapterHistory","label":"Chapter History"}}]}}