{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2026,3,18]],"date-time":"2026-03-18T04:43:44Z","timestamp":1773809024422,"version":"3.50.1"},"reference-count":37,"publisher":"Springer Science and Business Media LLC","issue":"10","license":[{"start":{"date-parts":[[2022,6,1]],"date-time":"2022-06-01T00:00:00Z","timestamp":1654041600000},"content-version":"tdm","delay-in-days":0,"URL":"https:\/\/www.springer.com\/tdm"},{"start":{"date-parts":[[2022,6,1]],"date-time":"2022-06-01T00:00:00Z","timestamp":1654041600000},"content-version":"vor","delay-in-days":0,"URL":"https:\/\/www.springer.com\/tdm"}],"funder":[{"DOI":"10.13039\/100000181","name":"Air Force Office of Scientific Research","doi-asserted-by":"crossref","award":["FA9550-19-1-017"],"award-info":[{"award-number":["FA9550-19-1-017"]}],"id":[{"id":"10.13039\/100000181","id-type":"DOI","asserted-by":"crossref"}]}],"content-domain":{"domain":["link.springer.com"],"crossmark-restriction":false},"short-container-title":["Ann Math Artif Intell"],"published-print":{"date-parts":[[2022,10]]},"DOI":"10.1007\/s10472-022-09800-7","type":"journal-article","created":{"date-parts":[[2022,6,1]],"date-time":"2022-06-01T20:10:37Z","timestamp":1654114237000},"page":"979-998","update-policy":"https:\/\/doi.org\/10.1007\/springer_crossmark_policy","source":"Crossref","is-referenced-by-count":2,"title":["On the lengths of tree-like and Dag-like cutting plane refutations of Horn constraint systems"],"prefix":"10.1007","volume":"90","author":[{"given":"P.","family":"Wojciechowski","sequence":"first","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"ORCID":"https:\/\/orcid.org\/0000-0001-5821-5117","authenticated-orcid":false,"given":"K.","family":"Subramani","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]}],"member":"297","published-online":{"date-parts":[[2022,6,1]]},"reference":[{"key":"9800_CR1","doi-asserted-by":"crossref","unstructured":"Alekhnovich, M., Buss, S., Moran, S., Pitassi, T.: Minimum propositional proof length is NP-hard to linearly approximate. In: Mathematical Foundations of Computer Science (MFCS), pp. 176\u2013184. Springer, Lecture Notes in Computer Science (1998)","DOI":"10.1007\/BFb0055766"},{"key":"9800_CR2","doi-asserted-by":"crossref","unstructured":"Bakhirkin, A., Monniaux, D.: Combining forward and backward abstract interpretation of Horn clauses. In: Static Analysis - 24th International Symposium, SAS 2017, New York, NY, USA, 30 of Aug. - 1 of Sept., 2017, pp. 23\u201345 (2017)","DOI":"10.1007\/978-3-319-66706-5_2"},{"key":"9800_CR3","doi-asserted-by":"crossref","unstructured":"Bj\u00f8rner, N., Gurfinkel, A., McMillan, K.L., Rybalchenko, A.: Horn clause solvers for program verification. In: Fields of Logic and Computation II - Essays Dedicated to Yuri Gurevich on the Occasion of His 75th Birthday, pp. 24\u201351 (2015)","DOI":"10.1007\/978-3-319-23534-9_2"},{"issue":"3","key":"9800_CR4","doi-asserted-by":"publisher","first-page":"708","DOI":"10.2307\/2275569","volume":"62","author":"ML Bonet","year":"1997","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)","journal-title":"J. Symb Log."},{"key":"9800_CR5","doi-asserted-by":"publisher","first-page":"85","DOI":"10.1016\/j.disopt.2012.11.001","volume":"10","author":"R Chandrasekaran","year":"2013","unstructured":"Chandrasekaran, R., Subramani, K.: A combinatorial algorithm for Horn programs. Discret. Optim. 10, 85\u2013101 (2013)","journal-title":"Discret. Optim."},{"key":"9800_CR6","doi-asserted-by":"publisher","first-page":"701","DOI":"10.1613\/jair.3196","volume":"40","author":"A Cimatti","year":"2011","unstructured":"Cimatti, A., Griggio, A., Sebastiani, R.: Computing small unsatisfiable cores in satisfiability modulo theories. J. Artif Intell. Res. (JAIR) 40, 701\u2013728 (2011)","journal-title":"J. Artif Intell. Res. (JAIR)"},{"key":"9800_CR7","doi-asserted-by":"publisher","first-page":"25","DOI":"10.1016\/0166-218X(87)90039-4","volume":"18","author":"W Cook","year":"1987","unstructured":"Cook, W., Coullard, C.R., Turan, G.Y.: On the complexity of cutting-plane proofs. Discret. Appl. Math. 18, 25\u201338 (1987)","journal-title":"Discret. Appl. Math."},{"key":"9800_CR8","doi-asserted-by":"crossref","unstructured":"Cousot, P., Cousot, R.: Abstract interpretation: a unified lattice model for static analysis of programs by construction or approximation of fixpoints. POPL, pp. 238\u2013252 (1977)","DOI":"10.1145\/512950.512973"},{"key":"9800_CR9","doi-asserted-by":"crossref","unstructured":"de Moura, L., Bj\u00f8rner, N.: Z3: an efficient SMT solver. Microsoft Research, http:\/\/research.microsoft.com\/projects\/z3\/ (2008)","DOI":"10.1007\/978-3-540-78800-3_24"},{"key":"9800_CR10","doi-asserted-by":"crossref","unstructured":"de Moura, L., Owre, S., Ruess, H., Rushby, J.M., Shankar, N.: The ICS decision procedures for embedded deduction. IJCAR, pp. 218\u2013222 (2004)","DOI":"10.1007\/978-3-540-25984-8_14"},{"key":"9800_CR11","unstructured":"Dhiflaoui, M., Funke, S., Kwappik, C., Mehlhorn, K., Seel, M., Sch\u00f6mer, E., Schulte, R., Weber, D.: Certifying and repairing solutions to large lps how good are lp-solvers? SODA, pp. 255\u2013256 (2003)"},{"key":"9800_CR12","unstructured":"Duterre, B., de Moura, L.: The YICES SMT Solver. Technical report, SRI International (2006)"},{"issue":"124","key":"9800_CR13","first-page":"1","volume":"124","author":"G Farkas","year":"1902","unstructured":"Farkas, G.: \u00dcber die Theorie der Einfachen Ungleichungen. Journal f\u00fcr die Reine und Angewandte Mathematik 124(124), 1\u201327 (1902)","journal-title":"Journal f\u00fcr die Reine und Angewandte Mathematik"},{"key":"9800_CR14","doi-asserted-by":"crossref","unstructured":"Ford, J., Shankar, N.: Formal verification of a combination decision procedure. CADE, pp. 347\u2013362 (2002)","DOI":"10.1007\/3-540-45620-1_29"},{"key":"9800_CR15","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, 275\u2013278 (1958)","journal-title":"Bull. Am. Math. Soc."},{"issue":"2-3","key":"9800_CR16","doi-asserted-by":"publisher","first-page":"297","DOI":"10.1016\/0304-3975(85)90144-6","volume":"39","author":"A Haken","year":"1985","unstructured":"Haken, A.: The intractability of resolution. Theor. Comput. Sci. 39 (2-3), 297\u2013308 (1985)","journal-title":"Theor. Comput. Sci."},{"issue":"1-4","key":"9800_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-4), 217\u2013239 (1988)","journal-title":"Ann. Oper. Res."},{"key":"9800_CR18","doi-asserted-by":"crossref","unstructured":"Iwama, K.: Intractability of read-once resolution. In: Proceedings of the 10Th Annual Conference on Structure in Complexity Theory (SCTC \u201995), pp 29\u201336. IEEE Computer Society Press, Los Alamitos (1995)","DOI":"10.1109\/SCT.1995.514725"},{"issue":"10","key":"9800_CR19","doi-asserted-by":"publisher","first-page":"503","DOI":"10.1016\/0743-1066(94)90033-7","volume":"19-20","author":"J Jaffar","year":"1994","unstructured":"Jaffar, J., Maher, M.: Constraint logic programming: a survey. The Journal of Logic Programming 19-20(10), 503\u2013581 (1994)","journal-title":"The Journal of Logic Programming"},{"issue":"15","key":"9800_CR20","doi-asserted-by":"publisher","first-page":"3216","DOI":"10.1016\/j.dam.2009.07.002","volume":"157","author":"H Kaplan","year":"2009","unstructured":"Kaplan, H., Nussbaum, Y.: Certifying algorithms for recognizing proper circular-arc graphs and unit circular-arc graphs. Discret. Appl. Math. 157 (15), 3216\u20133230 (2009)","journal-title":"Discret. Appl. Math."},{"key":"9800_CR21","doi-asserted-by":"crossref","unstructured":"Karp, R.M.: Reducibility among combinatorial problems. In: Miller, R.E., Thatcher, J.W. (eds.) Complexity of Computer Computations, pp 85\u2013103. Plenum Press, New York (1972)","DOI":"10.1007\/978-1-4684-2001-2_9"},{"key":"9800_CR22","doi-asserted-by":"crossref","unstructured":"B\u00fcning, H.K. , Wojciechowski, J.P., Chandrasekaran, R. , Subramani, K.: Restricted cutting plane proofs in horn constraint systems. In: Herzig, A., Popescu, A. (eds.) Frontiers of Combining Systems - 12th International Symposium, FroCoS 2019, London, UK, 4-6 September, Proceedings, volume 11715 of Lecture Notes in Computer Science, pp. 149\u2013164. Springer (2019)","DOI":"10.1007\/978-3-030-29007-8_9"},{"key":"9800_CR23","doi-asserted-by":"publisher","first-page":"42","DOI":"10.1016\/j.tcs.2018.02.002","volume":"729","author":"KH B\u00fcning","year":"2018","unstructured":"B\u00fcning, K.H., Wojciechowski, J.P., Subramani, K.: Finding read-once resolution refutations in systems of 2 CNF, clauses. Theor. Comput. Sci. 729, 42\u201356 (2018)","journal-title":"Theor. Comput. Sci."},{"key":"9800_CR24","unstructured":"B\u00fcning, K.H., Wojciechowski, J.P., Subramani, K.: New results on cutting plane proofs for Horn constraint systems. In: 39th IARCS Annual Conference on Foundations of Software Technology and Theoretical Computer Science, FSTTCS 11-13 December 2019, Bombay, India, pp. 43:1\u201343:14 (2019)"},{"key":"9800_CR25","doi-asserted-by":"crossref","unstructured":"Komuravelli, A., bj\u00f8rner, N., Gurfinkel, A., McMillan, K.L.: Compositional verification of procedural programs using Horn clauses over integers and arrays. In: Formal Methods in Computer-Aided Design, FMCAD Austin, Texas, USA 27-30 September 2015. pp. 89\u201396 (2015)","DOI":"10.1109\/FMCAD.2015.7542257"},{"key":"9800_CR26","unstructured":"Kratsch, D., McConnell, R.M., Mehlhorn, K., Spinrad, J.: Certifying algorithms for recognizing interval graphs and permutation graphs. In: SODA. pp. 158\u2013167 (2003)"},{"key":"9800_CR27","doi-asserted-by":"crossref","unstructured":"Lau, K.-K., Ornaghi, M.: Specifying compositional units for correct program development in computational logic. In: Program Development in Computational Logic: A Decade of Research Advances in Logic-Based Program Development, pp. 1\u201329. Springer (2004)","DOI":"10.1007\/978-3-540-25951-0_1"},{"issue":"2","key":"9800_CR28","doi-asserted-by":"publisher","first-page":"119","DOI":"10.1016\/j.cosrev.2010.09.009","volume":"5","author":"RM McConnell","year":"2011","unstructured":"McConnell, R.M., Mehlhorn, K., N\u00e4her, S., Schweitzer, P.: Certifying algorithms. Comput. Sci. Rev. 5(2), 119\u2013161 (2011)","journal-title":"Comput. Sci. Rev."},{"key":"9800_CR29","unstructured":"Nemhauser, G.L., Wolsey, L.A.: Integer and combinatorial Optimization. Wiley, New York (1999)"},{"issue":"3","key":"9800_CR30","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. Symb. Log. 62(3), 981\u2013998 (1997)","journal-title":"J. Symb. Log."},{"key":"9800_CR31","unstructured":"Schrijver, A.: Theory of linear and integer Programming. Wiley, New York (1987)"},{"key":"9800_CR32","unstructured":"SRI International: Yices: An SMT solver. http:\/\/yices.csl.sri.com\/"},{"issue":"2","key":"9800_CR33","doi-asserted-by":"publisher","first-page":"121","DOI":"10.1007\/s10817-009-9139-4","volume":"43","author":"K Subramani","year":"2009","unstructured":"Subramani, K.: Optimal length resolution refutations of difference constraint systems. J. Autom. Reason. (JAR) 43(2), 121\u2013137 (2009)","journal-title":"J. Autom. Reason. (JAR)"},{"issue":"7","key":"9800_CR34","doi-asserted-by":"publisher","first-page":"2765","DOI":"10.1007\/s00453-019-00554-z","volume":"81","author":"K Subramani","year":"2019","unstructured":"Subramani, K., Wojciechowki, P.: A polynomial time algorithm for read-once certification of linear infeasibility in UTVPI constraints. Algorithmica 81 (7), 2765\u20132794 (2019)","journal-title":"Algorithmica"},{"key":"9800_CR35","doi-asserted-by":"crossref","unstructured":"Szeider, S.: NP-completeness of refutability by literal-once resolution. In: Automated Reasoning, First International Joint Conference, IJCAR 2001, Siena, Italy, June 18-23, 2001, Proceedings, vol. 2083 pp. 168\u2013181 (2001)","DOI":"10.1007\/3-540-45744-5_13"},{"key":"9800_CR36","unstructured":"Truemper, K.: Personal communication (2003)"},{"key":"9800_CR37","doi-asserted-by":"publisher","first-page":"371","DOI":"10.1137\/1010063","volume":"10","author":"AF Veinott","year":"1968","unstructured":"Veinott, A.F., Dantzig, G.B.: Integral extreme points. SIAM Rev. 10, 371\u2013372 (1968)","journal-title":"SIAM Rev."}],"container-title":["Annals of Mathematics and Artificial Intelligence"],"original-title":[],"language":"en","link":[{"URL":"https:\/\/link.springer.com\/content\/pdf\/10.1007\/s10472-022-09800-7.pdf","content-type":"application\/pdf","content-version":"vor","intended-application":"text-mining"},{"URL":"https:\/\/link.springer.com\/article\/10.1007\/s10472-022-09800-7\/fulltext.html","content-type":"text\/html","content-version":"vor","intended-application":"text-mining"},{"URL":"https:\/\/link.springer.com\/content\/pdf\/10.1007\/s10472-022-09800-7.pdf","content-type":"application\/pdf","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2024,9,26]],"date-time":"2024-09-26T08:03:12Z","timestamp":1727337792000},"score":1,"resource":{"primary":{"URL":"https:\/\/link.springer.com\/10.1007\/s10472-022-09800-7"}},"subtitle":["Horn constraint systems and cutting plane refutations"],"short-title":[],"issued":{"date-parts":[[2022,6,1]]},"references-count":37,"journal-issue":{"issue":"10","published-print":{"date-parts":[[2022,10]]}},"alternative-id":["9800"],"URL":"https:\/\/doi.org\/10.1007\/s10472-022-09800-7","relation":{},"ISSN":["1012-2443","1573-7470"],"issn-type":[{"value":"1012-2443","type":"print"},{"value":"1573-7470","type":"electronic"}],"subject":[],"published":{"date-parts":[[2022,6,1]]},"assertion":[{"value":"28 April 2022","order":1,"name":"accepted","label":"Accepted","group":{"name":"ArticleHistory","label":"Article History"}},{"value":"1 June 2022","order":2,"name":"first_online","label":"First Online","group":{"name":"ArticleHistory","label":"Article History"}},{"order":1,"name":"Ethics","group":{"name":"EthicsHeading","label":"Declarations"}},{"value":"The authors declare that they have no conflict of interest.","order":2,"name":"Ethics","group":{"name":"EthicsHeading","label":"<!--Emphasis Type='Bold' removed-->Conflict of Interests"}}]}}