{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2026,3,18]],"date-time":"2026-03-18T04:45:24Z","timestamp":1773809124337,"version":"3.50.1"},"reference-count":55,"publisher":"Springer Science and Business Media LLC","issue":"2","license":[{"start":{"date-parts":[[2009,6,27]],"date-time":"2009-06-27T00:00:00Z","timestamp":1246060800000},"content-version":"tdm","delay-in-days":0,"URL":"http:\/\/www.springer.com\/tdm"}],"content-domain":{"domain":[],"crossmark-restriction":false},"short-container-title":["J Autom Reasoning"],"published-print":{"date-parts":[[2009,8]]},"DOI":"10.1007\/s10817-009-9139-4","type":"journal-article","created":{"date-parts":[[2009,6,26]],"date-time":"2009-06-26T10:29:08Z","timestamp":1246012148000},"page":"121-137","source":"Crossref","is-referenced-by-count":29,"title":["Optimal Length Resolution Refutations of Difference Constraint Systems"],"prefix":"10.1007","volume":"43","author":[{"given":"K.","family":"Subramani","sequence":"first","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]}],"member":"297","published-online":{"date-parts":[[2009,6,27]]},"reference":[{"key":"9139_CR1","doi-asserted-by":"crossref","first-page":"391","DOI":"10.1287\/mnsc.34.3.391","volume":"34","author":"J Adams","year":"1988","unstructured":"Adams, J., Balas, E., Zawack, D.: The shifting bottleneck procedure for job shop scheduling. Manage. Sci. 34, 391\u2013401 (1988)","journal-title":"Manage. Sci."},{"issue":"7","key":"9139_CR2","doi-asserted-by":"crossref","first-page":"57","DOI":"10.1016\/0895-7177(93)90068-A","volume":"17","author":"A Aggoun","year":"1993","unstructured":"Aggoun, A., Beldiceanu, N.: Extending chip to solve complex scheduling and placement problems. J. Math. Comput. Model. 17(7), 57\u201373 (1993)","journal-title":"J. Math. Comput. Model."},{"key":"9139_CR3","volume-title":"Network Flows: Theory, Algorithms and Applications","author":"RK Ahuja","year":"1993","unstructured":"Ahuja, R.K., Magnanti, T.L., Orlin, J.B.: Network Flows: Theory, Algorithms and Applications. Prentice-Hall, Englewood Cliffs (1993)"},{"key":"9139_CR4","volume-title":"Mathematical Foundations of Computer Science (MFCS). Lecture Notes in Computer Science","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: Mathematical Foundations of Computer Science (MFCS). Lecture Notes in Computer Science. Springer, New York (1998)"},{"key":"9139_CR5","doi-asserted-by":"crossref","unstructured":"Asarin, E., Bozga, M., Kerbrat, A., Maler, O., Pnueli, A., Rasse, A.: Data structures for verification of timed automata. In: Proceedings of the Hybrid and Real-Time Systems (1997)","DOI":"10.1007\/BFb0014737"},{"key":"9139_CR6","unstructured":"Baptiste, P., Pape, C.L., Nuijten, W.: Constraint-based optimization and approximation for job-shop scheduling. In: AAAI-SIGMAN Workshop on Intelligent Manufacturing Systems (1995)"},{"key":"9139_CR7","first-page":"274","volume-title":"37th Annual Symposium on Foundations of Computer Science","author":"P Beame","year":"1996","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 (1996)"},{"key":"9139_CR8","first-page":"66","volume":"65","author":"P Beame","year":"1998","unstructured":"Beame, P., Pitassi, T.: Propositional proof complexity: past, present, future. Bull. EATCS 65, 66\u201389 (1998)","journal-title":"Bull. EATCS"},{"key":"9139_CR9","doi-asserted-by":"crossref","unstructured":"Bockmayr, A., Eisenbrand, F.: Combining logic and optimization in cutting plane theory. In: FroCos, pp. 1\u201317 (2000)","DOI":"10.1007\/10720084_1"},{"key":"9139_CR10","volume-title":"Asynchronous Circuits","author":"JA Brzowski","year":"1994","unstructured":"Brzowski, J.A., Seger, C.J.: Asynchronous Circuits. Springer, New York (1994)"},{"issue":"1\u20133","key":"9139_CR11","doi-asserted-by":"crossref","first-page":"83","DOI":"10.1016\/S0166-218X(00)00245-6","volume":"107","author":"HK B\u00fcning","year":"2000","unstructured":"B\u00fcning, H.K.: On subclasses of minimal unsatisfiable formulas. Discrete Appl. Math. 107(1\u20133), 83\u201398 (2000)","journal-title":"Discrete Appl. Math."},{"key":"9139_CR12","volume-title":"CSL: 11th Workshop on Computer Science Logic, LNCS","author":"P Buss","year":"1997","unstructured":"Buss, P.: Resolution and the weak pigeonhole principle. In: CSL: 11th Workshop on Computer Science Logic, LNCS. Springer, New York (1997)"},{"key":"9139_CR13","volume-title":"Handbook of Proof Theory","year":"1998","unstructured":"Buss, S.R. (ed.): Handbook of Proof Theory. Elsevier, Amsterdam (1998)"},{"key":"9139_CR14","volume-title":"Algorithms and Theory of Computation Handbook, CRC Press, 1999","author":"V Chandru","year":"1999","unstructured":"Chandru, V., Rao, M.: Linear programming. In: Algorithms and Theory of Computation Handbook, CRC Press, 1999. CRC, Boca Raton (1999)"},{"issue":"4","key":"9139_CR15","doi-asserted-by":"crossref","first-page":"354","DOI":"10.1016\/S0022-0000(73)80029-7","volume":"7","author":"SA Cook","year":"1973","unstructured":"Cook, S.A., Reckhow, R.A.: Time bounded random access machines. J. Comput. Syst. Sci. 7(4), 354\u2013375 (1973)","journal-title":"J. Comput. Syst. Sci."},{"key":"9139_CR16","volume-title":"Introduction to Algorithms","author":"TH Cormen","year":"1992","unstructured":"Cormen, T.H., Leiserson, C.E., Rivest, R.L.: Introduction to Algorithms, 2nd edn. MIT and McGraw-Hill, Boston (1992)","edition":"2"},{"key":"9139_CR17","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":"9139_CR18","doi-asserted-by":"crossref","first-page":"288","DOI":"10.1016\/0097-3165(73)90004-6","volume":"14","author":"GB Dantzig","year":"1973","unstructured":"Dantzig, G.B., Eaves, B.C.: Fourier-Motzkin elimination and its dual. J. Comb. Theory (A) 14, 288\u2013297 (1973)","journal-title":"J. Comb. Theory (A)"},{"issue":"6","key":"9139_CR19","doi-asserted-by":"crossref","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":"9139_CR20","doi-asserted-by":"crossref","first-page":"269","DOI":"10.1007\/BF01386390","volume":"1","author":"EW Dijkstra","year":"1959","unstructured":"Dijkstra, E.W.: A note on two problems in connexion with graphs. Numer. Math. 1, 269\u2013271 (1959)","journal-title":"Numer. Math."},{"key":"9139_CR21","unstructured":"Duterre, B., de\u00a0Moura, L.: The yices smt solver. Tech. rep., SRI International (2006)"},{"key":"9139_CR22","doi-asserted-by":"crossref","unstructured":"Ford, J., Shankar, N.: Formal verification of a combination decision procedure. In: CADE, pp. 347\u2013362 (2002)","DOI":"10.1007\/3-540-45620-1_29"},{"key":"9139_CR23","unstructured":"Fourier, J.B.J.: Reported In: Analyse de travaux de l\u2019Academie Royale des Sciences, pendant l\u2019annee 1824, Partie Mathematique, Histoire de \u2019Academie Royale de Sciences de l\u2019Institue de France 7 (1827) xlvii-lv. (Partial English translation in: D.A. Kohler, Translation of a Report by Fourier on his work on Linear Inequalities. Opsearch 10 (1973) 38\u201342.). Academic, London (1824)"},{"key":"9139_CR24","volume-title":"Computers and Intractability: A Guide to the Theory of NP-Completeness","author":"MR Garey","year":"1979","unstructured":"Garey, M.R., Johnson, D.S.: Computers and Intractability: A Guide to the Theory of NP-Completeness. W. H. Freeman, San Francisco (1979)"},{"issue":"2\u20133","key":"9139_CR25","doi-asserted-by":"crossref","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. Comp. Sci. 39(2\u20133), 297\u2013308 (1985)","journal-title":"Theor. Comp. Sci."},{"key":"9139_CR26","unstructured":"Han, C.C., Lin, K.J.: Job scheduling with temporal distance constraints. Tech. Rep. UIUCDCS-R-89-1560, University of Illinois at Urbana-Champaign, Department of Computer Science (1989)"},{"issue":"6","key":"9139_CR27","doi-asserted-by":"crossref","first-page":"1179","DOI":"10.1137\/S0097539793251876","volume":"23","author":"DS Hochbaum","year":"1994","unstructured":"Hochbaum, D.S., Naor, J.S.: Simple and fast algorithms for linear and integer programs with two variables per inequality. SIAM J. Comput. 23(6), 1179\u20131192 (1994)","journal-title":"SIAM J. Comput."},{"key":"9139_CR28","first-page":"117","volume-title":"Proceedings Second International Conference on Algebraic and Logic Programming. Lecture Notes in Computer Science, vol. 463","author":"T Huynh","year":"1990","unstructured":"Huynh, T., Lassez, C., Lassez, J.L.: Fourier algorithm revisited. In: Kirchner, H., Wechler, W. (eds.) Proceedings Second International Conference on Algebraic and Logic Programming. Lecture Notes in Computer Science, vol. 463, pp. 117\u2013131. Springer, Nancy (1990)"},{"key":"9139_CR29","doi-asserted-by":"crossref","first-page":"29","DOI":"10.1109\/SCT.1995.514725","volume-title":"Proceedings of the 10th Annual Conference on Structure in Complexity Theory (SCTC \u201995)","author":"K Iwama","year":"1995","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, Los Alamitos (1995)"},{"issue":"1","key":"9139_CR30","doi-asserted-by":"crossref","first-page":"93","DOI":"10.1016\/0304-3975(78)90006-3","volume":"6","author":"DS Johnson","year":"1978","unstructured":"Johnson, D.S., Preparata, F.P.: The densest hemisphere problem. Theoretical Comput. Sci. 6(1), 93\u2013107 (1978)","journal-title":"Theoretical Comput. Sci."},{"key":"9139_CR31","doi-asserted-by":"crossref","first-page":"85","DOI":"10.1007\/978-1-4684-2001-2_9","volume-title":"Complexity of Computer Computations","author":"RM Karp","year":"1972","unstructured":"Karp, R.M.: Reducibility among combinatorial problems. In: Miller, R.E., Thatcher, J.W. (eds.) Complexity of Computer Computations, pp. 85\u2013103. Plenum, New York (1972)"},{"key":"9139_CR32","unstructured":"Kratsch, D., McConnell, R.M., Mehlhorn, K., Spinrad, J.: Certifying algorithms for recognizing interval graphs and permutation graphs. In: SODA, pp. 158\u2013167 (2003)"},{"issue":"1","key":"9139_CR33","doi-asserted-by":"crossref","first-page":"196","DOI":"10.1137\/0214016","volume":"14","author":"JC Lagarias","year":"1985","unstructured":"Lagarias, J.C.: The computational complexity of simultaneous Diophantine approximation problems. SIAM J. Comput. 14(1), 196\u2013209 (1985)","journal-title":"SIAM J. Comput."},{"key":"9139_CR34","doi-asserted-by":"crossref","unstructured":"Lahiri, S.K., Musuvathi, M.: An efficient decision procedure for UTVPI constraints. In: FroCos, pp. 168\u2013183 (2005)","DOI":"10.1007\/11559306_9"},{"key":"9139_CR35","doi-asserted-by":"crossref","first-page":"373","DOI":"10.1007\/BF00245296","volume":"9","author":"JL Lassez","year":"1992","unstructured":"Lassez, J.L., Maher, M.: On fourier\u2019s algorithm for linear constraints. J. Autom. Reason 9, 373\u2013379 (1992)","journal-title":"J. Autom. Reason"},{"issue":"3","key":"9139_CR36","doi-asserted-by":"crossref","first-page":"90","DOI":"10.1145\/71021.71026","volume":"23","author":"ST Levi","year":"1989","unstructured":"Levi, S.T., Tripathi, S.K., Carson, S.D., Agrawala, A.K.: The Maruti hard real-time operating system. ACM Special Interest Group on Operating Systems. Oper. Syst. Rev. 23(3), 90\u2013106 (1989)","journal-title":"Oper. Syst. Rev."},{"key":"9139_CR37","unstructured":"Lynce, I., Silva, J.P.M.: On computing minimum unsatisfiable cores. In: SAT (2004)"},{"key":"9139_CR38","doi-asserted-by":"crossref","unstructured":"de\u00a0Moura, L.M., Owre, S., Ruess, H., Rushby, J.M., Shankar, N.: The ICS decision procedures for embedded deduction. In: IJCAR, pp. 218\u2013222 (2004)","DOI":"10.1007\/978-3-540-25984-8_14"},{"key":"9139_CR39","volume-title":"Integer and Combinatorial Optimization","author":"GL Nemhauser","year":"1999","unstructured":"Nemhauser, G.L., Wolsey, L.A.: Integer and Combinatorial Optimization. Wiley, New York (1999)"},{"key":"9139_CR40","volume-title":"Scheduling: Theory, Algorithms, and Systems","author":"M Pinedo","year":"1995","unstructured":"Pinedo, M.: Scheduling: Theory, Algorithms, and Systems. Prentice-Hall, Englewood Cliffs (1995)"},{"issue":"3","key":"9139_CR41","doi-asserted-by":"crossref","first-page":"981","DOI":"10.2307\/2275583","volume":"62","author":"P Pudl\u00e1k","year":"1997","unstructured":"Pudl\u00e1k, P.: Lower bounds for resolution and cutting plane proofs and monotone computations. J. Symb. Log. 62(3), 981\u2013998 (1997)","journal-title":"J. Symb. Log."},{"key":"9139_CR42","volume-title":"Handbook of Automated Reasoning","year":"2001","unstructured":"Robinson, A., Voronkov, A. (eds.): Handbook of Automated Reasoning. Elsevier, Amsterdam (2001)"},{"issue":"1","key":"9139_CR43","doi-asserted-by":"crossref","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":"9139_CR44","doi-asserted-by":"crossref","unstructured":"Rushby, J.M.: Tutorial: automated formal methods with pvs, sal, and yices. In: SEFM, p. 262 (2006)","DOI":"10.1109\/SEFM.2006.37"},{"key":"9139_CR45","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)"},{"key":"9139_CR46","doi-asserted-by":"crossref","unstructured":"Seshia, S.A., Bryant, R.E.: Deciding quantifier-free presburger formulas using parameterized solution bounds. In: LICS, pp. 100\u2013109 (2004)","DOI":"10.1109\/LICS.2004.1319604"},{"key":"9139_CR47","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"},{"issue":"1,2","key":"9139_CR48","doi-asserted-by":"crossref","first-page":"67","DOI":"10.3233\/SAT190030","volume":"3","author":"SA Seshia","year":"2007","unstructured":"Seshia, S.A., Subramani, K., Bryant, R.E.: On solving boolean combinations of UTVPI constraints. Journal on Satisfiability, Boolean Modeling and Computation 3(1,2), 67\u201390 (2007)","journal-title":"Journal on Satisfiability, Boolean Modeling and Computation"},{"issue":"3","key":"9139_CR49","doi-asserted-by":"crossref","first-page":"281","DOI":"10.1002\/malq.200310099","volume":"50","author":"K Subramani","year":"2004","unstructured":"Subramani, K.: On deciding the non-emptiness of 2SAT polytopes with respect to first order queries. Math. Log. Q. 50(3):281\u2013292 (2004)","journal-title":"Math. Log. Q."},{"issue":"2","key":"9139_CR50","doi-asserted-by":"crossref","first-page":"113","DOI":"10.1007\/s10951-005-6367-2","volume":"8","author":"K Subramani","year":"2005","unstructured":"Subramani, K.: An analysis of totally clairvoyant scheduling. J. Sched. 8(2), 113\u2013133 (2005)","journal-title":"J. Sched."},{"issue":"3","key":"9139_CR51","doi-asserted-by":"crossref","first-page":"259","DOI":"10.1093\/comjnl\/bxh082","volume":"48","author":"K Subramani","year":"2005","unstructured":"Subramani, K.: A comprehensive framework for specifying clairvoyance, constraints and periodicty in real-time scheduling. Comput. J. 48(3), 259\u2013272 (2005)","journal-title":"Comput. J."},{"key":"9139_CR52","doi-asserted-by":"crossref","unstructured":"Tseitin, G.: On the complexity of derivation in propositional calculus. In: Studies in Constructive Mathematics and Mathematical Logic, pp. 115\u2013125 (1970)","DOI":"10.1007\/978-1-4899-5327-8_25"},{"issue":"4","key":"9139_CR53","doi-asserted-by":"crossref","first-page":"425","DOI":"10.2178\/bsl\/1203350879","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."},{"issue":"6","key":"9139_CR54","doi-asserted-by":"crossref","first-page":"826","DOI":"10.1145\/268999.269003","volume":"44","author":"H Wasserman","year":"1997","unstructured":"Wasserman, H., Blum, M.: Software reliability via run-time result-checking. J ACM 44(6), 826\u2013849 (1997)","journal-title":"J ACM"},{"key":"9139_CR55","doi-asserted-by":"crossref","first-page":"118","DOI":"10.1016\/0097-3165(76)90055-8","volume":"21","author":"H Williams","year":"1976","unstructured":"Williams, H.: Fourier-motzkin elimination extension to integer programming. J. Comb. Theory 21, 118\u2013123 (1976)","journal-title":"J. Comb. Theory"}],"container-title":["Journal of Automated Reasoning"],"original-title":[],"language":"en","link":[{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/s10817-009-9139-4.pdf","content-type":"application\/pdf","content-version":"vor","intended-application":"text-mining"},{"URL":"http:\/\/link.springer.com\/article\/10.1007\/s10817-009-9139-4\/fulltext.html","content-type":"text\/html","content-version":"vor","intended-application":"text-mining"},{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/s10817-009-9139-4","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2025,2,10]],"date-time":"2025-02-10T11:19:36Z","timestamp":1739186376000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/s10817-009-9139-4"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2009,6,27]]},"references-count":55,"journal-issue":{"issue":"2","published-print":{"date-parts":[[2009,8]]}},"alternative-id":["9139"],"URL":"https:\/\/doi.org\/10.1007\/s10817-009-9139-4","relation":{},"ISSN":["0168-7433","1573-0670"],"issn-type":[{"value":"0168-7433","type":"print"},{"value":"1573-0670","type":"electronic"}],"subject":[],"published":{"date-parts":[[2009,6,27]]}}}