{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2026,3,18]],"date-time":"2026-03-18T04:40:21Z","timestamp":1773808821091,"version":"3.50.1"},"reference-count":28,"publisher":"Springer Science and Business Media LLC","issue":"7","license":[{"start":{"date-parts":[[2019,3,2]],"date-time":"2019-03-02T00:00:00Z","timestamp":1551484800000},"content-version":"tdm","delay-in-days":0,"URL":"http:\/\/www.springer.com\/tdm"}],"content-domain":{"domain":["link.springer.com"],"crossmark-restriction":false},"short-container-title":["Algorithmica"],"published-print":{"date-parts":[[2019,7]]},"DOI":"10.1007\/s00453-019-00554-z","type":"journal-article","created":{"date-parts":[[2019,3,2]],"date-time":"2019-03-02T07:32:13Z","timestamp":1551511933000},"page":"2765-2794","update-policy":"https:\/\/doi.org\/10.1007\/springer_crossmark_policy","source":"Crossref","is-referenced-by-count":21,"title":["A Polynomial Time Algorithm for Read-Once Certification of Linear Infeasibility in UTVPI Constraints"],"prefix":"10.1007","volume":"81","author":[{"ORCID":"https:\/\/orcid.org\/0000-0001-5821-5117","authenticated-orcid":false,"given":"K.","family":"Subramani","sequence":"first","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"ORCID":"https:\/\/orcid.org\/0000-0003-1684-1077","authenticated-orcid":false,"given":"Piotr","family":"Wojciechowki","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]}],"member":"297","published-online":{"date-parts":[[2019,3,2]]},"reference":[{"key":"554_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). Lecture Notes in Computer Science, pp. 176\u2013184. Springer, Berlin (1998)","DOI":"10.1007\/BFb0055766"},{"key":"554_CR2","first-page":"66","volume":"65","author":"P Beame","year":"1998","unstructured":"Beame, P., Pitassi, T.: Propositional proof complexity: past, present, future. Bull. EATCS 65, 66\u201389 (1998)","journal-title":"Bull. EATCS"},{"key":"554_CR3","volume-title":"Introduction to Algorithms","author":"TH Cormen","year":"2001","unstructured":"Cormen, T.H., Leiserson, C.E., Rivest, R.L., Stein, C.: Introduction to Algorithms. MIT Press, Cambridge (2001)"},{"key":"554_CR4","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. In: POPL, pp. 238\u2013252 (1977)","DOI":"10.1145\/512950.512973"},{"issue":"1","key":"554_CR5","doi-asserted-by":"publisher","first-page":"8:1","DOI":"10.1145\/3155301","volume":"14","author":"R Duan","year":"2018","unstructured":"Duan, R., Pettie, S., Hsin-Hao, S.: Scaling algorithms for weighted matching in general graphs. ACM Trans. Algorithms 14(1), 8:1\u20138:35 (2018)","journal-title":"ACM Trans. Algorithms"},{"key":"554_CR6","volume-title":"An Introduction to Matching. Engineering Summer Conference on Mimeographed Notes","author":"J Edmonds","year":"1967","unstructured":"Edmonds, J.: An Introduction to Matching. Engineering Summer Conference on Mimeographed Notes. University of Michigan, Ann Arbor (1967)"},{"issue":"124","key":"554_CR7","first-page":"1","volume":"124","author":"G Farkas","year":"1902","unstructured":"Farkas, G.: \u00dcber die Theorie der Einfachen Ungleichungen. J. Reine Angew. Math. 124(124), 1\u201327 (1902)","journal-title":"J. Reine Angew. Math."},{"key":"554_CR8","doi-asserted-by":"publisher","first-page":"111","DOI":"10.1016\/0304-3975(80)90009-2","volume":"10","author":"S Fortune","year":"1980","unstructured":"Fortune, S., Hopcroft, J.E., Wyllie, J.: The directed subgraph homeomorphism problem. Theor. Comput. Sci. 10, 111\u2013121 (1980)","journal-title":"Theor. Comput. Sci."},{"issue":"2","key":"554_CR9","doi-asserted-by":"publisher","first-page":"221","DOI":"10.1145\/321941.321942","volume":"23","author":"HN Gabow","year":"1976","unstructured":"Gabow, H.N.: An efficient implementation of Edmonds\u2019 algorithm for maximum matching on graphs. J. ACM 23(2), 221\u2013234 (1976)","journal-title":"J. ACM"},{"key":"554_CR10","first-page":"434","volume-title":"Proceedings of the 1st Annual ACM-SIAM Symposium on Discrete Algorithms (SODA \u201990)","author":"HN Gabow","year":"1990","unstructured":"Gabow, H.N.: Data structures for weighted matching and nearest common ancestors with linking. In: Johnson, D. (ed.) Proceedings of the 1st Annual ACM-SIAM Symposium on Discrete Algorithms (SODA \u201990), pp. 434\u2013443. SIAM, San Francisco (1990)"},{"issue":"3","key":"554_CR11","doi-asserted-by":"publisher","first-page":"471","DOI":"10.1109\/12.372041","volume":"44","author":"R Gerber","year":"1995","unstructured":"Gerber, R., Pugh, W., Saksena, M.: Parametric dispatching of hard real-time tasks. IEEE Trans. Comput. 44(3), 471\u2013479 (1995)","journal-title":"IEEE Trans. Comput."},{"issue":"2\u20133","key":"554_CR12","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\u20133), 297\u2013308 (1985)","journal-title":"Theor. Comput. Sci."},{"issue":"6","key":"554_CR13","doi-asserted-by":"publisher","first-page":"1179","DOI":"10.1137\/S0097539793251876","volume":"23","author":"DS Hochbaum","year":"1994","unstructured":"Hochbaum, D.S., Naor, J.: Simple and fast algorithms for linear and integer programs with two variables per inequality. SIAM J. Comput. 23(6), 1179\u20131192 (1994)","journal-title":"SIAM J. Comput."},{"key":"554_CR14","doi-asserted-by":"publisher","first-page":"309","DOI":"10.1007\/BFb0029974","volume":"1295","author":"K Iwama","year":"1997","unstructured":"Iwama, K.: Complexity of finding short resolution proofs. Lect. Notes Comput. Sci. 1295, 309\u2013319 (1997)","journal-title":"Lect. Notes Comput. Sci."},{"key":"554_CR15","doi-asserted-by":"publisher","first-page":"29","DOI":"10.1109\/SCT.1995.514725","volume-title":"Proceedings of the 10th Annual Conference on Structure in Complexity Theory (SCTC \u201995)","author":"K Iwama","year":"1995","unstructured":"Iwama, K., Miyano, E.: Intractability of read-once resolution. Proceedings of the 10th Annual Conference on Structure in Complexity Theory (SCTC \u201995), pp. 29\u201336. IEEE Computer Society Press, Los Alamitos (1995)"},{"key":"554_CR16","doi-asserted-by":"publisher","first-page":"42","DOI":"10.1016\/j.tcs.2018.02.002","volume":"729","author":"HK B\u00fcning","year":"2018","unstructured":"B\u00fcning, H.K., Wojciechowski, P.J., Subramani, K.: Finding read-once resolution refutations in systems of 2cnf clauses. Theor. Comput. Sci. 729, 42\u201356 (2018)","journal-title":"Theor. Comput. Sci."},{"issue":"4","key":"554_CR17","doi-asserted-by":"publisher","first-page":"419","DOI":"10.1023\/A:1016339119669","volume":"36","author":"HK B\u00fcning","year":"2002","unstructured":"B\u00fcning, H.K., Zhao, X.: The complexity of read-once resolution. Ann. Math. Artif. Intell. 36(4), 419\u2013435 (2002)","journal-title":"Ann. Math. Artif. Intell."},{"key":"554_CR18","volume-title":"Combinatorial Optimization. Number\u00a021 in Algorithms and Combinatorics","author":"B Korte","year":"2010","unstructured":"Korte, B., Vygen, J.: Combinatorial Optimization. Number\u00a021 in Algorithms and Combinatorics, vol. 4. Springer, New York (2010)"},{"key":"554_CR19","doi-asserted-by":"crossref","unstructured":"Lahiri, S.K., Musuvathi, M.: An efficient decision procedure for UTVPI constraints. In: Proceedings of the \n                    \n                      \n                    \n                    $$5{\\rm th}$$\n                    \n                      \n                        \n                          5\n                          th\n                        \n                      \n                    \n                   International Workshop on the Frontiers of Combining Systems, September 19-21, Vienna, Austria, pp. 168\u2013183. Springer, New York (2005)","DOI":"10.1007\/11559306_9"},{"issue":"1","key":"554_CR20","doi-asserted-by":"publisher","first-page":"31","DOI":"10.1007\/s10990-006-8609-1","volume":"19","author":"A Min\u00e9","year":"2006","unstructured":"Min\u00e9, A.: The octagon abstract domain. Higher Order Symb. Comput. 19(1), 31\u2013100 (2006)","journal-title":"Higher Order Symb. Comput."},{"key":"554_CR21","volume-title":"Integer and Combinatorial Optimization","author":"GL Nemhauser","year":"1999","unstructured":"Nemhauser, G.L., Wolsey, L.A.: Integer and Combinatorial Optimization. Wiley, New York (1999)"},{"key":"554_CR22","unstructured":"Revesz, P.Z.: Tightened transitive closure of integer addition constraints. In: Symposium on Abstraction, Reformulation, and Approximation (SARA), pp. 136\u2013142 (2009)"},{"key":"554_CR23","volume-title":"Theory of Linear and Integer Programming","author":"A Schrijver","year":"1987","unstructured":"Schrijver, A.: Theory of Linear and Integer Programming. Wiley, New York (1987)"},{"issue":"2","key":"554_CR24","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. 43(2), 121\u2013137 (2009)","journal-title":"J. Autom. Reason."},{"issue":"2","key":"554_CR25","doi-asserted-by":"publisher","first-page":"319","DOI":"10.1007\/s00165-011-0186-3","volume":"25","author":"K Subramani","year":"2013","unstructured":"Subramani, K., Williamson, M., Gu, X.: Improved algorithms for optimal length resolution refutation in difference constraint systems. Formal Asp. Comput. 25(2), 319\u2013341 (2013)","journal-title":"Formal Asp. Comput."},{"issue":"1","key":"554_CR26","doi-asserted-by":"publisher","first-page":"166","DOI":"10.1007\/s00453-016-0131-1","volume":"78","author":"K Subramani","year":"2017","unstructured":"Subramani, K., Wojciechowski, P.J.: A combinatorial certifying algorithm for linear feasibility in UTVPI constraints. Algorithmica 78(1), 166\u2013208 (2017)","journal-title":"Algorithmica"},{"key":"554_CR27","doi-asserted-by":"crossref","unstructured":"Szeider, S.: Np-completeness of refutability by literal-once resolution. In: Proceeding of the Automated Reasoning, First International Joint Conference, IJCAR 2001, Siena, Italy, June 18\u201323, 2001, pp. 168\u2013181 (2001)","DOI":"10.1007\/3-540-45744-5_13"},{"issue":"4","key":"554_CR28","doi-asserted-by":"publisher","first-page":"425","DOI":"10.2178\/bsl\/1203350879","volume":"1","author":"A Urquhart","year":"1995","unstructured":"Urquhart, A.: The complexity of propositional proofs. Bull. Symb. Logic 1(4), 425\u2013467 (1995)","journal-title":"Bull. Symb. Logic"}],"container-title":["Algorithmica"],"original-title":[],"language":"en","link":[{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/s00453-019-00554-z.pdf","content-type":"application\/pdf","content-version":"vor","intended-application":"text-mining"},{"URL":"http:\/\/link.springer.com\/article\/10.1007\/s00453-019-00554-z\/fulltext.html","content-type":"text\/html","content-version":"vor","intended-application":"text-mining"},{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/s00453-019-00554-z.pdf","content-type":"application\/pdf","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2020,2,29]],"date-time":"2020-02-29T19:08:20Z","timestamp":1583003300000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/s00453-019-00554-z"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2019,3,2]]},"references-count":28,"journal-issue":{"issue":"7","published-print":{"date-parts":[[2019,7]]}},"alternative-id":["554"],"URL":"https:\/\/doi.org\/10.1007\/s00453-019-00554-z","relation":{},"ISSN":["0178-4617","1432-0541"],"issn-type":[{"value":"0178-4617","type":"print"},{"value":"1432-0541","type":"electronic"}],"subject":[],"published":{"date-parts":[[2019,3,2]]},"assertion":[{"value":"15 January 2018","order":1,"name":"received","label":"Received","group":{"name":"ArticleHistory","label":"Article History"}},{"value":"21 February 2019","order":2,"name":"accepted","label":"Accepted","group":{"name":"ArticleHistory","label":"Article History"}},{"value":"2 March 2019","order":3,"name":"first_online","label":"First Online","group":{"name":"ArticleHistory","label":"Article History"}}]}}