{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2026,6,5]],"date-time":"2026-06-05T04:11:08Z","timestamp":1780632668971,"version":"3.54.1"},"publisher-location":"Berlin, Heidelberg","reference-count":31,"publisher":"Springer Berlin Heidelberg","isbn-type":[{"value":"9783540231677","type":"print"},{"value":"9783540302063","type":"electronic"}],"license":[{"start":{"date-parts":[[2004,1,1]],"date-time":"2004-01-01T00:00:00Z","timestamp":1072915200000},"content-version":"tdm","delay-in-days":0,"URL":"http:\/\/www.springer.com\/tdm"}],"content-domain":{"domain":[],"crossmark-restriction":false},"short-container-title":[],"published-print":{"date-parts":[[2004]]},"DOI":"10.1007\/978-3-540-30206-3_19","type":"book-chapter","created":{"date-parts":[[2011,1,18]],"date-time":"2011-01-18T10:19:15Z","timestamp":1295345955000},"page":"263-276","source":"Crossref","is-referenced-by-count":24,"title":["Some Progress in Satisfiability Checking for Difference Logic"],"prefix":"10.1007","author":[{"given":"Scott","family":"Cotton","sequence":"first","affiliation":[],"role":[{"vocabulary":"crossref","role":"author"}]},{"given":"Eugene","family":"Asarin","sequence":"additional","affiliation":[],"role":[{"vocabulary":"crossref","role":"author"}]},{"given":"Oded","family":"Maler","sequence":"additional","affiliation":[],"role":[{"vocabulary":"crossref","role":"author"}]},{"given":"Peter","family":"Niebert","sequence":"additional","affiliation":[],"role":[{"vocabulary":"crossref","role":"author"}]}],"member":"297","reference":[{"key":"19_CR1","doi-asserted-by":"publisher","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. Management Science\u00a034, 391\u2013401 (1988)","journal-title":"Management Science"},{"key":"19_CR2","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","DOI":"10.1007\/10720246_8","volume-title":"Recent Advances in AI Planning","author":"A. Armando","year":"2000","unstructured":"Armando, A., Castellini, C., Giunchiglia, E.: SAT-based Procedures for Temporal Reasoning. In: Biundo, S., Fox, M. (eds.) ECP 1999. LNCS, vol.\u00a01809, Springer, Heidelberg (2000)"},{"key":"19_CR3","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"346","DOI":"10.1007\/BFb0014737","volume-title":"Hybrid and Real-Time Systems","author":"E. Asarin","year":"1997","unstructured":"Asarin, E., Bozga, M., Kerbrat, A., Maler, O., Pnueli, A., Rasse, A.: Data Structures for the Verification of Timed Automata. In: Maler, O. (ed.) HART 1997. LNCS, vol.\u00a01201, pp. 346\u2013360. Springer, Heidelberg (1997)"},{"key":"19_CR4","series-title":"Lecture Notes in Artificial Intelligence","first-page":"193","volume-title":"Automated Deduction - CADE-18","author":"G. Audemard","year":"2002","unstructured":"Audemard, G., Bertoli, P., Cimatti, A., Kornilowics, A., Sebastiani, R.: A SATBased Approach for Solving Formulas over Boolean and Linear Mathematical Propositions. In: Voronkov, A. (ed.) CADE 2002. LNCS (LNAI), vol.\u00a02392, pp. 193\u2013208. Springer, Heidelberg (2002)"},{"key":"19_CR5","doi-asserted-by":"crossref","unstructured":"Audemard, G., Cimatti, A., Kornilowics, A., Sebastiani, R.: Bounded Model Checking for Timed Systems, Technical report ITC-0201-05, IRST, Trento (2002)","DOI":"10.1007\/3-540-36135-9_16"},{"key":"19_CR6","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"236","DOI":"10.1007\/3-540-45657-0_18","volume-title":"Computer Aided Verification","author":"C.W. Barrett","year":"2002","unstructured":"Barrett, C.W., Dill, D.L., Stump, A.: Checking Satisfiability of First-Order Formulas by Incremental Translation to SAT. In: Brinksma, E., Larsen, K.G. (eds.) CAV 2002. LNCS, vol.\u00a02404, pp. 236\u2013249. Springer, Heidelberg (2002)"},{"key":"19_CR7","series-title":"Lecture Notes in Computer Science","volume-title":"Formal Modeling and Analysis of Timed Systems","author":"R. Ben Salah","year":"2004","unstructured":"Ben Salah, R., Bozga, M., Maler, O.: On Timing Analysis of Combinational Circuits. In: Larsen, K.G., Niebert, P. (eds.) FORMATS 2003. LNCS, vol.\u00a02791, Springer, Heidelberg (2004)"},{"key":"19_CR8","volume-title":"Asynchronous Circuits","author":"J.A. Brzozowski","year":"1994","unstructured":"Brzozowski, J.A., Seger, C.-J.H.: Asynchronous Circuits. Springer, Heidelberg (1994)"},{"key":"19_CR9","unstructured":"Cormen, T., Leiserson, C., Rivest, R., Stein, C.: Introduction to Algorithms. MIT Press, McGraw-Hill (2001)"},{"key":"19_CR10","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","DOI":"10.1007\/3-540-45739-9_16","volume-title":"Formal Techniques in Real-Time and Fault-Tolerant Systems","author":"M. Fr\u00e4nzle","year":"2002","unstructured":"Fr\u00e4nzle, M.: Take It NP-Easy: Bounded Model Construction for Duration Calculus. In: Damm, W., Olderog, E.-R. (eds.) FTRTFT 2002. LNCS, vol.\u00a02469, Springer, Heidelberg (2002)"},{"key":"19_CR11","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"246","DOI":"10.1007\/3-540-44585-4_22","volume-title":"Computer Aided Verification","author":"J.-C. Filli\u00e2tre","year":"2001","unstructured":"Filli\u00e2tre, J.-C., Owre, S., Rue\u00df, H., Shankar, N.: ICS: Integrated Canonizer and Solver. In: Berry, G., Comon, H., Finkel, A. (eds.) CAV 2001. LNCS, vol.\u00a02102, pp. 246\u2013250. Springer, Heidelberg (2001)"},{"key":"19_CR12","doi-asserted-by":"crossref","unstructured":"Goldberg, E., Novikov, Y.: BerkMin, a Fast and Robust SAT-solver. In: Proc. DATE 2002, pp. 142\u2013149 (2002)","DOI":"10.1109\/DATE.2002.998262"},{"key":"19_CR13","doi-asserted-by":"crossref","unstructured":"Goldberg, A.V., Radzik, T.: A Heuristic Improvement of the Bellman-Ford Algorithm. Applied Mathematics Letters 6 (1993)","DOI":"10.1016\/0893-9659(93)90022-F"},{"key":"19_CR14","doi-asserted-by":"crossref","DOI":"10.1002\/9781118033036","volume-title":"Logic-Based Methods for Optimization: Combining Optimization and Constraint Satisfaction","author":"J. Hooker","year":"2000","unstructured":"Hooker, J.: Logic-Based Methods for Optimization: Combining Optimization and Constraint Satisfaction. Wiley, Chichester (2000)"},{"key":"19_CR15","doi-asserted-by":"publisher","first-page":"503","DOI":"10.1016\/0743-1066(94)90033-7","volume":"19\/20","author":"J. Jaffar","year":"1994","unstructured":"Jaffar, J., Maher, M.J.: Constraint Logic Programming: A Survey. Journal of Logic Programming\u00a019\/20, 503\u2013581 (1994)","journal-title":"Journal of Logic Programming"},{"key":"19_CR16","doi-asserted-by":"publisher","first-page":"390","DOI":"10.1016\/S0377-2217(98)00113-1","volume":"113","author":"A.S. Jain","year":"1999","unstructured":"Jain, A.S., Meeran, S.: Deterministic Job-Shop Scheduling: Past, Present and Future. European Journal of Operational Research\u00a0113, 390\u2013434 (1999)","journal-title":"European Journal of Operational Research"},{"key":"19_CR17","unstructured":"Mahfoudh, M.: On Satisfaiblity Checking for Difference Logic, PhD Thesis, Univerist \u00e9 Joseph Fourier, Grenoble (2003)"},{"key":"19_CR18","unstructured":"Mahfoudh, M., Niebert, P., Asarin, E., Maler, O.: A Satisfiability Checker for Difference Logic. In: Proc. SAT 2002 (2002)"},{"key":"19_CR19","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"crossref","first-page":"189","DOI":"10.1007\/3-540-60385-9_12","volume-title":"Correct Hardware Design and Verification Methods","author":"O. Maler","year":"1995","unstructured":"Maler, O., Pnueli, A.: Timing Analysis of Asynchronous Circuits using Timed Automata. In: Camurati, P.E., Eveking, H. (eds.) CHARME 1995. LNCS, vol.\u00a0987, pp. 189\u2013205. Springer, Heidelberg (1995)"},{"key":"19_CR20","doi-asserted-by":"publisher","first-page":"506","DOI":"10.1109\/12.769433","volume":"48","author":"J.P. Marques-Silva","year":"1999","unstructured":"Marques-Silva, J.P., Sakallah, K.A.: GRASP: A Search Algorithm for Propositional Satisfiability. IEEE Transactions on Computers\u00a048, 506\u2013521 (1999)","journal-title":"IEEE Transactions on Computers"},{"key":"19_CR21","doi-asserted-by":"crossref","unstructured":"Moskewicz, M., Madigan, C., Zhao, Y., Zhang, L., Malik, S.: Chaff: Engineering an Efficient SAT Solver. In: Proc. DAC 2001 (2001)","DOI":"10.1145\/378239.379017"},{"key":"19_CR22","series-title":"Lecture Notes in Artificial Intelligence","first-page":"437","volume-title":"Automated Deduction - CADE-18","author":"L. Moura de","year":"2002","unstructured":"de Moura, L., Rue\u00df, H., Sorea, M.: Lazy Theorem Proving for Bounded Model Checking over Infinite Domains. In: Voronkov, A. (ed.) CADE 2002. LNCS (LNAI), vol.\u00a02392, pp. 437\u2013453. Springer, Heidelberg (2002)"},{"key":"19_CR23","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"225","DOI":"10.1007\/3-540-45739-9_15","volume-title":"Formal Techniques in Real-Time and Fault-Tolerant Systems","author":"P. Niebert","year":"2002","unstructured":"Niebert, P., Mahfoudh, M., Asarin, E., Bozga, M., Jain, N., Maler, O.: Verification of Timed Automata via Satisfiability Checking. In: Damm, W., Olderog, E.-R. (eds.) FTRTFT 2002. LNCS, vol.\u00a02469, pp. 225\u2013244. Springer, Heidelberg (2002)"},{"key":"19_CR24","unstructured":"Sorea, M.: Bounded Model Checking for Timed Automata. In: Proc. MTCS 2002 (2002)"},{"key":"19_CR25","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"209","DOI":"10.1007\/3-540-45657-0_16","volume-title":"Computer Aided Verification","author":"O. Strichman","year":"2002","unstructured":"Strichman, O., Seshia, S.A., Bryant, R.E.: Deciding Separation Formulas with SAT. In: Brinksma, E., Larsen, K.G. (eds.) CAV 2002. LNCS, vol.\u00a02404, p. 209. Springer, Heidelberg (2002)"},{"key":"19_CR26","doi-asserted-by":"publisher","first-page":"146","DOI":"10.1137\/0201010","volume":"1","author":"R. Tarjan","year":"1972","unstructured":"Tarjan, R.: Depth-first Search and Linear Graph Algorithms. SIAM J. Comput.\u00a01, 146\u2013160 (1972)","journal-title":"SIAM J. Comput."},{"key":"19_CR27","doi-asserted-by":"crossref","unstructured":"Tseitin, G.: On the Complexity of Derivation in Propositional Calculus, Consultants Bureau, New York. Studies in Constructive Mathematics and Mathematical Logic, vol.\u00a02, pp. 115\u2013125 (1970)","DOI":"10.1007\/978-1-4899-5327-8_25"},{"key":"19_CR28","doi-asserted-by":"crossref","unstructured":"Wilson, J.M.: Compact normal forms in propositional logic and integer programming formulations. Computers and Operation Research, 309\u2013314 (1990)","DOI":"10.1016\/0305-0548(90)90007-T"},{"key":"19_CR29","first-page":"223","volume":"55","author":"B. Wozna","year":"2003","unstructured":"Wozna, B., Zbrzezny, A., Penczek, W.: Checking Reachability Properties for Timed Automata via SAT. Fundamenta Informaticae\u00a055, 223\u2013241 (2003)","journal-title":"Fundamenta Informaticae"},{"key":"19_CR30","volume-title":"Advances in Logic Programming and Automated Reasoning","author":"G. Zhang","year":"1995","unstructured":"Zhang, G.: The Davis-Putnam Resolution Procedure. In: Advances in Logic Programming and Automated Reasoning, vol.\u00a02, Ablex Publishing Corporation, Greenwich (1995)"},{"key":"19_CR31","unstructured":"Zhang, H., Stickel, M.: An Efficient Algorithm for Unit Propogation. In: Proceedings of the Fourth International Symposium on Artificial Intelligence and Mathematics (1996)"}],"container-title":["Lecture Notes in Computer Science","Formal Techniques, Modelling and Analysis of Timed and Fault-Tolerant Systems"],"original-title":[],"language":"en","link":[{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/978-3-540-30206-3_19","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2025,3,1]],"date-time":"2025-03-01T22:09:12Z","timestamp":1740866952000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/978-3-540-30206-3_19"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2004]]},"ISBN":["9783540231677","9783540302063"],"references-count":31,"URL":"https:\/\/doi.org\/10.1007\/978-3-540-30206-3_19","relation":{},"ISSN":["0302-9743","1611-3349"],"issn-type":[{"value":"0302-9743","type":"print"},{"value":"1611-3349","type":"electronic"}],"subject":[],"published":{"date-parts":[[2004]]}}}