{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2025,12,30]],"date-time":"2025-12-30T22:47:52Z","timestamp":1767134872547,"version":"3.48.0"},"publisher-location":"Cham","reference-count":28,"publisher":"Springer International Publishing","isbn-type":[{"type":"print","value":"9783031252105"},{"type":"electronic","value":"9783031252112"}],"license":[{"start":{"date-parts":[[2023,1,1]],"date-time":"2023-01-01T00:00:00Z","timestamp":1672531200000},"content-version":"tdm","delay-in-days":0,"URL":"https:\/\/www.springernature.com\/gp\/researchers\/text-and-data-mining"},{"start":{"date-parts":[[2023,1,1]],"date-time":"2023-01-01T00:00:00Z","timestamp":1672531200000},"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":[[2023]]},"DOI":"10.1007\/978-3-031-25211-2_2","type":"book-chapter","created":{"date-parts":[[2023,1,25]],"date-time":"2023-01-25T19:02:42Z","timestamp":1674673362000},"page":"15-27","update-policy":"https:\/\/doi.org\/10.1007\/springer_crossmark_policy","source":"Crossref","is-referenced-by-count":0,"title":["Optimal Length Cutting Plane Refutations of\u00a0Integer Programs"],"prefix":"10.1007","author":[{"given":"K.","family":"Subramani","sequence":"first","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"P.","family":"Wojciechowski","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]}],"member":"297","published-online":{"date-parts":[[2023,1,26]]},"reference":[{"key":"2_CR1","doi-asserted-by":"crossref","unstructured":"Alekhnovich, M., Razborov, A.: Resolution is not automatizable unless W[P] is tractable. In: Proceedings of the 42nd IEEE Symposium on Foundations of Computer Science, FOCS 2001, pp. 210, USA. IEEE Computer Society (2001)","DOI":"10.1109\/SFCS.2001.959895"},{"key":"2_CR2","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"209","DOI":"10.1007\/978-3-540-30482-1_22","volume-title":"Formal Methods and Software Engineering","author":"A Armando","year":"2004","unstructured":"Armando, A., Castellini, C., Mantovani, J.: Software model checking using linear constraints. In: Davies, J., Schulte, W., Barnett, M. (eds.) ICFEM 2004. LNCS, vol. 3308, pp. 209\u2013223. Springer, Heidelberg (2004). https:\/\/doi.org\/10.1007\/978-3-540-30482-1_22"},{"key":"2_CR3","doi-asserted-by":"crossref","unstructured":"Atserias, A., Luisa Bonet, M.: On the automatizability of resolution and related propositional proof systems. Inf. Comput. 189(2), 182\u2013201 (2004)","DOI":"10.1016\/j.ic.2003.10.004"},{"key":"2_CR4","unstructured":"Atserias, A., M\u00fcller, M.: Automating resolution is NP-hard. CoRR, abs\/1904.02991 (2019)"},{"key":"2_CR5","doi-asserted-by":"crossref","unstructured":"Beame, P., Pitassi, T.: Simplified and improved resolution lower bounds. In: 37th Annual Symposium on Foundations of Computer Science, pages 274\u2013282, Burlington, Vermont, 14\u201316 October 1996. IEEE (1996)","DOI":"10.1109\/SFCS.1996.548486"},{"key":"2_CR6","doi-asserted-by":"crossref","unstructured":"Berste, B., Leconte, M.: Using constraints to verify properties of rule programs. In: Proceedings of the 2010 International Conference on Software Testing, Verification, and Validation Workshops, pp. 349\u2013354 (2008)","DOI":"10.1109\/ICSTW.2010.42"},{"key":"2_CR7","doi-asserted-by":"crossref","unstructured":"Bonet, M.L., Pitassi, T., Raz, R.: Lower bounds for cutting planes proofs with small coefficients. J. Symb. Log., 62(3), 708\u2013728 (1997)","DOI":"10.2307\/2275569"},{"key":"2_CR8","unstructured":"Ceberio, M., Acosta, C., Servin, C.: A constraint-based approach to verification of programs with floating-point numbers. In: Proceedings of the 2008 International Conference on Software Engineering Research and Practice, pp. 225\u2013230 (2008)"},{"key":"2_CR9","doi-asserted-by":"crossref","unstructured":"Cheung, K.K.H., Gleixner, A.M., Steffy. D.E.: Verifying integer programming results. In: Integer Programming and Combinatorial Optimization - 19th International Conference, IPCO 2017, vol. 10328 of Lecture Notes in Computer Science, pp. 148\u2013160 (2017)","DOI":"10.1007\/978-3-319-59250-3_13"},{"issue":"10\u201311","key":"2_CR10","first-page":"886","volume":"4","author":"V Chvatal","year":"1973","unstructured":"Chvatal, V.: Edmonds polytopes and a hierarchy of combinatorial problems. Discret. Math. 4(10\u201311), 886\u2013904 (1973)","journal-title":"Discret. Math."},{"key":"2_CR11","doi-asserted-by":"crossref","unstructured":"Collavizza, H., Reuher, N.: Exploration of the capabilities of constraint programming for software verification. In: Proceedings of the 2006 International Conference on Tools and Algorithms for the Construction and Analysis of Systems (2006)","DOI":"10.1007\/11691372_12"},{"key":"2_CR12","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"327","DOI":"10.1007\/978-3-540-85958-1_22","volume-title":"Principles and Practice of Constraint Programming","author":"H Collavizza","year":"2008","unstructured":"Collavizza, H., Rueher, M., Van Hentenryck, P.: CPBPV: a constraint-programming framework for bounded program verification. In: Stuckey, P.J. (ed.) CP 2008. LNCS, vol. 5202, pp. 327\u2013341. Springer, Heidelberg (2008). https:\/\/doi.org\/10.1007\/978-3-540-85958-1_22"},{"issue":"1","key":"2_CR13","doi-asserted-by":"publisher","first-page":"11","DOI":"10.1007\/BF01580849","volume":"47","author":"W Cook","year":"1990","unstructured":"Cook, W.: Cutting-plane proofs in polynomial space. Math. Program. 47(1), 11\u201318 (1990)","journal-title":"Math. Program."},{"key":"2_CR14","doi-asserted-by":"crossref","unstructured":"Cook, W., Coullard, C.R., Turan, Gy. On the complexity of cutting-plane proofs. Discrete Appl. Math. 18, 25\u201338 (1987)","DOI":"10.1016\/0166-218X(87)90039-4"},{"key":"2_CR15","doi-asserted-by":"crossref","unstructured":"Fleming, N., Pankratov, D., Pitassi, T., Robere, R.: Random $$\\varTheta $$(log n)-CNFs are hard for cutting planes. In: 58th IEEE Annual Symposium on Foundations of Computer Science, FOCS 2017, pp. 109\u2013120 (2017)","DOI":"10.1109\/FOCS.2017.19"},{"key":"2_CR16","unstructured":"Galesi, N., Pudl\u00e1k, P., Thapen, N.: The space complexity of cutting planes refutations. In: Proceedings of the 30th Conference on Computational Complexity, CCC 2015, pp. 433\u2013447 (2005)"},{"key":"2_CR17","unstructured":"Goldreich, O.: On promise problems (a survey in memory of Shimon even [1935-2004]). Electron. Colloquium Comput. Complex 61(018) (2005)"},{"key":"2_CR18","doi-asserted-by":"crossref","unstructured":"Sajin Koroth, M., Mertz, I., Pitassi, T.: Automating cutting planes is NP-hard. In: Proceedings of the 52nd Annual ACM SIGACT Symposium on Theory of Computing, STOC 2020, pp. 68\u201377 (2020)","DOI":"10.1145\/3357713.3384248"},{"key":"2_CR19","doi-asserted-by":"crossref","unstructured":"Gulwani, S., Srivastava, S., Venkatesan, R.: Program analysis as constraint solving. In: Proceedings of the 2008 ACM SIGPLAN Conference on Programming language design and implementation, New York, NY. ACM (2008)","DOI":"10.1145\/1375581.1375616"},{"key":"2_CR20","doi-asserted-by":"crossref","unstructured":"Hrubes, P., Pudl\u00e1k, P.: Random formulas, monotone circuits, and interpolation. In: 58th IEEE Annual Symposium on Foundations of Computer Science, FOCS 2017, pp. 121\u2013131 (2017)","DOI":"10.1109\/FOCS.2017.20"},{"key":"2_CR21","unstructured":"Kann, V.: On the approximability of np-complete optimization problems. Ph.D. thesis, Royal Institute of Technology Stockholm (1992)"},{"issue":"3","key":"2_CR22","first-page":"317","volume":"1","author":"V Kann","year":"1994","unstructured":"Kann, V.: Polynomially bounded minimization problems that are hard to approximate. Nordic J. of Compu. 1(3), 317\u2013331 (1994)","journal-title":"Nordic J. of Compu."},{"issue":"3","key":"2_CR23","doi-asserted-by":"publisher","first-page":"490","DOI":"10.1016\/0022-0000(88)90039-6","volume":"36","author":"MW Krentel","year":"1988","unstructured":"Krentel, M.W.: The complexity of optimization problems. J. Comput. Syst. Sci. 36(3), 490\u2013509 (1988)","journal-title":"J. Comput. Syst. Sci."},{"key":"2_CR24","unstructured":"Orponen, P., Mannila, H.: On approximation preserving reductions: complete problems and robust measures. Technical report, Department of Computer Science, University of Helsinki (1987)"},{"issue":"3","key":"2_CR25","doi-asserted-by":"publisher","first-page":"981","DOI":"10.2307\/2275583","volume":"62","author":"P Pudl\u00e1k","year":"1997","unstructured":"Pudl\u00e1k, P.: Lower bounds for resolution and cutting plane proofs and monotone computations. J. Symbol Logic 62(3), 981\u2013998 (1997)","journal-title":"J. Symbol Logic"},{"key":"2_CR26","doi-asserted-by":"crossref","unstructured":"Subramani, K., Wojciechowki, P.: Integer feasibility and refutations in UTVPI constraints using bit-scaling. Algorithmica (Accepted In Press 2022)","DOI":"10.1007\/s00453-022-01048-1"},{"key":"2_CR27","doi-asserted-by":"crossref","unstructured":"Subramani, K., Wojciechowski, P.J.: A bit-scaling algorithm for integer feasibility in UTVPI constraints. In: Combinatorial Algorithms - 27th International Workshop, IWOCA 2016, vol. 9843, pp. 321\u2013333 (2016)","DOI":"10.1007\/978-3-319-44543-4_25"},{"key":"2_CR28","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"292","DOI":"10.1007\/978-3-319-94144-8_18","volume-title":"Theory and Applications of Satisfiability Testing \u2013 SAT 2018","author":"M Vinyals","year":"2018","unstructured":"Vinyals, M., Elffers, J., Gir\u00e1ldez-Cru, J., Gocht, S., Nordstr\u00f6m, J.: In between resolution and cutting planes: a study of proof systems for pseudo-Boolean SAT solving. In: Beyersdorff, O., Wintersteiger, C.M. (eds.) SAT 2018. LNCS, vol. 10929, pp. 292\u2013310. Springer, Cham (2018). https:\/\/doi.org\/10.1007\/978-3-319-94144-8_18"}],"container-title":["Lecture Notes in Computer Science","Algorithms and Discrete Applied Mathematics"],"original-title":[],"language":"en","link":[{"URL":"https:\/\/link.springer.com\/content\/pdf\/10.1007\/978-3-031-25211-2_2","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2025,12,30]],"date-time":"2025-12-30T22:44:04Z","timestamp":1767134644000},"score":1,"resource":{"primary":{"URL":"https:\/\/link.springer.com\/10.1007\/978-3-031-25211-2_2"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2023]]},"ISBN":["9783031252105","9783031252112"],"references-count":28,"URL":"https:\/\/doi.org\/10.1007\/978-3-031-25211-2_2","relation":{},"ISSN":["0302-9743","1611-3349"],"issn-type":[{"type":"print","value":"0302-9743"},{"type":"electronic","value":"1611-3349"}],"subject":[],"published":{"date-parts":[[2023]]},"assertion":[{"value":"26 January 2023","order":1,"name":"first_online","label":"First Online","group":{"name":"ChapterHistory","label":"Chapter History"}},{"value":"CALDAM","order":1,"name":"conference_acronym","label":"Conference Acronym","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"Conference on Algorithms and Discrete Applied Mathematics","order":2,"name":"conference_name","label":"Conference Name","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"Gandhinagar","order":3,"name":"conference_city","label":"Conference City","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"India","order":4,"name":"conference_country","label":"Conference Country","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"2023","order":5,"name":"conference_year","label":"Conference Year","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"9 February 2023","order":7,"name":"conference_start_date","label":"Conference Start Date","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"11 February 2023","order":8,"name":"conference_end_date","label":"Conference End Date","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"9","order":9,"name":"conference_number","label":"Conference Number","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"caldam2023","order":10,"name":"conference_id","label":"Conference ID","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"https:\/\/caldam2023.daiict.ac.in\/","order":11,"name":"conference_url","label":"Conference URL","group":{"name":"ConferenceInfo","label":"Conference Information"}}]}}