{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2025,12,31]],"date-time":"2025-12-31T00:01:22Z","timestamp":1767139282212,"version":"build-2238731810"},"reference-count":27,"publisher":"Springer Science and Business Media LLC","issue":"2","license":[{"start":{"date-parts":[[2024,1,6]],"date-time":"2024-01-06T00:00:00Z","timestamp":1704499200000},"content-version":"tdm","delay-in-days":0,"URL":"https:\/\/www.springernature.com\/gp\/researchers\/text-and-data-mining"},{"start":{"date-parts":[[2024,1,6]],"date-time":"2024-01-06T00:00:00Z","timestamp":1704499200000},"content-version":"vor","delay-in-days":0,"URL":"https:\/\/www.springernature.com\/gp\/researchers\/text-and-data-mining"}],"funder":[{"DOI":"10.13039\/100006502","name":"Defense Sciences Office, DARPA","doi-asserted-by":"publisher","award":["HR001123S0001-FP-004"],"award-info":[{"award-number":["HR001123S0001-FP-004"]}],"id":[{"id":"10.13039\/100006502","id-type":"DOI","asserted-by":"publisher"}]}],"content-domain":{"domain":["link.springer.com"],"crossmark-restriction":false},"short-container-title":["Theory Comput Syst"],"published-print":{"date-parts":[[2024,4]]},"DOI":"10.1007\/s00224-023-10156-6","type":"journal-article","created":{"date-parts":[[2024,1,6]],"date-time":"2024-01-06T01:01:41Z","timestamp":1704502901000},"page":"227-249","update-policy":"https:\/\/doi.org\/10.1007\/springer_crossmark_policy","source":"Crossref","is-referenced-by-count":0,"title":["Farkas Bounds on Horn Constraint Systems"],"prefix":"10.1007","volume":"68","author":[{"given":"K.","family":"Subramani","sequence":"first","affiliation":[]},{"given":"Piotr","family":"Wojciechowski","sequence":"additional","affiliation":[]},{"given":"Alvaro","family":"Velasquez","sequence":"additional","affiliation":[]}],"member":"297","published-online":{"date-parts":[[2024,1,6]]},"reference":[{"key":"10156_CR1","doi-asserted-by":"crossref","unstructured":"Bakhirkin, A., Monniaux, D.: Combining forward and backward abstract interpretation of Horn clauses. Static Analysis - 24th International Symposium, SAS 2017, New York, USA, August 30 - September 1, 2017, Proceedings, pages 23\u201345 (2017)","DOI":"10.1007\/978-3-319-66706-5_2"},{"key":"10156_CR2","doi-asserted-by":"crossref","unstructured":"Bj\u00f8rner, N., Gurfinkel, A., McMillan, K., 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, pages 24\u201351 (2015)","DOI":"10.1007\/978-3-319-23534-9_2"},{"key":"10156_CR3","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. Discrete Optimization 10, 85\u2013101 (2013)","journal-title":"Discrete Optimization"},{"key":"10156_CR4","doi-asserted-by":"crossref","unstructured":"De Angelis, E., Fioravanti, F., Pettorossi, A., Proietti, M.: Verimap: a tool for verifying programs through transformations. In: International Conference on Tools and Algorithms for the Construction and Analysis of Systems, pages 568\u2013574. Springer (2014)","DOI":"10.1007\/978-3-642-54862-8_47"},{"key":"10156_CR5","doi-asserted-by":"crossref","unstructured":"De Moura, L., Bj\u00f8rner, N.: Z3: An efficient SMT solver. Microsoft Research (2008). http:\/\/research.microsoft.com\/projects\/z3\/","DOI":"10.1007\/978-3-540-78800-3_24"},{"key":"10156_CR6","doi-asserted-by":"crossref","unstructured":"Farkas, G.: \u00dcber die Theorie der Einfachen Ungleichungen. J. f\u00fcr die Reine und Angewandte Mathematik, 124(124), 1\u201327 (1902)","DOI":"10.1515\/crll.1902.124.1"},{"key":"10156_CR7","doi-asserted-by":"crossref","unstructured":"Fedyukovich, G., Prabhu, S., Madhukar, K., Gupta, A.: Solving constrained horn clauses using syntax and data. In: 2018 Formal Methods in Computer Aided Design (FMCAD), pages 1\u20139. IEEE, (2018)","DOI":"10.23919\/FMCAD.2018.8603011"},{"issue":"6","key":"10156_CR8","doi-asserted-by":"publisher","first-page":"405","DOI":"10.1145\/2345156.2254112","volume":"47","author":"S Grebenshchikov","year":"2012","unstructured":"Grebenshchikov, S., Lopes, N.P., Popeea, C., Rybalchenko, A.: Synthesizing software verifiers from proof rules. ACM SIGPLAN Notices 47(6), 405\u2013416 (2012)","journal-title":"ACM SIGPLAN Notices"},{"key":"10156_CR9","doi-asserted-by":"crossref","unstructured":"Hojjat, H., R\u00fcmmer, P.: The Eldarica Horn solver. In: 2018 Formal Methods in Computer Aided Design (FMCAD), pages 1\u20137. IEEE, (2018)","DOI":"10.23919\/FMCAD.2018.8603013"},{"key":"10156_CR10","doi-asserted-by":"crossref","unstructured":"Iwama, K., Miyano, E.: Intractability of read-once resolution. In: Proceedings of the 10th Annual Conference on Structure in Complexity Theory (SCTC \u201995), pages 29\u201336, Los Alamitos, CA, USA, June 1995. IEEE Computer Society Press","DOI":"10.1109\/SCT.1995.514725"},{"key":"10156_CR11","doi-asserted-by":"crossref","unstructured":"Kafle, B., Gallagher, J.P., Morales, J.F.: Rahft: a tool for verifying Horn clauses using abstract interpretation and finite tree automata. In: International Conference on Computer Aided Verification, pages 261\u2013268. Springer, (2016)","DOI":"10.1007\/978-3-319-41528-4_14"},{"key":"10156_CR12","doi-asserted-by":"crossref","unstructured":"Karp, R.M.: Reducibility among combinatorial problems. In: Miller, R.\u00a0E., Thatcher, J.\u00a0W. (eds.), Complexity of Computer Computations, pages 85\u2013103, New York, 1972. Plenum Press","DOI":"10.1007\/978-1-4684-2001-2_9"},{"key":"10156_CR13","doi-asserted-by":"crossref","unstructured":"Kleine B\u00fcning, H., Wojciechowski, P., Chandrasekaran, R. and 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, September 4-6, 2019, Proceedings, vol. 11715 of Lecture Notes in Computer Science, pages 149\u2013164. Springer (2019)","DOI":"10.1007\/978-3-030-29007-8_9"},{"key":"10156_CR14","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., Subramani, K.: Finding read-once resolution refutations in systems of 2CNF clauses. Theor. Comput. Sci. 729, 42\u201356 (2018)","journal-title":"Theor. Comput. Sci."},{"key":"10156_CR15","unstructured":"B\u00fcning, HK., Wojciechowski, 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 2019, December 11-13, 2019, Bombay, India, pages 43:1\u201343:14 (2019)"},{"key":"10156_CR16","doi-asserted-by":"crossref","unstructured":"B\u00fcning, HK., Wojciechowski, P., Subramani, K.: Read-once resolutions in Horn formulas.In: Frontiers in Algorithmics - 13th International Workshop, FAW 2019, Sanya, China, April 29 - May 3, 2019, Proceedings, pages 100\u2013110 (2019)","DOI":"10.1007\/978-3-030-18126-0_9"},{"issue":"3","key":"10156_CR17","doi-asserted-by":"publisher","first-page":"175","DOI":"10.1007\/s10703-016-0249-4","volume":"48","author":"A Komuravelli","year":"2016","unstructured":"Komuravelli, A., Gurfinkel, A., Chaki, S.: Smt-based model checking for recursive programs. Formal Methods in System Design 48(3), 175\u2013205 (2016)","journal-title":"Formal Methods in System Design"},{"key":"10156_CR18","unstructured":"LiCalzi, M., Veinott, A.F.: Subextremal functions and lattice programming. SSRN Electronic J., 10 2005"},{"key":"10156_CR19","volume-title":"Integer and Combinatorial Optimization","author":"LA Wolsey","year":"1999","unstructured":"Wolsey, L.A., Nemhauser, G.L.: Integer and Combinatorial Optimization. John Wiley & Sons, New York (1999)"},{"key":"10156_CR20","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":"1","key":"10156_CR21","doi-asserted-by":"publisher","first-page":"23","DOI":"10.1145\/321250.321253","volume":"12","author":"JA Robinson","year":"1965","unstructured":"Robinson, J.A.: A machine-oriented logic based on the resolution principle. J. ACM 12(1), 23\u201341 (1965)","journal-title":"J. ACM"},{"key":"10156_CR22","volume-title":"Theory of Linear and Integer Programming","author":"A Schrijver","year":"1987","unstructured":"Schrijver, A.: Theory of Linear and Integer Programming. John Wiley and Sons, New York (1987)"},{"issue":"2","key":"10156_CR23","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. Auto. Reas. (JAR) 43(2), 121\u2013137 (2009)","journal-title":"J. Auto. Reas. (JAR)"},{"issue":"7","key":"10156_CR24","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"},{"issue":"1","key":"10156_CR25","doi-asserted-by":"publisher","first-page":"166","DOI":"10.1007\/s00453-016-0131-1","volume":"78","author":"K Subramani","year":"2017","unstructured":"Subramani, K., Wojciechowki, P.: A combinatorial certifying algorithm for linear feasibility in UTVPI constraints. Algorithmica 78(1), 166\u2013208 (2017)","journal-title":"Algorithmica"},{"key":"10156_CR26","doi-asserted-by":"crossref","unstructured":"Subramani, K., Wojciechowski, P., Velasquez, A.: On the copy complexity of width 3 Horn constraint systems. In: Konev, B., Reger, G. (eds.) editors, Frontiers of Combining Systems - 13th International Symposium, FroCoS 2021, Birmingham, UK, September 8-10, 2021, Proceedings, vol. 12941 of Lecture Notes in Computer Science, pages 63\u201378. Springer (2021)","DOI":"10.1007\/978-3-030-86205-3_4"},{"key":"10156_CR27","doi-asserted-by":"publisher","first-page":"70","DOI":"10.1016\/j.tcs.2021.08.017","volume":"890","author":"P Wojciechowski","year":"2021","unstructured":"Wojciechowski, P., Subramani, K.: Copy complexity of Horn formulas with respect to unit read-once resolution. Theor. Comput. Sci. 890, 70\u201386 (2021)","journal-title":"Theor. Comput. Sci."}],"updated-by":[{"DOI":"10.1007\/s00224-025-10219-w","type":"correction","label":"Correction","source":"publisher","updated":{"date-parts":[[2025,4,26]],"date-time":"2025-04-26T00:00:00Z","timestamp":1745625600000}}],"container-title":["Theory of Computing Systems"],"original-title":[],"language":"en","link":[{"URL":"https:\/\/link.springer.com\/content\/pdf\/10.1007\/s00224-023-10156-6.pdf","content-type":"application\/pdf","content-version":"vor","intended-application":"text-mining"},{"URL":"https:\/\/link.springer.com\/article\/10.1007\/s00224-023-10156-6\/fulltext.html","content-type":"text\/html","content-version":"vor","intended-application":"text-mining"},{"URL":"https:\/\/link.springer.com\/content\/pdf\/10.1007\/s00224-023-10156-6.pdf","content-type":"application\/pdf","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2025,4,26]],"date-time":"2025-04-26T14:02:33Z","timestamp":1745676153000},"score":1,"resource":{"primary":{"URL":"https:\/\/link.springer.com\/10.1007\/s00224-023-10156-6"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2024,1,6]]},"references-count":27,"journal-issue":{"issue":"2","published-print":{"date-parts":[[2024,4]]}},"alternative-id":["10156"],"URL":"https:\/\/doi.org\/10.1007\/s00224-023-10156-6","relation":{},"ISSN":["1432-4350","1433-0490"],"issn-type":[{"value":"1432-4350","type":"print"},{"value":"1433-0490","type":"electronic"}],"subject":[],"published":{"date-parts":[[2024,1,6]]},"assertion":[{"value":"22 November 2023","order":1,"name":"accepted","label":"Accepted","group":{"name":"ArticleHistory","label":"Article History"}},{"value":"6 January 2024","order":2,"name":"first_online","label":"First Online","group":{"name":"ArticleHistory","label":"Article History"}},{"value":"25 April 2025","order":3,"name":"change_date","label":"Change Date","group":{"name":"ArticleHistory","label":"Article History"}},{"value":"Update","order":4,"name":"change_type","label":"Change Type","group":{"name":"ArticleHistory","label":"Article History"}},{"value":"The original version of this paper was updated. The family name of the second author, Piotr Wojciechowski was incorrectly written as Piotr Wojciechowki.","order":5,"name":"change_details","label":"Change Details","group":{"name":"ArticleHistory","label":"Article History"}},{"value":"26 April 2025","order":6,"name":"change_date","label":"Change Date","group":{"name":"ArticleHistory","label":"Article History"}},{"value":"Correction","order":7,"name":"change_type","label":"Change Type","group":{"name":"ArticleHistory","label":"Article History"}},{"value":"A Correction to this paper has been published:","order":8,"name":"change_details","label":"Change Details","group":{"name":"ArticleHistory","label":"Article History"}},{"value":"https:\/\/doi.org\/10.1007\/s00224-025-10219-w","URL":"https:\/\/doi.org\/10.1007\/s00224-025-10219-w","order":9,"name":"change_details","label":"Change Details","group":{"name":"ArticleHistory","label":"Article History"}},{"order":1,"name":"Ethics","group":{"name":"EthicsHeading","label":"Declarations"}},{"value":"The authors declare no competing interests.","order":2,"name":"Ethics","group":{"name":"EthicsHeading","label":"Competing interests"}}]}}