{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2025,9,28]],"date-time":"2025-09-28T12:46:10Z","timestamp":1759063570047},"reference-count":26,"publisher":"Association for Computing Machinery (ACM)","issue":"2","license":[{"start":{"date-parts":[[2013,3,1]],"date-time":"2013-03-01T00:00:00Z","timestamp":1362096000000},"content-version":"tdm","delay-in-days":0,"URL":"http:\/\/www.springer.com\/tdm"}],"content-domain":{"domain":[],"crossmark-restriction":false},"short-container-title":["Form. Asp. Comput."],"published-print":{"date-parts":[[2013,3]]},"abstract":"<jats:title>Abstract<\/jats:title>\n          <jats:p>\n            This paper is concerned with the design and analysis of improved algorithms for determining the optimal length resolution refutation (OLRR) of a system of difference constraints over an integral domain. The problem of finding short explanations for unsatisfiable Difference Constraint Systems (DCS) finds applications in a number of design domains including program verification, proof theory, real-time scheduling, and operations research. These explanations have also been called \u201ccertificates\u201d and \u201crefutations\u201d in the literature. This problem was first studied in Subramani (J Autom Reason 43(2):121\u2013137,\n            <jats:xref ref-type=\"bibr\">2009<\/jats:xref>\n            ), wherein the first polynomial time algorithm was proposed. In this paper, we propose two new strongly polynomial algorithms which improve on the existing time bound. Our first algorithm, which we call the edge progression approach, runs in\n            <jats:italic>O<\/jats:italic>\n            (\n            <jats:italic>n<\/jats:italic>\n            <jats:sup>2<\/jats:sup>\n            \u00b7\n            <jats:italic>k<\/jats:italic>\n            \u00a0+\u00a0\n            <jats:italic>m<\/jats:italic>\n            \u00b7\n            <jats:italic>n<\/jats:italic>\n            \u00b7\n            <jats:italic>k<\/jats:italic>\n            ) time, while our second algorithm, which we call the edge relaxation approach, runs in\n            <jats:italic>O<\/jats:italic>\n            (\n            <jats:italic>m<\/jats:italic>\n            \u00b7\n            <jats:italic>n<\/jats:italic>\n            \u00b7\n            <jats:italic>k<\/jats:italic>\n            ) time, where\n            <jats:italic>m<\/jats:italic>\n            is the number of constraints in the DCS,\n            <jats:italic>n<\/jats:italic>\n            is the number of program variables, and\n            <jats:italic>k<\/jats:italic>\n            denotes the length of the shortest refutation. We conducted an extensive empirical analysis of the three OLRR algorithms discussed in this paper. Our experiments indicate that in the case of sparse graphs, the new algorithms discussed in this paper are superior to the algorithm in Subramani (J Autom Reason 43(2):121\u2013137,\n            <jats:xref ref-type=\"bibr\">2009<\/jats:xref>\n            ). Likewise, in the case of dense graphs, the approach in Subramani (J Autom Reason 43(2):121\u2013137,\n            <jats:xref ref-type=\"bibr\">2009<\/jats:xref>\n            ) is superior to the algorithms described in this paper. One surprising observation is the superiority of the edge relaxation algorithm over the edge progression algorithm in all cases, although both algorithms have the same asymptotic time complexity.\n          <\/jats:p>","DOI":"10.1007\/s00165-011-0186-3","type":"journal-article","created":{"date-parts":[[2011,7,6]],"date-time":"2011-07-06T19:43:47Z","timestamp":1309981427000},"page":"319-341","source":"Crossref","is-referenced-by-count":11,"title":["Improved algorithms for optimal length resolution refutation in difference constraint systems"],"prefix":"10.1145","volume":"25","author":[{"given":"K.","family":"Subramani","sequence":"first","affiliation":[{"name":"LDCSEE, West Virginia University, Morgantown, WV, USA"}],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Matthew","family":"Williamson","sequence":"additional","affiliation":[{"name":"LDCSEE, West Virginia University, Morgantown, WV, USA"}],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Xiaofeng","family":"Gu","sequence":"additional","affiliation":[{"name":"Department of Mathematics, West Virginia University, Morgantown, WV, USA"}],"role":[{"role":"author","vocabulary":"crossref"}]}],"member":"320","reference":[{"key":"e_1_2_1_2_1_2","doi-asserted-by":"crossref","unstructured":"Alekhnovich M Buss S Moran S Pitassi T (1998) Minimum propositional proof length is NP-hard to linearly approximate. In: Mathematical foundations of computer science (MFCS) Lecture Notes in Computer Science Springer Berlin","DOI":"10.1007\/BFb0055766"},{"key":"e_1_2_1_2_2_2","unstructured":"P. Beame T. Pitassi (1996) Simplified and improved resolution lower bounds. In: 37th Annual symposium on foundations of computer science IEEE pp 274\u2013282. Burlington Vermont 14\u201316 October 1996"},{"key":"e_1_2_1_2_3_2","doi-asserted-by":"crossref","unstructured":"Buss SR Pitassi T (1997) Resolution and the weak pigeonhole principle. In: CSL: 11th Workshop on computer science logic. LNCS Springer Berlin","DOI":"10.1007\/BFb0028012"},{"key":"e_1_2_1_2_4_2","volume-title":"Introduction to algorithms","author":"Cormen TH","year":"2001"},{"key":"e_1_2_1_2_5_2","unstructured":"Demetrescu C Goldberg AV Johnson D (2005) 9th DIMACS implementation challenge\u2014shortest paths. http:\/\/www.dis.uniroma1.it\/~challenge9\/"},{"key":"e_1_2_1_2_6_2","doi-asserted-by":"crossref","unstructured":"de Moura LM Owre S Ruess H Rushby JM Shankar N (2004) The ICS decision procedures for embedded deduction. In: IJCAR pp 218\u2013222","DOI":"10.1007\/978-3-540-25984-8_14"},{"key":"e_1_2_1_2_7_2","first-page":"38","article-title":"Translation of a report by fourier on his work on linear inequalities","volume":"10","author":"Fourier JBJ","year":"1827","journal-title":"Opsearch"},{"key":"e_1_2_1_2_8_2","doi-asserted-by":"crossref","unstructured":"Ford J Shankar N (2002) Formal verification of a combination decision procedure. In: CADE pp 347\u2013362","DOI":"10.1007\/3-540-45620-1_29"},{"key":"e_1_2_1_2_9_2","doi-asserted-by":"publisher","DOI":"10.1137\/S0097539792231179"},{"key":"e_1_2_1_2_10_2","doi-asserted-by":"publisher","DOI":"10.1016\/0304-3975(85)90144-6"},{"key":"e_1_2_1_2_11_2","unstructured":"Han CC Lin KJ (1989) Job scheduling with temporal distance constraints. Technical report UIUCDCS-R-89-1560 Department of Computer Science University of Illinois at Urbana-Champaign"},{"key":"e_1_2_1_2_12_2","doi-asserted-by":"publisher","DOI":"10.1137\/S0097539793251876"},{"key":"e_1_2_1_2_13_2","volume-title":"Integer and combinatorial optimization","author":"Nemhauser GL","year":"1999"},{"key":"e_1_2_1_2_14_2","volume-title":"Scheduling: theory, algorithms, and systems","author":"Pinedo M","year":"1995"},{"key":"e_1_2_1_2_15_2","doi-asserted-by":"publisher","DOI":"10.1145\/321250.321253"},{"key":"e_1_2_1_2_16_2","doi-asserted-by":"crossref","unstructured":"Seshia SA Bryant RE (2004) Deciding quantifier-free presburger formulas using parameterized solution bounds. In: LICS pp 100\u2013109","DOI":"10.21236\/ADA461078"},{"key":"e_1_2_1_2_17_2","volume-title":"Theory of linear and integer programming","author":"Schrijver A","year":"1987"},{"key":"e_1_2_1_2_18_2","unstructured":"Stankovic JA Ramamritham K (1988) Hard real-time systems. IEEE Computer Society Press Los Alamitos"},{"key":"e_1_2_1_2_19_2","doi-asserted-by":"publisher","DOI":"10.1002\/malq.200310099"},{"key":"e_1_2_1_2_20_2","doi-asserted-by":"publisher","DOI":"10.1145\/976706.976711"},{"key":"e_1_2_1_2_21_2","doi-asserted-by":"publisher","DOI":"10.1007\/s10951-005-6367-2"},{"key":"e_1_2_1_2_22_2","doi-asserted-by":"publisher","DOI":"10.1093\/comjnl\/bxh082"},{"key":"e_1_2_1_2_23_2","doi-asserted-by":"publisher","DOI":"10.1007\/s10817-009-9139-4"},{"key":"e_1_2_1_2_24_2","doi-asserted-by":"crossref","unstructured":"Tseitin G (1970) On the complexity of derivation in propositional calculus. In: Studies in constructive mathematics and mathematical logic pp 115\u2013125","DOI":"10.1007\/978-1-4899-5327-8_25"},{"key":"e_1_2_1_2_25_2","doi-asserted-by":"publisher","DOI":"10.2178\/bsl\/1203350879"},{"key":"e_1_2_1_2_26_2","doi-asserted-by":"publisher","DOI":"10.1016\/0097-3165(76)90055-8"}],"container-title":["Formal Aspects of Computing"],"original-title":[],"language":"en","link":[{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/s00165-011-0186-3.pdf","content-type":"application\/pdf","content-version":"vor","intended-application":"text-mining"},{"URL":"http:\/\/link.springer.com\/article\/10.1007\/s00165-011-0186-3\/fulltext.html","content-type":"text\/html","content-version":"vor","intended-application":"text-mining"},{"URL":"https:\/\/dl.acm.org\/doi\/pdf\/10.1007\/s00165-011-0186-3","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2022,1,6]],"date-time":"2022-01-06T15:54:17Z","timestamp":1641484457000},"score":1,"resource":{"primary":{"URL":"https:\/\/dl.acm.org\/doi\/10.1007\/s00165-011-0186-3"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2013,3]]},"references-count":26,"journal-issue":{"issue":"2","published-print":{"date-parts":[[2013,3]]}},"alternative-id":["10.1007\/s00165-011-0186-3"],"URL":"https:\/\/doi.org\/10.1007\/s00165-011-0186-3","relation":{},"ISSN":["0934-5043","1433-299X"],"issn-type":[{"value":"0934-5043","type":"print"},{"value":"1433-299X","type":"electronic"}],"subject":[],"published":{"date-parts":[[2013,3]]}}}