{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2024,10,24]],"date-time":"2024-10-24T01:10:28Z","timestamp":1729732228841,"version":"3.28.0"},"reference-count":38,"publisher":"Springer Science and Business Media LLC","issue":"4","license":[{"start":{"date-parts":[[2023,7,12]],"date-time":"2023-07-12T00:00:00Z","timestamp":1689120000000},"content-version":"tdm","delay-in-days":0,"URL":"https:\/\/www.springernature.com\/gp\/researchers\/text-and-data-mining"},{"start":{"date-parts":[[2023,7,12]],"date-time":"2023-07-12T00:00:00Z","timestamp":1689120000000},"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":["Theory Comput Syst"],"published-print":{"date-parts":[[2023,8]]},"DOI":"10.1007\/s00224-023-10134-y","type":"journal-article","created":{"date-parts":[[2023,7,12]],"date-time":"2023-07-12T10:02:01Z","timestamp":1689156121000},"page":"877-899","update-policy":"http:\/\/dx.doi.org\/10.1007\/springer_crossmark_policy","source":"Crossref","is-referenced-by-count":0,"title":["Unit Read-once Refutations for Systems of Difference Constraints"],"prefix":"10.1007","volume":"67","author":[{"given":"K.","family":"Subramani","sequence":"first","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"P.","family":"Wojciechowski","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]}],"member":"297","published-online":{"date-parts":[[2023,7,12]]},"reference":[{"issue":"4","key":"10134_CR1","doi-asserted-by":"publisher","first-page":"844","DOI":"10.1145\/210332.210337","volume":"42","author":"N Alon","year":"1995","unstructured":"Alon, N., Yuster, R., Zwick, U.: Color-coding. J. ACM 42(4), 844\u2013856 (1995)","journal-title":"J. ACM"},{"key":"10134_CR2","doi-asserted-by":"crossref","unstructured":"Ausiello, G., Crescenzi, P., Gambosi, G., Kann, V., Marchetti-Spaccamela, A., Protasi, M.: Complexity and Approximation: Combinatorial Optimization and Their Approximability Properties. 1st edition, Springer (1999)","DOI":"10.1007\/978-3-642-58412-1_1"},{"key":"10134_CR3","doi-asserted-by":"crossref","unstructured":"Beame, P., Pitassi, T.: Simplified and improved resolution lower bounds. In 37th Annual Symposium on Foundations of Computer Science, pp. 274\u2013282. IEEE, Burlington, Vermont 14\u201316 (1996)","DOI":"10.1109\/SFCS.1996.548486"},{"issue":"1","key":"10134_CR4","doi-asserted-by":"publisher","first-page":"77","DOI":"10.1016\/0890-5401(92)90056-L","volume":"96","author":"P Berman","year":"1992","unstructured":"Berman, P., Schnitger, G.: On the complexity of approximating the independent set problem. Inf. Comput. 96(1), 77\u201394 (1992)","journal-title":"Inf. Comput."},{"key":"10134_CR5","doi-asserted-by":"crossref","unstructured":"Buss, Pitassi: Resolution and the weak pigeonhole principle. In CSL: 11th Workshop on Computer Science Logic. LNCS, Springer-Verlag (1997)","DOI":"10.1007\/BFb0028012"},{"key":"10134_CR6","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 Optim. 10, 85\u2013101 (2013)","journal-title":"Discrete Optim."},{"key":"10134_CR7","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, MA (2009)","edition":"3"},{"key":"10134_CR8","doi-asserted-by":"crossref","unstructured":"Cotton, S., Asarin, E., Maler, O., Niebert, P.: Some progress in satisfiability checking for difference logic. In FORMATS\/FTRTFT, pp. 263\u2013276. (2004)","DOI":"10.1007\/978-3-540-30206-3_19"},{"key":"10134_CR9","doi-asserted-by":"crossref","unstructured":"Cotton, S., Maler, O.: Fast and flexible difference constraint propagation for dpll(t). In SAT, pp. 170\u2013183. Springer (2006)","DOI":"10.1007\/11814948_19"},{"key":"10134_CR10","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, pp. 238\u2013252. In POPL (1977)","DOI":"10.1145\/512950.512973"},{"key":"10134_CR11","doi-asserted-by":"crossref","unstructured":"Cox, I.J., Rao, S.B., Zhong, Y.: Ratio regions: A technique for image segmentation. In Proceedings of the International Conference on Pattern Recognition, pp. 557\u2013564. IEEE (1996)","DOI":"10.1109\/ICPR.1996.546886"},{"key":"10134_CR12","doi-asserted-by":"crossref","unstructured":"Cygan, M., Fomin, F.V., Kowalik, L., Lokshtanov, D., Marx, D., Pilipczuk, M., Pilipczuk, M., Saurabh, S.: Parameterized Algorithms. Springer (2015)","DOI":"10.1007\/978-3-319-21275-3"},{"issue":"6","key":"10134_CR13","doi-asserted-by":"publisher","first-page":"968","DOI":"10.1145\/1039488.1039492","volume":"51","author":"C Demtrescu","year":"2004","unstructured":"Demtrescu, C., Italiano, G.F.: A new approach to dynamic all pairs shortest paths. J. ACM 51(6), 968\u2013992 (2004)","journal-title":"J. ACM"},{"key":"10134_CR14","unstructured":"Diestel, R.: Graph Theory. Springer-Verlag, 2nd ed. (2000)"},{"issue":"124","key":"10134_CR15","first-page":"1","volume":"124","author":"G Farkas","year":"1902","unstructured":"Farkas, G.: \u00dcber die Theorie der Einfachen Ungleichungen. J. f\u00fcr Reine Angew. Math. 124(124), 1\u201327 (1902)","journal-title":"J. f\u00fcr Reine Angew. Math."},{"key":"10134_CR16","unstructured":"Fleury, P.H.: Deux probl\u00e9mes de g\u00e9om\u00e9trie de situation. J. Math. \u00c9lem. 2nd ser. (in French) 2,257\u2013261 (1883)"},{"issue":"3","key":"10134_CR17","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 Transac. Comput. 44(3), 471\u2013479 (1995)","journal-title":"IEEE Transac. Comput."},{"issue":"2\u20133","key":"10134_CR18","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."},{"key":"10134_CR19","unstructured":"Han, C.C., Lin, K.J.: Job scheduling with temporal distance constraints. Technical Report UIUCDCS-R-89-1560, University of Illinois at Urbana-Champaign, Department of Computer Science (1989)"},{"key":"10134_CR20","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), pp. 29\u201336. IEEE Computer Society Press, Los Alamitos, CA, USA (1995)","DOI":"10.1109\/SCT.1995.514725"},{"issue":"3","key":"10134_CR21","first-page":"317","volume":"1","author":"V Kann","year":"1994","unstructured":"Kann, V.: Polynomially bounded minimization problems that are hard to approximate. Nordic J. Comput. 1(3), 317\u2013331 (1994)","journal-title":"Nordic J. Comput."},{"key":"10134_CR22","doi-asserted-by":"crossref","unstructured":"B\u00fcning, H.K., Wojciechowski, P.J., Chandrasekaran, R., Subramani, K.: Restricted cutting plane proofs in horn constraint systems. In Andreas Herzig and Andrei Popescu, (eds.) Frontiers of Combining Systems - 12th International Symposium, FroCoS 2019, September 4-6, 2019, Proceedings, volume 11715 of Lecture Notes in Computer Science, pp. 149\u2013164. Springer, London, UK (2019)","DOI":"10.1007\/978-3-030-29007-8_9"},{"key":"10134_CR23","unstructured":"B\u00fcning, H.K., Wojciechowski, P.J., 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, pp. 43:1\u201343:14. Bombay, India (2019)"},{"key":"10134_CR24","unstructured":"B\u00fcning, H.K., Wojciechowski, P.J., 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, pp. 43:1\u201343:14. Bombay, India (2019)"},{"key":"10134_CR25","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)"},{"key":"10134_CR26","doi-asserted-by":"crossref","unstructured":"Nieuwenhuis, R., Oliveras, A.: Dpll(t) with exhaustive theory propagation and its application to difference logic. In CAV, pp. 321\u2013334 (2005)","DOI":"10.1007\/11513988_33"},{"key":"10134_CR27","unstructured":"Orponen, P., Mannila, H.: On approximation preserving reductions: Complete problems and robust measures. Technical report, Department of Computer Science, University of Helsinki (1987)"},{"key":"10134_CR28","doi-asserted-by":"crossref","unstructured":"Pelleau, M.: 5 - an abstract solver: Absolute. In Marie Pelleau, (ed.), Abstract Domains in Constraint Programming, pp. 111\u2013137. Elsevier, (2015)","DOI":"10.1016\/B978-1-78548-010-2.50005-2"},{"issue":"1","key":"10134_CR29","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":"10134_CR30","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":"10134_CR31","doi-asserted-by":"crossref","unstructured":"Seshia, S.A., Lahiri, S.K., Bryant, R.E.: A hybrid sat-based decision procedure for separation logic with uninterpreted functions. In DAC, pp. 425\u2013430 (2003)","DOI":"10.1145\/775832.775945"},{"key":"10134_CR32","unstructured":"SRI International. Yices: An SMT solver. http:\/\/yices.csl.sri.com\/"},{"issue":"2","key":"10134_CR33","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":"10134_CR34","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. Form. Asp. Comput. 25(2), 319\u2013341 (2013)","journal-title":"Form. Asp. Comput."},{"issue":"7","key":"10134_CR35","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 readonce certification of linear infeasibility in UTVPI constraints. Algorithmica 81(7), 2765\u20132794 (2019)","journal-title":"Algorithmica"},{"issue":"1","key":"10134_CR36","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":"10134_CR37","doi-asserted-by":"crossref","unstructured":"Subramani, K., Wojciechowski, P.,J.: Analyzing unit read-once refutations in difference constraint systems. In Wolfgang Faber, Gerhard Friedrich, Martin Gebser, and Michael Morak, (eds.), Logics in Artificial Intelligence - 17th European Conference, JELIA 2021, Virtual Event, May 17-20, 2021, Proceedings, volume 12678 of Lecture Notes in Computer Science, pp. 147\u2013161. Springer (2021)","DOI":"10.1007\/978-3-030-75775-5_11"},{"issue":"4","key":"10134_CR38","doi-asserted-by":"publisher","first-page":"425","DOI":"10.2307\/421131","volume":"1","author":"A Urquhart","year":"1995","unstructured":"Urquhart, A.: The complexity of propositional proofs. Bull. Symb. Log. 1(4), 425\u2013467 (1995)","journal-title":"Bull. Symb. Log."}],"container-title":["Theory of Computing Systems"],"original-title":[],"language":"en","link":[{"URL":"https:\/\/link.springer.com\/content\/pdf\/10.1007\/s00224-023-10134-y.pdf","content-type":"application\/pdf","content-version":"vor","intended-application":"text-mining"},{"URL":"https:\/\/link.springer.com\/article\/10.1007\/s00224-023-10134-y\/fulltext.html","content-type":"text\/html","content-version":"vor","intended-application":"text-mining"},{"URL":"https:\/\/link.springer.com\/content\/pdf\/10.1007\/s00224-023-10134-y.pdf","content-type":"application\/pdf","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2024,10,24]],"date-time":"2024-10-24T00:38:15Z","timestamp":1729730295000},"score":1,"resource":{"primary":{"URL":"https:\/\/link.springer.com\/10.1007\/s00224-023-10134-y"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2023,7,12]]},"references-count":38,"journal-issue":{"issue":"4","published-print":{"date-parts":[[2023,8]]}},"alternative-id":["10134"],"URL":"https:\/\/doi.org\/10.1007\/s00224-023-10134-y","relation":{},"ISSN":["1432-4350","1433-0490"],"issn-type":[{"type":"print","value":"1432-4350"},{"type":"electronic","value":"1433-0490"}],"subject":[],"published":{"date-parts":[[2023,7,12]]},"assertion":[{"value":"2 June 2023","order":1,"name":"accepted","label":"Accepted","group":{"name":"ArticleHistory","label":"Article History"}},{"value":"12 July 2023","order":2,"name":"first_online","label":"First Online","group":{"name":"ArticleHistory","label":"Article History"}},{"order":1,"name":"Ethics","group":{"name":"EthicsHeading","label":"Declarations"}},{"value":"We declare that we have no conflicts of interest.","order":2,"name":"Ethics","group":{"name":"EthicsHeading","label":"Conflicts of interest"}}]}}