{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2026,1,25]],"date-time":"2026-01-25T14:51:28Z","timestamp":1769352688082,"version":"3.49.0"},"publisher-location":"Cham","reference-count":29,"publisher":"Springer Nature Switzerland","isbn-type":[{"value":"9783031712937","type":"print"},{"value":"9783031712944","type":"electronic"}],"license":[{"start":{"date-parts":[[2024,1,1]],"date-time":"2024-01-01T00:00:00Z","timestamp":1704067200000},"content-version":"tdm","delay-in-days":0,"URL":"https:\/\/www.springernature.com\/gp\/researchers\/text-and-data-mining"},{"start":{"date-parts":[[2024,1,1]],"date-time":"2024-01-01T00:00:00Z","timestamp":1704067200000},"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":[[2024]]},"DOI":"10.1007\/978-3-031-71294-4_6","type":"book-chapter","created":{"date-parts":[[2024,9,6]],"date-time":"2024-09-06T14:03:47Z","timestamp":1725631427000},"page":"99-114","update-policy":"https:\/\/doi.org\/10.1007\/springer_crossmark_policy","source":"Crossref","is-referenced-by-count":1,"title":["A Certifying Algorithm for\u00a0Linear (and Integer) Feasibility in\u00a0Horn Constraint Systems"],"prefix":"10.1007","author":[{"ORCID":"https:\/\/orcid.org\/0000-0003-1684-1077","authenticated-orcid":false,"given":"Piotr","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":[[2024,9,7]]},"reference":[{"key":"6_CR1","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"176","DOI":"10.1007\/BFb0055766","volume-title":"Mathematical Foundations of Computer Science 1998","author":"M Alekhnovich","year":"1998","unstructured":"Alekhnovich, M., Buss, S., Moran, S., Pitassi, T.: Minimum propositional proof length is NP-hard to linearly approximate. In: Brim, L., Gruska, J., Zlatu\u0161ka, J. (eds.) MFCS 1998. LNCS, vol. 1450, pp. 176\u2013184. Springer, Heidelberg (1998). https:\/\/doi.org\/10.1007\/BFb0055766"},{"key":"6_CR2","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"23","DOI":"10.1007\/978-3-319-66706-5_2","volume-title":"Static Analysis","author":"A Bakhirkin","year":"2017","unstructured":"Bakhirkin, A., Monniaux, D.: Combining forward and backward abstract interpretation of horn clauses. In: Ranzato, F. (ed.) SAS 2017. LNCS, vol. 10422, pp. 23\u201345. Springer, Cham (2017). https:\/\/doi.org\/10.1007\/978-3-319-66706-5_2"},{"key":"6_CR3","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"24","DOI":"10.1007\/978-3-319-23534-9_2","volume-title":"Fields of Logic and Computation II","author":"N Bj\u00f8rner","year":"2015","unstructured":"Bj\u00f8rner, N., Gurfinkel, A., McMillan, K., Rybalchenko, A.: Horn clause solvers for program verification. In: Beklemishev, L.D., Blass, A., Dershowitz, N., Finkbeiner, B., Schulte, W. (eds.) Fields of Logic and Computation II. LNCS, vol. 9300, pp. 24\u201351. Springer, Cham (2015). https:\/\/doi.org\/10.1007\/978-3-319-23534-9_2"},{"key":"6_CR4","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":"6_CR5","volume-title":"Introduction to Algorithms","author":"TH Cormen","year":"2009","unstructured":"Cormen, T.H., Leiserson, C.E., Rivest, R.L., Stein, C.: Introduction to Algorithms, 3rd edn. The MIT Press, Cambridge (2009)","edition":"3"},{"key":"6_CR6","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"},{"key":"6_CR7","doi-asserted-by":"publisher","first-page":"295","DOI":"10.2307\/1910385","volume":"23","author":"GB Dantzig","year":"1955","unstructured":"Dantzig, G.B.: Optimal solution of a dynamic Leontief model with substitution. Econometrica 23, 295 (1955)","journal-title":"Econometrica"},{"key":"6_CR8","series-title":"Lecture Notes in Computer Science (Lecture Notes in Artificial Intelligence)","doi-asserted-by":"publisher","first-page":"218","DOI":"10.1007\/978-3-540-25984-8_14","volume-title":"Automated Reasoning","author":"L de Moura","year":"2004","unstructured":"de Moura, L., Owre, S., Rue\u00df, H., Rushby, J., Shankar, N.: The ICS decision procedures for embedded deduction. In: Basin, D., Rusinowitch, M. (eds.) IJCAR 2004. LNCS (LNAI), vol. 3097, pp. 218\u2013222. Springer, Heidelberg (2004). https:\/\/doi.org\/10.1007\/978-3-540-25984-8_14"},{"key":"6_CR9","unstructured":"Dutertre, B., de Moura, L.: The YICES SMT solver. Technical report, SRI International (2006)"},{"issue":"124","key":"6_CR10","first-page":"1","volume":"124","author":"G Farkas","year":"1902","unstructured":"Farkas, G.: \u00dcber die Theorie der Einfachen Ungleichungen. J. f\u00fcr die Reine und Angewandte Mathematik 124(124), 1\u201327 (1902)","journal-title":"J. f\u00fcr die Reine und Angewandte Mathematik"},{"key":"6_CR11","series-title":"Lecture Notes in Computer Science (Lecture Notes in Artificial Intelligence)","doi-asserted-by":"publisher","first-page":"347","DOI":"10.1007\/3-540-45620-1_29","volume-title":"Automated Deduction\u2014CADE-18","author":"J Ford","year":"2002","unstructured":"Ford, J., Shankar, N.: Formal verification of a combination decision procedure. In: Voronkov, A. (ed.) CADE 2002. LNCS (LNAI), vol. 2392, pp. 347\u2013362. Springer, Heidelberg (2002). https:\/\/doi.org\/10.1007\/3-540-45620-1_29"},{"key":"6_CR12","doi-asserted-by":"crossref","unstructured":"Iwama, K.,\u00a0Miyano, E.: Intractability of read-once resolution. In: Proceedings of the 10th Annual Conference on Structure in Complexity Theory (SCTC 1995), Los Alamitos, CA, USA, June 1995, pp. 29\u201336. IEEE Computer Society Press (1995)","DOI":"10.1109\/SCT.1995.514725"},{"issue":"10","key":"6_CR13","first-page":"19","volume":"503\u2013581","author":"J Jaffar","year":"1994","unstructured":"Jaffar, J., Maher, M.: Constraint logic programming: a survey. J. Logic Program. 503\u2013581(10), 19\u201320 (1994)","journal-title":"J. Logic Program."},{"key":"6_CR14","doi-asserted-by":"publisher","first-page":"375","DOI":"10.1007\/BF01581090","volume":"57","author":"RG Jeroslow","year":"1992","unstructured":"Jeroslow, R.G., Martin, R.K., Rardin, R.L., Wang, J.: Gainfree Leontief substitution flow problems. Math. Program. 57, 375\u2013414 (1992)","journal-title":"Math. Program."},{"key":"6_CR15","unstructured":"Kimura, K., Makino, K.: A combinatorial certifying algorithm for linear programming problems with gainfree Leontief substitution systems. In: Iwata, S., Kakimura, N. (eds.) 34th International Symposium on Algorithms and Computation, ISAAC 2023, Kyoto, Japan, 3\u20136 December 2023, volume 283 of LIPIcs, pp. 47:1\u201347:17. Schloss Dagstuhl - Leibniz-Zentrum f\u00fcr Informatik 2023"},{"key":"6_CR16","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 2015, Austin, Texas, USA, 27\u201330 September 2015, pp. 89\u201396 (2015)","DOI":"10.1109\/FMCAD.2015.7542257"},{"key":"6_CR17","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"1","DOI":"10.1007\/978-3-540-25951-0_1","volume-title":"Program Development in Computational Logic","author":"K-K Lau","year":"2004","unstructured":"Lau, K.-K., Ornaghi, M.: Specifying compositional units for correct program development in computational logic. In: Bruynooghe, M., Lau, K.-K. (eds.) Program Development in Computational Logic. LNCS, vol. 3049, pp. 1\u201329. Springer, Heidelberg (2004). https:\/\/doi.org\/10.1007\/978-3-540-25951-0_1"},{"key":"6_CR18","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-540-30717-4","volume-title":"Understanding and Using Linear Programming (Universitext)","author":"J Matouek","year":"2006","unstructured":"Matouek, J., G\u00e4rtner, B.: Understanding and Using Linear Programming (Universitext). Springer, Heidelberg (2006). https:\/\/doi.org\/10.1007\/978-3-540-30717-4"},{"issue":"2","key":"6_CR19","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":"6_CR20","volume-title":"The LEDA Platform of Combinatorial and Geometric Computing","author":"K Mehlhorn","year":"1999","unstructured":"Mehlhorn, K., N\u00e4her, S.: The LEDA Platform of Combinatorial and Geometric Computing. Cambridge University Press, Cambridge (1999)"},{"key":"6_CR21","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":"6_CR22","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":"2","key":"6_CR23","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 Aspects Comput. 25(2), 319\u2013341 (2013)","journal-title":"Formal Aspects Comput."},{"issue":"1","key":"6_CR24","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"},{"issue":"2","key":"6_CR25","doi-asserted-by":"publisher","first-page":"389","DOI":"10.1007\/s10878-017-0176-3","volume":"35","author":"K Subramani","year":"2018","unstructured":"Subramani, K., Wojciechowski, P.J.: A certifying algorithm for lattice point feasibility in a system of UTVPI constraints. J. Comb. Optim. 35(2), 389\u2013408 (2018)","journal-title":"J. Comb. Optim."},{"key":"6_CR26","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"226","DOI":"10.1007\/978-3-030-68195-1_18","volume-title":"Language and Automata Theory and Applications","author":"K Subramani","year":"2021","unstructured":"Subramani, K., Wojciechowski, P.: Tree-like unit refutations in horn constraint systems. In: Leporati, A., Mart\u00edn-Vide, C., Shapira, D., Zandron, C. (eds.) LATA 2021. LNCS, vol. 12638, pp. 226\u2013237. Springer, Cham (2021). https:\/\/doi.org\/10.1007\/978-3-030-68195-1_18"},{"key":"6_CR27","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."},{"key":"6_CR28","doi-asserted-by":"publisher","first-page":"239","DOI":"10.1007\/s10817-022-09618-2","volume":"66","author":"P Wojciechowski","year":"2022","unstructured":"Wojciechowski, P., Subramani, K., Chandrasekaran, R.: Analyzing read-once cutting plane proofs in Horn systems. J. Autom. Reason. (JAR) 66, 239\u2013274 (2022)","journal-title":"J. Autom. Reason. (JAR)"},{"key":"6_CR29","doi-asserted-by":"publisher","first-page":"979","DOI":"10.1007\/s10472-022-09800-7","volume":"90","author":"P Wojciechowski","year":"2022","unstructured":"Wojciechowski, P., Subramani, K.: On the lengths of tree-like and dag-like cutting plane refutations of Horn constraint systems. Ann. Math. Artif. Intell. 90, 979\u2013995 (2022)","journal-title":"Ann. Math. Artif. Intell."}],"container-title":["Lecture Notes in Computer Science","Logic-Based Program Synthesis and Transformation"],"original-title":[],"language":"en","link":[{"URL":"https:\/\/link.springer.com\/content\/pdf\/10.1007\/978-3-031-71294-4_6","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2024,11,27]],"date-time":"2024-11-27T21:15:16Z","timestamp":1732742116000},"score":1,"resource":{"primary":{"URL":"https:\/\/link.springer.com\/10.1007\/978-3-031-71294-4_6"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2024]]},"ISBN":["9783031712937","9783031712944"],"references-count":29,"URL":"https:\/\/doi.org\/10.1007\/978-3-031-71294-4_6","relation":{},"ISSN":["0302-9743","1611-3349"],"issn-type":[{"value":"0302-9743","type":"print"},{"value":"1611-3349","type":"electronic"}],"subject":[],"published":{"date-parts":[[2024]]},"assertion":[{"value":"7 September 2024","order":1,"name":"first_online","label":"First Online","group":{"name":"ChapterHistory","label":"Chapter History"}},{"value":"LOPSTR","order":1,"name":"conference_acronym","label":"Conference Acronym","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"International Symposium on Logic-Based Program Synthesis and Transformation","order":2,"name":"conference_name","label":"Conference Name","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"Milan","order":3,"name":"conference_city","label":"Conference City","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"Italy","order":4,"name":"conference_country","label":"Conference Country","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"2024","order":5,"name":"conference_year","label":"Conference Year","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"9 September 2024","order":7,"name":"conference_start_date","label":"Conference Start Date","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"10 September 2024","order":8,"name":"conference_end_date","label":"Conference End Date","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"34","order":9,"name":"conference_number","label":"Conference Number","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"lopstr2024","order":10,"name":"conference_id","label":"Conference ID","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"https:\/\/www.fm24.polimi.it\/?page_id=63#lopstrppdp2024","order":11,"name":"conference_url","label":"Conference URL","group":{"name":"ConferenceInfo","label":"Conference Information"}}]}}