{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2025,8,24]],"date-time":"2025-08-24T01:40:16Z","timestamp":1755999616416},"publisher-location":"Berlin, Heidelberg","reference-count":20,"publisher":"Springer Berlin Heidelberg","isbn-type":[{"type":"print","value":"9783540278290"},{"type":"electronic","value":"9783540315803"}],"content-domain":{"domain":[],"crossmark-restriction":false},"short-container-title":[],"published-print":{"date-parts":[[2005]]},"DOI":"10.1007\/11527695_2","type":"book-chapter","created":{"date-parts":[[2010,12,20]],"date-time":"2010-12-20T17:06:47Z","timestamp":1292864807000},"page":"16-29","source":"Crossref","is-referenced-by-count":23,"title":["A SAT-Based Decision Procedure for the Boolean Combination of Difference Constraints"],"prefix":"10.1007","author":[{"given":"Alessandro","family":"Armando","sequence":"first","affiliation":[]},{"given":"Claudio","family":"Castellini","sequence":"additional","affiliation":[]},{"given":"Enrico","family":"Giunchiglia","sequence":"additional","affiliation":[]},{"given":"Marco","family":"Maratea","sequence":"additional","affiliation":[]}],"member":"297","reference":[{"key":"2_CR1","series-title":"Lecture Notes in Artificial Intelligence","doi-asserted-by":"crossref","first-page":"195","DOI":"10.1007\/3-540-45620-1_17","volume-title":"Automated Deduction - CADE-18","author":"G. Audemard","year":"2002","unstructured":"Audemard, G., Bertoli, P.G., Cimatti, A., Kornilowicz, A., Sebastiani, R.: A SAT based approach for solving formulas over boolean and linear mathematical propositions. In: Voronkov, A. (ed.) CADE 2002. LNCS (LNAI), vol.\u00a02392, pp. 195\u2013210. Springer, Heidelberg (2002)"},{"key":"2_CR2","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"97","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, pp. 97\u2013108. Springer, Heidelberg (2000)"},{"key":"2_CR3","unstructured":"Armando, A., Castellini, C., Giunchiglia, E., Idini, M., Maratea, M.: TSAT++: an open platform for satisfiability modulo theories. In: Proceedings of PDPAR 2004 - Pragmatics of Decision Procedures in Automated Reasoning, Cork, Ireland. Elsevier Science Publishers, Amsterdam (2004) (to appear)"},{"key":"2_CR4","unstructured":"Bayardo Jr., R.J., Miranker, D.P.: A complexity analysis of space-bounded learning algorithms for the constraint satisfaction problem. In: Proc. AAAI, pp. 298\u2013304 (1996)"},{"key":"2_CR5","first-page":"203","volume-title":"Proceedings of the 14th National Conference on Artificial Intelligence and 9th Innovative Applications of Artificial Intelligence Conference (AAAI 1997\/IAAI 1997)","author":"R.J. Bayardo Jr.","year":"1997","unstructured":"Bayardo Jr., R.J., Schrag, R.C.: Using CSP look-back techniques to solve real-world SAT instances. In: Proceedings of the 14th National Conference on Artificial Intelligence and 9th Innovative Applications of Artificial Intelligence Conference (AAAI 1997\/IAAI 1997), July 27\u201331, pp. 203\u2013208. AAAI Press, Menlo Park (1997)"},{"key":"2_CR6","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"452","DOI":"10.1007\/978-3-540-24605-3_34","volume-title":"Theory and Applications of Satisfiability Testing","author":"D. Berre Le","year":"2004","unstructured":"Le Berre, D., Simon, L.: The essentials of the SAT 2003 competition. In: Giunchiglia, E., Tacchella, A. (eds.) SAT 2003. LNCS, vol.\u00a02919, pp. 452\u2013467. Springer, Heidelberg (2004)"},{"key":"2_CR7","volume-title":"Introduction to Algorithms","author":"T.H. Cormen","year":"1998","unstructured":"Cormen, T.H., Leiserson, C.E., Rivest, R.R.: Introduction to Algorithms. MIT Press, Cambridge (1998)"},{"key":"2_CR8","unstructured":"CPLEX user\u2019s guide. Manual, CPLEX Optimization, Inc., Incline Village, NV, USA (1993)"},{"issue":"1-3","key":"2_CR9","doi-asserted-by":"publisher","first-page":"61","DOI":"10.1016\/0004-3702(91)90006-6","volume":"49","author":"R. Dechter","year":"1991","unstructured":"Dechter, R., Meiri, I., Pearl, J.: Temporal constraint networks. Artificial Intelligence\u00a049(1-3), 61\u201395 (1991)","journal-title":"Artificial Intelligence"},{"key":"2_CR10","first-page":"1460","volume-title":"Proceedings of the 15th International Joint Conference on Artificial Intelligence (IJCAI 1997)","author":"A. Gerevini","year":"1997","unstructured":"Gerevini, A., Cristani, M.: On finding a solution in temporal constraint satisfaction problems. In: Proceedings of the 15th International Joint Conference on Artificial Intelligence (IJCAI 1997), August\u00a023\u201329, pp. 1460\u20131465. Morgan Kaufmann Publishers, San Francisco (1997)"},{"key":"2_CR11","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","DOI":"10.1007\/b95238","volume-title":"Theory and Applications of Satisfiability Testing","author":"E. Giunchiglia","year":"2004","unstructured":"Giunchiglia, E., Maratea, M., Tacchella, A.: Look-ahead vs. look-back techniques in a modern SAT solver. In: Giunchiglia, E., Tacchella, A. (eds.) SAT 2003. LNCS, vol.\u00a02919. Springer, Heidelberg (2004)"},{"key":"2_CR12","first-page":"366","volume-title":"Proceedings of the 15th International Joint Conference on Artificial Intelligence (IJCAI 1997)","author":"C.M. Li","year":"1997","unstructured":"Li, C.M., Anbulagan: Heuristics based on unit propagation for satisfiability problems. In: Proceedings of the 15th International Joint Conference on Artificial Intelligence (IJCAI 1997), August 23\u201329, pp. 366\u2013371. Morgan Kaufmann Publishers, San Francisco (1997)"},{"key":"2_CR13","doi-asserted-by":"crossref","unstructured":"Moskewicz, M.W., Madigan, C.F., Zhao, Y., Zhang, L., Malik, S.: Chaff: Engineering an Efficient SAT Solver. In: Proceedings of the 38th Design Automation Conference, DAC 2001 (June 2001)","DOI":"10.1145\/378239.379017"},{"key":"2_CR14","unstructured":"Oddi, A., Cesta, A.: Incremental forward checking for the disjunctive temporal problem. In: Proceedings of the 14th European Conference on Artificial Intelligence (ECAI 2000), Berlin, pp. 108\u2013112 (2000)"},{"issue":"3","key":"2_CR15","doi-asserted-by":"publisher","first-page":"268","DOI":"10.1111\/j.1467-8640.1993.tb00310.x","volume":"9","author":"P. Prosser","year":"1993","unstructured":"Prosser, P.: Hybrid algorithms for the constraint satisfaction problem. Computational Intelligence\u00a09(3), 268\u2013299 (1993)","journal-title":"Computational Intelligence"},{"key":"2_CR16","unstructured":"Stergiou, K., Koubarakis, M.: Backtracking algorithms for disjunctions of temporal constraints. In: Proc.\u00a0AAAI (1998)"},{"key":"2_CR17","doi-asserted-by":"crossref","unstructured":"Silva, J.P.M., Sakallah, K.A.: GRASP: A search algorithm for propositional satisfiability. IEEETC: IEEE Transactions on Computers\u00a048 (1999)","DOI":"10.1109\/12.769433"},{"key":"2_CR18","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, pp. 209\u2013222. Springer, Heidelberg (2002)"},{"key":"2_CR19","doi-asserted-by":"crossref","unstructured":"Tsamardinos, I., Pollack, M.: Efficient solution techniques for disjunctive temporal reasoning problems. Artificial Intelligence (2003) (to appear)","DOI":"10.1016\/S0004-3702(03)00113-9"},{"key":"2_CR20","unstructured":"Wolfman, S., Weld, D.: The LPSAT-engine & its application to resource planning. In: Proc.\u00a0IJCAI 1999 (1999)"}],"container-title":["Lecture Notes in Computer Science","Theory and Applications of Satisfiability Testing"],"original-title":[],"link":[{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/11527695_2.pdf","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2020,11,17]],"date-time":"2020-11-17T20:07:17Z","timestamp":1605643637000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/11527695_2"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2005]]},"ISBN":["9783540278290","9783540315803"],"references-count":20,"URL":"https:\/\/doi.org\/10.1007\/11527695_2","relation":{},"ISSN":["0302-9743","1611-3349"],"issn-type":[{"type":"print","value":"0302-9743"},{"type":"electronic","value":"1611-3349"}],"subject":[],"published":{"date-parts":[[2005]]}}}