{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2025,7,3]],"date-time":"2025-07-03T04:21:28Z","timestamp":1751516488259,"version":"3.41.0"},"publisher-location":"Cham","reference-count":17,"publisher":"Springer International Publishing","isbn-type":[{"type":"print","value":"9783319784540"},{"type":"electronic","value":"9783319784557"}],"license":[{"start":{"date-parts":[[2018,1,1]],"date-time":"2018-01-01T00:00:00Z","timestamp":1514764800000},"content-version":"unspecified","delay-in-days":0,"URL":"http:\/\/www.springer.com\/tdm"}],"content-domain":{"domain":["link.springer.com"],"crossmark-restriction":false},"short-container-title":[],"published-print":{"date-parts":[[2018]]},"DOI":"10.1007\/978-3-319-78455-7_23","type":"book-chapter","created":{"date-parts":[[2018,3,20]],"date-time":"2018-03-20T08:53:10Z","timestamp":1521535990000},"page":"300-314","update-policy":"https:\/\/doi.org\/10.1007\/springer_crossmark_policy","source":"Crossref","is-referenced-by-count":2,"title":["Optimal Length Tree-Like Refutations of\u00a0Linear Feasibility in UTVPI Constraints"],"prefix":"10.1007","author":[{"given":"P.","family":"Wojciechowski","sequence":"first","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"K.","family":"Subramani","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Matthew","family":"Williamson","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]}],"member":"297","published-online":{"date-parts":[[2018,3,21]]},"reference":[{"key":"23_CR1","doi-asserted-by":"crossref","unstructured":"Patrick Cousot and Radhia Cousot. Abstract interpretation: A unified lattice model for static analysis of programs by construction or approximation of fixpoints. In POPL, pages 238\u2013252, 1977","DOI":"10.1145\/512950.512973"},{"issue":"124","key":"23_CR2","first-page":"1","volume":"124","author":"G Farkas","year":"1902","unstructured":"Farkas, G.: \u00dcber die Theorie der Einfachen Ungleichungen. Journal fr die Reine und Angewandte Mathematik 124(124), 1\u201327 (1902)","journal-title":"Journal fr die Reine und Angewandte Mathematik"},{"issue":"3","key":"23_CR3","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 Transactions on Computers 44(3), 471\u2013479 (1995)","journal-title":"IEEE Transactions on Computers"},{"key":"23_CR4","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. Lecture Notes in Computer Science 1295, 309\u2013319 (1997)","journal-title":"Lecture Notes in Computer Science"},{"key":"23_CR5","doi-asserted-by":"crossref","unstructured":"K. Iwama and E. Miyano. 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":"23_CR6","unstructured":"B. Korte and J. Vygen. Combinatorial Optimization. Number 21 in Algorithms and Combinatorics. Springer-Verlag, New York, $$4^{th}$$ edition, 2010"},{"key":"23_CR7","doi-asserted-by":"crossref","unstructured":"S. K. Lahiri and M. Musuvathi. An Efficient Decision Procedure for UTVPI Constraints. In Proceedings of the $$5^{th}$$ International Workshop on the Frontiers of Combining Systems, September 19\u201321, Vienna, Austria, pages 168\u2013183, New York, 2005. Springer","DOI":"10.1007\/11559306_9"},{"issue":"1","key":"23_CR8","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 and Symbolic Computation 19(1), 31\u2013100 (2006)","journal-title":"Higher-Order and Symbolic Computation"},{"key":"23_CR9","doi-asserted-by":"publisher","DOI":"10.1017\/CBO9780511814075","volume-title":"Randomized Algorithms","author":"R Motwani","year":"1995","unstructured":"Motwani, R., Raghavan, P.: Randomized Algorithms. Cambridge University Press, Cambridge, England (1995)"},{"key":"23_CR10","volume-title":"Integer and Combinatorial Optimization","author":"GL Nemhauser","year":"1999","unstructured":"Nemhauser, G.L., Wolsey, L.A.: Integer and Combinatorial Optimization. John Wiley & Sons, New York (1999)"},{"issue":"1","key":"23_CR11","first-page":"387","volume":"236","author":"B James","year":"2018","unstructured":"James, B., Orlin, K.: Subramani, and Piotr Wojciechowski. Randomized algorithms for finding the shortest negative cost cycle in networks. Discrete Applied Mathematics 236(1), 387\u2013394 (2018)","journal-title":"Discrete Applied Mathematics"},{"key":"23_CR12","doi-asserted-by":"crossref","unstructured":"Toniann Pitassi and Alasdair Urquhart. The complexity of the Haj\u00f3s calculus. In 33rd Annual Symposium on Foundations of Computer Science, Pittsburgh, Pennsylvania, USA, 24\u201327 October 1992, pages 187\u2013196, 1992","DOI":"10.1109\/SFCS.1992.267773"},{"key":"23_CR13","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)"},{"key":"23_CR14","unstructured":"SRI International. Yices: An SMT solver. http:\/\/yices.csl.sri.com\/"},{"issue":"2","key":"23_CR15","doi-asserted-by":"publisher","first-page":"316","DOI":"10.1145\/976706.976711","volume":"5","author":"K Subramani","year":"2004","unstructured":"Subramani, K.: Optimal length tree-like resolution refutations for 2sat formulas. ACM Transactions on Computational Logic 5(2), 316\u2013320 (2004)","journal-title":"ACM Transactions on Computational Logic"},{"issue":"2","key":"23_CR16","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. Journal of Automated Reasoning (JAR) 43(2), 121\u2013137 (2009)","journal-title":"Journal of Automated Reasoning (JAR)"},{"issue":"1","key":"23_CR17","doi-asserted-by":"publisher","first-page":"166","DOI":"10.1007\/s00453-016-0131-1","volume":"78","author":"K Subramani","year":"2017","unstructured":"Subramani, K., Piotr, J.: Wojciechowski. A combinatorial certifying algorithm for linear feasibility in UTVPI constraints. Algorithmica 78(1), 166\u2013208 (2017)","journal-title":"Algorithmica"}],"container-title":["Lecture Notes in Computer Science","Frontiers in Algorithmics"],"original-title":[],"language":"en","link":[{"URL":"https:\/\/link.springer.com\/content\/pdf\/10.1007\/978-3-319-78455-7_23","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2025,7,2]],"date-time":"2025-07-02T21:55:23Z","timestamp":1751493323000},"score":1,"resource":{"primary":{"URL":"https:\/\/link.springer.com\/10.1007\/978-3-319-78455-7_23"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2018]]},"ISBN":["9783319784540","9783319784557"],"references-count":17,"URL":"https:\/\/doi.org\/10.1007\/978-3-319-78455-7_23","relation":{},"ISSN":["0302-9743","1611-3349"],"issn-type":[{"type":"print","value":"0302-9743"},{"type":"electronic","value":"1611-3349"}],"subject":[],"published":{"date-parts":[[2018]]},"assertion":[{"value":"21 March 2018","order":1,"name":"first_online","label":"First Online","group":{"name":"ChapterHistory","label":"Chapter History"}},{"value":"FAW","order":1,"name":"conference_acronym","label":"Conference Acronym","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"International Workshop on Frontiers in Algorithmics","order":2,"name":"conference_name","label":"Conference Name","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"Guangzhou","order":3,"name":"conference_city","label":"Conference City","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"China","order":4,"name":"conference_country","label":"Conference Country","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"2018","order":5,"name":"conference_year","label":"Conference Year","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"8 May 2018","order":7,"name":"conference_start_date","label":"Conference Start Date","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"10 May 2018","order":8,"name":"conference_end_date","label":"Conference End Date","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"12","order":9,"name":"conference_number","label":"Conference Number","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"faw2018","order":10,"name":"conference_id","label":"Conference ID","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"http:\/\/itcs.shufe.edu.cn\/faw2018\/","order":11,"name":"conference_url","label":"Conference URL","group":{"name":"ConferenceInfo","label":"Conference Information"}}]}}