{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2026,7,28]],"date-time":"2026-07-28T01:29:59Z","timestamp":1785202199673,"version":"3.55.0"},"publisher-location":"Berlin, Heidelberg","reference-count":20,"publisher":"Springer Berlin Heidelberg","isbn-type":[{"value":"9783540372066","type":"print"},{"value":"9783540372073","type":"electronic"}],"content-domain":{"domain":[],"crossmark-restriction":false},"short-container-title":[],"published-print":{"date-parts":[[2006]]},"DOI":"10.1007\/11814948_19","type":"book-chapter","created":{"date-parts":[[2006,7,18]],"date-time":"2006-07-18T10:12:38Z","timestamp":1153217558000},"page":"170-183","source":"Crossref","is-referenced-by-count":44,"title":["Fast and Flexible Difference Constraint Propagation for DPLL(T)"],"prefix":"10.1007","author":[{"given":"Scott","family":"Cotton","sequence":"first","affiliation":[],"role":[{"vocabulary":"crossref","role":"author"}]},{"given":"Oded","family":"Maler","sequence":"additional","affiliation":[],"role":[{"vocabulary":"crossref","role":"author"}]}],"member":"297","reference":[{"key":"19_CR1","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"crossref","first-page":"349","DOI":"10.1007\/3-540-61680-2_67","volume-title":"Algorithms - ESA \u201996","author":"B.V. Cherkassky","year":"1996","unstructured":"Cherkassky, B.V., Goldberg, A.V.: Negative-cycle detection algorithms. In: D\u00edaz, J. (ed.) ESA 1996. LNCS, vol.\u00a01136, pp. 349\u2013363. Springer, Heidelberg (1996)"},{"key":"19_CR2","volume-title":"Introduction to algorithms","author":"T.H. Cormen","year":"1990","unstructured":"Cormen, T.H., Leiserson, C.E., Rivest, R.L., Stein, C.: Introduction to algorithms. MIT Press, Cambridge (1990)"},{"key":"19_CR3","unstructured":"Cotton, S.: Satisfiability checking with difference constraints. Master\u2019s thesis, Max Planck Institute (2005)"},{"key":"19_CR4","unstructured":"Cotton, S., Maler, O.: Satisfiability modulo theory chains with DPLL(T). In Verimag Technical Report (2006), http:\/\/www-verimag.imag.fr\/TR\/TR-2006-4.pdf"},{"issue":"7","key":"19_CR5","doi-asserted-by":"publisher","first-page":"394","DOI":"10.1145\/368273.368557","volume":"5","author":"M. Davis","year":"1962","unstructured":"Davis, M., Logemann, G., Loveland, D.: A machine program for theorem proving. Communications of the ACM\u00a05(7), 394\u2013397 (1962)","journal-title":"Communications of the ACM"},{"issue":"1","key":"19_CR6","doi-asserted-by":"publisher","first-page":"201","DOI":"10.1145\/321033.321034","volume":"7","author":"M. Davis","year":"1960","unstructured":"Davis, M., Putnam, H.: A computing procedure for quantification theory. Journal of the ACM\u00a07(1), 201\u2013215 (1960)","journal-title":"Journal of the ACM"},{"key":"19_CR7","doi-asserted-by":"publisher","first-page":"269","DOI":"10.1007\/BF01386390","volume":"1","author":"E.W. Dijkstra","year":"1959","unstructured":"Dijkstra, E.W.: A note on two problems in connexion with graphs. Numer. Math.\u00a01, 269\u2013271 (1959)","journal-title":"Numer. Math."},{"key":"19_CR8","unstructured":"E\u00e8n, N., Sorensson, N.: Minisat \u2013 a sat solver with conflict-clause minimization. In: SAT 2005 (2005)"},{"key":"19_CR9","doi-asserted-by":"crossref","unstructured":"Frigioni, D., Marchetti-Spaccamela, A., Nanni, U.: Fully dynamic shortest paths and negative cycles detection on digraphs with arbitrary arc weights. In: European Symposium on Algorithms, pp. 320\u2013331 (1998)","DOI":"10.1007\/3-540-68530-8_27"},{"key":"19_CR10","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"175","DOI":"10.1007\/978-3-540-27813-9_14","volume-title":"Computer Aided Verification","author":"H. Ganzinger","year":"2004","unstructured":"Ganzinger, H., Hagen, G., Nieuwenhuis, R., Oliveras, A., Tinelli, C.: DPLL(T): Fast decision procedures. In: Alur, R., Peled, D.A. (eds.) CAV 2004. LNCS, vol.\u00a03114, pp. 175\u2013188. Springer, Heidelberg (2004)"},{"key":"19_CR11","doi-asserted-by":"crossref","unstructured":"Goldberg, A.V.: Shortests path algorithms: Engineering aspects. In: Proceedings of the Internation Symposium of Algorithms and Computation (2001)","DOI":"10.1007\/3-540-45678-3_43"},{"key":"19_CR12","unstructured":"Goldberg, E., Novikov, Y.: Berkmin: A fast and robust SAT solver (2002)"},{"key":"19_CR13","doi-asserted-by":"crossref","unstructured":"Johnson, D.B.: Efficient algorithms for shortest paths in sparse networks. J. Assoc. Comput. Mach.\u00a024(1) (1977)","DOI":"10.1145\/321992.321993"},{"key":"19_CR14","series-title":"Lecture Notes in Computer Science","first-page":"220","volume-title":"Computer Aided Verification","author":"J.P. Marquez-Silva","year":"1996","unstructured":"Marquez-Silva, J.P., Sakallah, K.A.: Grasp \u2013 a new search algorithm for satisfiability. In: Alur, R., Henzinger, T.A. (eds.) CAV 1996. LNCS, vol.\u00a01102, pp. 220\u2013227. Springer, Heidelberg (1996)"},{"key":"19_CR15","doi-asserted-by":"crossref","unstructured":"Moskewicz, M.W., Madigan, C.F., Zhao, Y., Zhang, L., Malik, S.: Chaff: Engineering an Efficient SAT Solver. In: DAC 2001 (2001)","DOI":"10.1145\/378239.379017"},{"key":"19_CR16","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., Maler, O., Jain, N.: Verification of Timed Automata via Satisfiability Checking. In: Damm, W., Olderog, E.-R. (eds.) FTRTFT 2002. LNCS, vol.\u00a02469, pp. 225\u2013243. Springer, Heidelberg (2002)"},{"key":"19_CR17","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"321","DOI":"10.1007\/11513988_33","volume-title":"Computer Aided Verification","author":"R. Nieuwenhuis","year":"2005","unstructured":"Nieuwenhuis, R., Oliveras, A.: DPLL(T) with Exhaustive Theory Propagation and its Application to Difference Logic. In: Etessami, K., Rajamani, S.K. (eds.) CAV 2005. LNCS, vol.\u00a03576, pp. 321\u2013334. Springer, Heidelberg (2005)"},{"key":"19_CR18","series-title":"Lecture Notes in Artificial Intelligence","doi-asserted-by":"publisher","first-page":"36","DOI":"10.1007\/978-3-540-32275-7_3","volume-title":"Logic for Programming, Artificial Intelligence, and Reasoning","author":"R. Nieuwenhuis","year":"2005","unstructured":"Nieuwenhuis, R., Oliveras, A., Tinelli, C.: Abstract DPLL and abstract DPLL modulo theories. In: Baader, F., Voronkov, A. (eds.) LPAR 2004. LNCS (LNAI), vol.\u00a03452, pp. 36\u201350. Springer, Heidelberg (2005)"},{"key":"19_CR19","unstructured":"Ranise, S., Tinelli, C.: The SMT-LIB format: An initial proposal. In: PDPAR (July 2003)"},{"key":"19_CR20","unstructured":"Tarjan, R.E.: Shortest paths. AT&T Technical Reports. AT&T Bell Laboratories (1981)"}],"container-title":["Lecture Notes in Computer Science","Theory and Applications of Satisfiability Testing - SAT 2006"],"original-title":[],"link":[{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/11814948_19.pdf","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2021,4,27]],"date-time":"2021-04-27T07:27:55Z","timestamp":1619508475000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/11814948_19"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2006]]},"ISBN":["9783540372066","9783540372073"],"references-count":20,"URL":"https:\/\/doi.org\/10.1007\/11814948_19","relation":{},"ISSN":["0302-9743","1611-3349"],"issn-type":[{"value":"0302-9743","type":"print"},{"value":"1611-3349","type":"electronic"}],"subject":[],"published":{"date-parts":[[2006]]}}}