{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2026,6,2]],"date-time":"2026-06-02T04:05:13Z","timestamp":1780373113097,"version":"3.54.1"},"publisher-location":"Cham","reference-count":29,"publisher":"Springer Nature Switzerland","isbn-type":[{"value":"9783032272416","type":"print"},{"value":"9783032272423","type":"electronic"}],"license":[{"start":{"date-parts":[[2026,1,1]],"date-time":"2026-01-01T00:00:00Z","timestamp":1767225600000},"content-version":"tdm","delay-in-days":0,"URL":"https:\/\/www.springernature.com\/gp\/researchers\/text-and-data-mining"},{"start":{"date-parts":[[2026,1,1]],"date-time":"2026-01-01T00:00:00Z","timestamp":1767225600000},"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":[[2026]]},"DOI":"10.1007\/978-3-032-27242-3_10","type":"book-chapter","created":{"date-parts":[[2026,6,2]],"date-time":"2026-06-02T03:25:57Z","timestamp":1780370757000},"page":"155-172","update-policy":"https:\/\/doi.org\/10.1007\/springer_crossmark_policy","source":"Crossref","is-referenced-by-count":0,"title":["Resolution Meets Cutting Planes: Introducing Hypercube Linear Resolution"],"prefix":"10.1007","author":[{"ORCID":"https:\/\/orcid.org\/0009-0005-5333-2767","authenticated-orcid":false,"given":"Maarten","family":"Flippo","sequence":"first","affiliation":[],"role":[{"vocabulary":"crossref","role":"author"}]},{"ORCID":"https:\/\/orcid.org\/0000-0003-2186-0459","authenticated-orcid":false,"given":"Peter J.","family":"Stuckey","sequence":"additional","affiliation":[],"role":[{"vocabulary":"crossref","role":"author"}]},{"ORCID":"https:\/\/orcid.org\/0000-0003-1587-5582","authenticated-orcid":false,"given":"Emir","family":"Demirovi\u0107","sequence":"additional","affiliation":[],"role":[{"vocabulary":"crossref","role":"author"}]}],"member":"297","published-online":{"date-parts":[[2026,6,1]]},"reference":[{"key":"10_CR1","doi-asserted-by":"publisher","unstructured":"Audemard, G., Katsirelos, G., Simon, L.: A Restriction of extended resolution for clause learning SAT solvers. In: Proceedings of the AAAI Conference on Artificial Intelligence, vol. 24, no. 1, pp. 15\u201320 (2010). https:\/\/doi.org\/10.1609\/aaai.v24i1.7553","DOI":"10.1609\/aaai.v24i1.7553"},{"key":"10_CR2","doi-asserted-by":"publisher","unstructured":"Baauw, R., Flippo, M., Demirovi\u0107, E.: Conflict analysis based on cutting-planes for constraint programming. In: de la Banda, M.G. (ed.) 31st International Conference on Principles and Practice of Constraint Programming (CP 2025). Leibniz International Proceedings in Informatics (LIPIcs), vol. 340, pp. 4:1\u20134:19. Schloss Dagstuhl - Leibniz-Zentrum f\u00fcr Informatik, Dagstuhl (2025). https:\/\/doi.org\/10.4230\/LIPIcs.CP.2025.4","DOI":"10.4230\/LIPIcs.CP.2025.4"},{"issue":"3","key":"10_CR3","doi-asserted-by":"publisher","first-page":"545","DOI":"10.1007\/s10589-016-9847-8","volume":"65","author":"P Belotti","year":"2016","unstructured":"Belotti, P., et al.: On handling indicator constraints in mixed integer programming. Comput. Optim. Appl. 65(3), 545\u2013566 (2016). https:\/\/doi.org\/10.1007\/s10589-016-9847-8","journal-title":"Comput. Optim. Appl."},{"key":"10_CR4","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"49","DOI":"10.1007\/978-3-319-44953-1_4","volume-title":"Principles and Practice of Constraint Programming","author":"G Belov","year":"2016","unstructured":"Belov, G., Stuckey, P.J., Tack, G., Wallace, M.: Improved linearization of constraint programming models. In: Rueher, M. (ed.) CP 2016. LNCS, vol. 9892, pp. 49\u201365. Springer, Cham (2016). https:\/\/doi.org\/10.1007\/978-3-319-44953-1_4"},{"key":"10_CR5","unstructured":"Biere, A., Heule, M., van Maaren, H.: Handbook of Satisfiability. IOS Press (2009)"},{"key":"10_CR6","doi-asserted-by":"publisher","first-page":"1539","DOI":"10.1613\/jair.1.14296","volume":"77","author":"B Bogaerts","year":"2023","unstructured":"Bogaerts, B., Gocht, S., McCreesh, C., Nordstr\u00f6m, J.: Certified dominance and symmetry breaking for combinatorial optimisation. J. Artif. Intell. Res. 77, 1539\u20131589 (2023)","journal-title":"J. Artif. Intell. Res."},{"key":"10_CR7","doi-asserted-by":"publisher","first-page":"102","DOI":"10.1016\/j.jsc.2019.07.021","volume":"100","author":"M Bromberger","year":"2020","unstructured":"Bromberger, M., Sturm, T., Weidenbach, C.: A complete and terminating approach to linear integer solving. J. Symb. Comput. 100, 102\u2013136 (2020). https:\/\/doi.org\/10.1016\/j.jsc.2019.07.021","journal-title":"J. Symb. Comput."},{"key":"10_CR8","doi-asserted-by":"publisher","unstructured":"Buss, S., Nordstr\u00f6m, J.: Chapter 7. Proof complexity and SAT solving. In: Handbook of Satisfiability, pp. 233\u2013350. IOS Press (2021). https:\/\/doi.org\/10.3233\/FAIA200990","DOI":"10.3233\/FAIA200990"},{"key":"10_CR9","doi-asserted-by":"publisher","unstructured":"Chai, D., Kuehlmann, A.: A fast pseudo-boolean constraint solver. In: Proceedings of the 40th Annual Design Automation Conference, DAC \u201903, pp. 830\u2013835. Association for Computing Machinery, New York (2003). https:\/\/doi.org\/10.1145\/775832.776041","DOI":"10.1145\/775832.776041"},{"key":"10_CR10","doi-asserted-by":"publisher","unstructured":"Codel, C., Fazekas, K., Heule, M., Iser, M.: Proceedings of SAT Competition 2025: Solver and Benchmark Descriptions, Report, TU Wien (2025). https:\/\/doi.org\/10.34726\/10379","DOI":"10.34726\/10379"},{"issue":"3","key":"10_CR11","doi-asserted-by":"publisher","first-page":"201","DOI":"10.1145\/321033.321034","volume":"7","author":"M Davis","year":"1960","unstructured":"Davis, M., Putnam, H.: A computing procedure for quantification theory. J. ACM 7(3), 201\u2013215 (1960). https:\/\/doi.org\/10.1145\/321033.321034","journal-title":"J. ACM"},{"key":"10_CR12","unstructured":"Delft High Performance Computing Centre (DHPC): DelftBlue Supercomputer (Phase 2) (2024). https:\/\/www.tudelft.nl\/dhpc\/ark:\/44463\/DelftBluePhase2"},{"key":"10_CR13","doi-asserted-by":"crossref","unstructured":"Elffers, J., Nordstr\u00f6m, J.: Divide and conquer: towards faster pseudo-Boolean solving. In: Proceedings of the 27th International Joint Conference on Artificial Intelligence, IJCAI\u201918, pp. 1291\u20131299. AAAI Press, Stockholm (2018)","DOI":"10.24963\/ijcai.2018\/180"},{"key":"10_CR14","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"352","DOI":"10.1007\/978-3-642-04244-7_29","volume-title":"Principles and Practice of Constraint Programming - CP 2009","author":"T Feydy","year":"2009","unstructured":"Feydy, T., Stuckey, P.J.: Lazy clause generation reengineered. In: Gent, I.P. (ed.) CP 2009. LNCS, vol. 5732, pp. 352\u2013366. Springer, Heidelberg (2009). https:\/\/doi.org\/10.1007\/978-3-642-04244-7_29"},{"key":"10_CR15","doi-asserted-by":"publisher","unstructured":"Flippo, M., Sidorov, K., Marijnissen, I., Smits, J., Demirovi\u0107, E.: A multi-stage proof logging framework to certify the correctness of CP solvers. In: Shaw, P. (ed.) 30th International Conference on Principles and Practice of Constraint Programming (CP 2024). Leibniz International Proceedings in Informatics (LIPIcs), vol. 307, pp. 11:1\u201311:20. Schloss Dagstuhl - Leibniz-Zentrum f\u00fcr Informatik, Dagstuhl (2024). https:\/\/doi.org\/10.4230\/LIPIcs.CP.2024.11. https:\/\/drops.dagstuhl.de\/entities\/document\/10.4230\/LIPIcs.CP.2024.11","DOI":"10.4230\/LIPIcs.CP.2024.11"},{"issue":"5","key":"10_CR16","doi-asserted-by":"publisher","first-page":"275","DOI":"10.1090\/S0002-9904-1958-10224-4","volume":"64","author":"RE Gomory","year":"1958","unstructured":"Gomory, R.E.: Outline of an algorithm for integer solutions to linear programs. Bull. Am. Math. Soc. 64(5), 275\u2013278 (1958). https:\/\/doi.org\/10.1090\/S0002-9904-1958-10224-4","journal-title":"Bull. Am. Math. Soc."},{"issue":"1","key":"10_CR17","doi-asserted-by":"publisher","first-page":"217","DOI":"10.1007\/BF02186368","volume":"12","author":"JN Hooker","year":"1988","unstructured":"Hooker, J.N.: Generalized resolution and cutting planes. Ann. Oper. Res. 12(1), 217\u2013239 (1988). https:\/\/doi.org\/10.1007\/BF02186368","journal-title":"Ann. Oper. Res."},{"issue":"15","key":"10_CR18","doi-asserted-by":"publisher","first-page":"1277","DOI":"10.1016\/j.artint.2010.07.008","volume":"174","author":"J Huang","year":"2010","unstructured":"Huang, J.: Extended clause learning. Artif. Intell. 174(15), 1277\u20131284 (2010). https:\/\/doi.org\/10.1016\/j.artint.2010.07.008","journal-title":"Artif. Intell."},{"issue":"1","key":"10_CR19","doi-asserted-by":"publisher","first-page":"79","DOI":"10.1007\/s10817-013-9281-x","volume":"51","author":"D Jovanovi\u0107","year":"2013","unstructured":"Jovanovi\u0107, D., de Moura, L.: Cutting to the Chase. J. Autom. Reason. 51(1), 79\u2013108 (2013). https:\/\/doi.org\/10.1007\/s10817-013-9281-x","journal-title":"J. Autom. Reason."},{"key":"10_CR20","unstructured":"Katsirelos, G.: Generalized NoGoods in CSPs. In: Proceedings of the AAAI Conference on Artificial Intelligence, vol. 5, pp. 390\u2013396 (2005)"},{"key":"10_CR21","doi-asserted-by":"publisher","unstructured":"Marques Silva, J., Sakallah, K.: GRASP-a new search algorithm for satisfiability. In: Proceedings of International Conference on Computer Aided Design, pp. 220\u2013227 (1996). https:\/\/doi.org\/10.1109\/ICCAD.1996.569607","DOI":"10.1109\/ICCAD.1996.569607"},{"key":"10_CR22","doi-asserted-by":"publisher","unstructured":"Moskewicz, M.W., Madigan, C.F., Zhao, Y., Zhang, L., Malik, S.: Chaff: engineering an efficient SAT solver. In: Proceedings of the 38th Annual Design Automation Conference, DAC \u201901, pp. 530\u2013535. Association for Computing Machinery, New York (2001). https:\/\/doi.org\/10.1145\/378239.379017","DOI":"10.1145\/378239.379017"},{"key":"10_CR23","doi-asserted-by":"publisher","unstructured":"Nieuwenhuis, R., Oliveras, A., Rodr\u00edguez-Carbonell, E.: IntSat: integer linear programming by conflict-driven constraint learning. Optim. Methods Softw. 1\u201328 (2023). https:\/\/doi.org\/10.1080\/10556788.2023.2246167","DOI":"10.1080\/10556788.2023.2246167"},{"issue":"3","key":"10_CR24","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.J., Codish, M.: Propagation via lazy clause generation. Constraints 14(3), 357\u2013391 (2009). https:\/\/doi.org\/10.1007\/s10601-008-9064-x","journal-title":"Constraints"},{"key":"10_CR25","doi-asserted-by":"publisher","unstructured":"Perron, L., Didier, F., Gay, S.: The CP-SAT-LP solver. In: Yap, R.H.C. (ed.) 29th International Conference on Principles and Practice of Constraint Programming (CP 2023). Leibniz International Proceedings in Informatics (LIPIcs), vol. 280, pp. 3:1\u20133:2. Schloss Dagstuhl - Leibniz-Zentrum f\u00fcr Informatik, Dagstuhl (2023). https:\/\/doi.org\/10.4230\/LIPIcs.CP.2023.3","DOI":"10.4230\/LIPIcs.CP.2023.3"},{"key":"10_CR26","doi-asserted-by":"publisher","first-page":"98","DOI":"10.1016\/j.compchemeng.2015.02.013","volume":"76","author":"F Trespalacios","year":"2015","unstructured":"Trespalacios, F., Grossmann, I.E.: Improved Big-M reformulation for generalized disjunctive programs. Comput. Chem. Eng. 76, 98\u2013103 (2015). https:\/\/doi.org\/10.1016\/j.compchemeng.2015.02.013","journal-title":"Comput. Chem. Eng."},{"key":"10_CR27","doi-asserted-by":"publisher","unstructured":"Tseitin, G.S.: On the complexity of derivation in propositional calculus. In: Siekmann, J.H., Wrightson, G. (eds.) Automation of Reasoning: 2: Classical Papers on Computational Logic 1967\u20131970, pp. 466\u2013483. Springer, Heidelberg (1983). https:\/\/doi.org\/10.1007\/978-3-642-81955-1_28","DOI":"10.1007\/978-3-642-81955-1_28"},{"key":"10_CR28","doi-asserted-by":"publisher","first-page":"135","DOI":"10.1016\/j.artint.2016.06.002","volume":"238","author":"M Veksler","year":"2016","unstructured":"Veksler, M., Strichman, O.: Learning general constraints in CSP. Artif. Intell. 238, 135\u2013153 (2016). https:\/\/doi.org\/10.1016\/j.artint.2016.06.002","journal-title":"Artif. Intell."},{"key":"10_CR29","doi-asserted-by":"crossref","unstructured":"Wolsey, L.A.: Integer Programming. John Wiley & Sons, Hoboken (2020)","DOI":"10.1002\/9781119606475"}],"container-title":["Lecture Notes in Computer Science","Integration of Constraint Programming, Artificial Intelligence, and Operations Research"],"original-title":[],"language":"en","link":[{"URL":"https:\/\/link.springer.com\/content\/pdf\/10.1007\/978-3-032-27242-3_10","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2026,6,2]],"date-time":"2026-06-02T03:26:05Z","timestamp":1780370765000},"score":1,"resource":{"primary":{"URL":"https:\/\/link.springer.com\/10.1007\/978-3-032-27242-3_10"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2026]]},"ISBN":["9783032272416","9783032272423"],"references-count":29,"URL":"https:\/\/doi.org\/10.1007\/978-3-032-27242-3_10","relation":{},"ISSN":["0302-9743","1611-3349"],"issn-type":[{"value":"0302-9743","type":"print"},{"value":"1611-3349","type":"electronic"}],"subject":[],"published":{"date-parts":[[2026]]},"assertion":[{"value":"1 June 2026","order":1,"name":"first_online","label":"First Online","group":{"name":"ChapterHistory","label":"Chapter History"}},{"value":"CPAIOR","order":1,"name":"conference_acronym","label":"Conference Acronym","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"International Conference on the Integration of Constraint Programming, Artificial Intelligence, and Operations Research","order":2,"name":"conference_name","label":"Conference Name","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"Rabat","order":3,"name":"conference_city","label":"Conference City","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"Morocco","order":4,"name":"conference_country","label":"Conference Country","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"2026","order":5,"name":"conference_year","label":"Conference Year","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"26 May 2026","order":7,"name":"conference_start_date","label":"Conference Start Date","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"29 May 2026","order":8,"name":"conference_end_date","label":"Conference End Date","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"23","order":9,"name":"conference_number","label":"Conference Number","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"cpaior2026","order":10,"name":"conference_id","label":"Conference ID","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"https:\/\/sites.google.com\/view\/cpaior2026\/home","order":11,"name":"conference_url","label":"Conference URL","group":{"name":"ConferenceInfo","label":"Conference Information"}}]}}