{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2024,9,6]],"date-time":"2024-09-06T14:59:04Z","timestamp":1725634744928},"reference-count":21,"publisher":"Springer Science and Business Media LLC","issue":"2","license":[{"start":{"date-parts":[[2017,9,27]],"date-time":"2017-09-27T00:00:00Z","timestamp":1506470400000},"content-version":"tdm","delay-in-days":0,"URL":"http:\/\/www.springer.com\/tdm"},{"start":{"date-parts":[[2017,9,27]],"date-time":"2017-09-27T00:00:00Z","timestamp":1506470400000},"content-version":"vor","delay-in-days":0,"URL":"http:\/\/www.springer.com\/tdm"}],"funder":[{"name":"National Science Foundation","award":["CCF-$1305054"],"award-info":[{"award-number":["CCF-$1305054"]}]}],"content-domain":{"domain":["link.springer.com"],"crossmark-restriction":false},"short-container-title":["J Comb Optim"],"published-print":{"date-parts":[[2018,2]]},"DOI":"10.1007\/s10878-017-0176-3","type":"journal-article","created":{"date-parts":[[2017,9,27]],"date-time":"2017-09-27T07:34:01Z","timestamp":1506497641000},"page":"389-408","update-policy":"http:\/\/dx.doi.org\/10.1007\/springer_crossmark_policy","source":"Crossref","is-referenced-by-count":7,"title":["A certifying algorithm for lattice point feasibility in a system of UTVPI constraints"],"prefix":"10.1007","volume":"35","author":[{"given":"K.","family":"Subramani","sequence":"first","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Piotr","family":"Wojciechowski","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]}],"member":"297","published-online":{"date-parts":[[2017,9,27]]},"reference":[{"key":"176_CR1","doi-asserted-by":"crossref","unstructured":"Bagnara R, Hill P\u00a0M, Zaffanella E (2008) An improved tight closure algorithm for integer octagonal constraints. In: VMCAI, pp 8\u201321","DOI":"10.1007\/978-3-540-78163-9_6"},{"key":"176_CR2","first-page":"129","volume":"73","author":"BV Cherkassky","year":"1996","unstructured":"Cherkassky BV, Goldberg AV, Radzik T (1996) Shortest paths algorithms: theory and experimental evaluation. Math Program 73:129\u2013174","journal-title":"Math Program"},{"key":"176_CR3","volume-title":"Introduction to algorithms","author":"TH Cormen","year":"2001","unstructured":"Cormen TH, Leiserson CE, Rivest RL, Stein C (2001) Introduction to algorithms. MIT Press, Cambridge"},{"key":"176_CR4","doi-asserted-by":"crossref","unstructured":"Cousot P, Cousot R (1977) Abstract interpretation: a unified lattice model for static analysis of programs by construction or approximation of fixpoints. In: Proceedings of the\u00a04th ACM symposium on the principles of programming languages (POPL), ACM Press, pp 238\u2013252","DOI":"10.1145\/512950.512973"},{"key":"176_CR5","doi-asserted-by":"crossref","unstructured":"Dantzig GB, Eaves BC (1973) Fourier\u2013Motzkin elimination and its dual. J Comb Theory (A) 14:288\u2013297","DOI":"10.1016\/0097-3165(73)90004-6"},{"key":"176_CR6","doi-asserted-by":"crossref","unstructured":"Fouilhe A, Monniaux D, P\u00e9rin M (2013). Efficient generation of correctness certificates for the abstract domain of polyhedra. In: Static analysis: 20th international symposium, pp 345\u2013365","DOI":"10.1007\/978-3-642-38856-9_19"},{"issue":"3","key":"176_CR7","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 (1995) Parametric dispatching of hard real-time tasks. IEEE Trans Comput 44(3):471\u2013479","journal-title":"IEEE Trans Comput"},{"issue":"2\u20133","key":"176_CR8","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 (1985) The intractability of resolution. Theor Comput Sci 39(2\u20133):297\u2013308","journal-title":"Theor Comput Sci"},{"key":"176_CR9","unstructured":"Harvey W, Stuckey PJ (1997). A unit two variable per inequality integer constraint solver for constraint logic programming. In: Proceedings of the 20th Australasian computer science conference, pp 102\u2013111"},{"issue":"6","key":"176_CR10","doi-asserted-by":"publisher","first-page":"1179","DOI":"10.1137\/S0097539793251876","volume":"23","author":"DS Hochbaum","year":"1994","unstructured":"Hochbaum DS, Naor J (1994) Simple and fast algorithms for linear and integer programs with two variables per inequality. SIAM J Comput 23(6):1179\u20131192","journal-title":"SIAM J Comput"},{"key":"176_CR11","doi-asserted-by":"crossref","unstructured":"Jaffar J, Maher MJ, Stuckey PJ, Yap HC (1994) Beyond finite domains. In: Proceedings of the second international workshop on principles and practice of constraint programming (PPCP), lecture notes in computer science, vol 874, pp 86\u201394","DOI":"10.1007\/3-540-58601-6_92"},{"key":"176_CR12","unstructured":"Lahiri SK, Musuvathi M (2005) An Efficient decision procedure for UTVPI constraints. In: Proceedings of the\u00a0$$5{\\rm th}$$\u00a0international workshop on the frontiers of combining systems (FroCos), lecture notes in computer science, vol 3717, pp 168\u2013183"},{"key":"176_CR13","volume-title":"The LEDA platform of combinatorial and geometric computing","author":"K Mehlhorn","year":"1999","unstructured":"Mehlhorn K, N\u00e4her S (1999) The LEDA platform of combinatorial and geometric computing. Cambridge University Press, Cambridge"},{"issue":"1","key":"176_CR14","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 (2006) The octagon abstract domain. High Order Symb Comput 19(1):31\u2013100","journal-title":"High Order Symb Comput"},{"key":"176_CR15","doi-asserted-by":"crossref","unstructured":"Nieuwenhuis R, Oliveras A (2005) DPLL(T) with exhaustive theory propagation and its application to difference logic. In: Proceedings of the $$17{\\rm th}$$ international conference on computer aided verification (CAV), lecture notes in computer science, vol 3576, pp 321\u2013334","DOI":"10.1007\/11513988_33"},{"key":"176_CR16","unstructured":"Nieuwenhuis R, Oliveras A, Tinelli C (2004) Abstract DPLL and abstract DPLL modulo theories. In: Proceedings of the\u00a0 $$11{\\rm th}$$\u00a0international conference on logic for programming, artificial intelligence and reasoning (LPAR), lecture notes in computer science, vol 3452, pp 36\u201350"},{"key":"176_CR17","unstructured":"Revesz PZ (2009) Tightened transitive closure of integer addition constraints. In: Proceedings of the\u00a0$$8{\\rm th}$$\u00a0symposium on abstraction, reformulation and approximation (SARA), AAAI"},{"issue":"4","key":"176_CR18","doi-asserted-by":"publisher","first-page":"514","DOI":"10.1287\/ijoc.1090.0369","volume":"22","author":"A Schutt","year":"2010","unstructured":"Schutt A, Stuckey PJ (2010) Incremental satisfiability and implication for UTVPI constraints. INFORMS J Comput 22(4):514\u2013527","journal-title":"INFORMS J Comput"},{"key":"176_CR19","unstructured":"Sitzmann I, Stuckey PJ (2000) O-trees: a constraint-based index structure. In: Australasian database conference, pp 127\u2013134"},{"issue":"3","key":"176_CR20","doi-asserted-by":"publisher","first-page":"281","DOI":"10.1002\/malq.200310099","volume":"50","author":"K Subramani","year":"2004","unstructured":"Subramani K (2004) On deciding the non-emptiness of 2SAT polytopes with respect to first order queries. Math Logic Q 50(3):281\u2013292","journal-title":"Math Logic Q"},{"key":"176_CR21","unstructured":"Subramani K, Wojciechowski P (2016) A combinatorial certifying algorithm for linear feasibility in UTVPI constraints. Algorithmica, First online: 28 April 2016"}],"container-title":["Journal of Combinatorial Optimization"],"original-title":[],"language":"en","link":[{"URL":"http:\/\/link.springer.com\/article\/10.1007\/s10878-017-0176-3\/fulltext.html","content-type":"text\/html","content-version":"vor","intended-application":"text-mining"},{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/s10878-017-0176-3.pdf","content-type":"application\/pdf","content-version":"vor","intended-application":"text-mining"},{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/s10878-017-0176-3.pdf","content-type":"application\/pdf","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2020,5,17]],"date-time":"2020-05-17T12:48:37Z","timestamp":1589719717000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/s10878-017-0176-3"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2017,9,27]]},"references-count":21,"journal-issue":{"issue":"2","published-print":{"date-parts":[[2018,2]]}},"alternative-id":["176"],"URL":"https:\/\/doi.org\/10.1007\/s10878-017-0176-3","relation":{},"ISSN":["1382-6905","1573-2886"],"issn-type":[{"value":"1382-6905","type":"print"},{"value":"1573-2886","type":"electronic"}],"subject":[],"published":{"date-parts":[[2017,9,27]]},"assertion":[{"value":"27 September 2017","order":1,"name":"first_online","label":"First Online","group":{"name":"ArticleHistory","label":"Article History"}}]}}