{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2026,9,26]],"date-time":"2026-09-26T16:19:00Z","timestamp":1790439540163,"version":"4.1.0"},"publisher-location":"Berlin, Heidelberg","reference-count":22,"publisher":"Springer Berlin Heidelberg","isbn-type":[{"value":"9783540462675","type":"print"},{"value":"9783540462682","type":"electronic"}],"content-domain":{"domain":[],"crossmark-restriction":false},"short-container-title":[],"published-print":{"date-parts":[[2006]]},"DOI":"10.1007\/11889205_31","type":"book-chapter","created":{"date-parts":[[2006,9,28]],"date-time":"2006-09-28T12:07:42Z","timestamp":1159445262000},"page":"421-436","source":"Crossref","is-referenced-by-count":8,"title":["Towards an Efficient SAT Encoding for Temporal Reasoning"],"prefix":"10.1007","author":[{"given":"Duc Nghia","family":"Pham","sequence":"first","affiliation":[],"role":[{"vocabulary":"crossref","role":"author"}]},{"given":"John","family":"Thornton","sequence":"additional","affiliation":[],"role":[{"vocabulary":"crossref","role":"author"}]},{"given":"Abdul","family":"Sattar","sequence":"additional","affiliation":[],"role":[{"vocabulary":"crossref","role":"author"}]}],"member":"297","reference":[{"key":"31_CR1","doi-asserted-by":"publisher","first-page":"832","DOI":"10.1145\/182.358434","volume":"26","author":"J.F. Allen","year":"1983","unstructured":"Allen, J.F.: Maintaining knowledge about temporal intervals. Communications of the ACM\u00a026, 832\u2013843 (1983)","journal-title":"Communications of the ACM"},{"key":"31_CR2","unstructured":"Cheeseman, P., Kanefsky, B., Taylor, W.M.: Where the really hard problems are. In: IJCAI 1991, pp. 331\u2013337 (1991)"},{"issue":"11","key":"31_CR3","doi-asserted-by":"publisher","first-page":"958","DOI":"10.1145\/359642.359654","volume":"21","author":"E.C. Freuder","year":"1978","unstructured":"Freuder, E.C.: Synthesizing constraint expressions. Communication of ACM\u00a021(11), 958\u2013966 (1978)","journal-title":"Communication of ACM"},{"key":"31_CR4","unstructured":"Frisch, A.M., Peugniez, T.J.: Solving non-Boolean satisfiability problems with stochastic local search. In: IJCAI 2001, pp. 282\u2013290 (2001)"},{"key":"31_CR5","unstructured":"Gent, I.P.: Arc consistency in SAT. In: ECAI 2002, pp. 121\u2013125 (2002)"},{"issue":"4","key":"31_CR6","first-page":"963","volume":"3","author":"K. Ghiathi","year":"2004","unstructured":"Ghiathi, K., Ghassem-Sani, G.: Using satisfiability in temporal planning. WSEAS Transactions on Computers\u00a03(4), 963\u2013969 (2004)","journal-title":"WSEAS Transactions on Computers"},{"key":"31_CR7","doi-asserted-by":"crossref","unstructured":"Golumbic, M.C., Shamir, R.: Complexity and algorithms for reasoning about time: A graph-theoretic approach. Journal of ACM, 1108\u20131133 (1993)","DOI":"10.1145\/174147.169675"},{"key":"31_CR8","unstructured":"Hoos, H.H.: SAT-encodings, search space structure, and local search performance. In: IJCAI 1999, pp. 296\u2013302 (1999)"},{"key":"31_CR9","unstructured":"Kautz, H., McAllester, D., Selman, B.: Encoding plans in propositional logic. In: KR 1996, pp. 374\u2013384 (1996)"},{"issue":"1","key":"31_CR10","doi-asserted-by":"publisher","first-page":"105","DOI":"10.1016\/0004-3702(92)90106-8","volume":"57","author":"P. Ladkin","year":"1992","unstructured":"Ladkin, P., Reinefeld, A.: Effective solution of qualitative interval constraint problems. Artificial Intelligence\u00a057(1), 105\u2013124 (1992)","journal-title":"Artificial Intelligence"},{"issue":"1","key":"31_CR11","doi-asserted-by":"publisher","first-page":"99","DOI":"10.1016\/0004-3702(77)90007-8","volume":"8","author":"A.K. Mackworth","year":"1977","unstructured":"Mackworth, A.K.: Consistency in networks of relations. Artificial Intelligence\u00a08(1), 99\u2013118 (1977)","journal-title":"Artificial Intelligence"},{"key":"31_CR12","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, pp. 530\u2013535 (2001)","DOI":"10.1145\/378239.379017"},{"issue":"3","key":"31_CR13","doi-asserted-by":"publisher","first-page":"175","DOI":"10.1007\/BF00137869","volume":"1","author":"B. Nebel","year":"1997","unstructured":"Nebel, B.: Solving hard qualitative temporal reasoning problems: Evaluating the efficiency of using the ORD-Horn class. Constraints\u00a01(3), 175\u2013190 (1997)","journal-title":"Constraints"},{"issue":"1","key":"31_CR14","doi-asserted-by":"publisher","first-page":"43","DOI":"10.1145\/200836.200848","volume":"42","author":"B. Nebel","year":"1995","unstructured":"Nebel, B., B\u00fcrckert, H.-J.: Reasoning about temporal relations: A maximal tractable subclass of Allen\u2019s Interval Algebra. Journal of ACM\u00a042(1), 43\u201366 (1995)","journal-title":"Journal of ACM"},{"key":"31_CR15","doi-asserted-by":"crossref","unstructured":"Prestwich, S.: Local search on SAT-encoded colouring problems. In: SAT 2003, pp. 105\u2013119 (2003)","DOI":"10.1007\/978-3-540-24605-3_9"},{"issue":"1-2","key":"31_CR16","doi-asserted-by":"publisher","first-page":"155","DOI":"10.1016\/0004-3702(95)00052-6","volume":"81","author":"B.M. Smith","year":"1996","unstructured":"Smith, B.M., Dyer, M.E.: Locating the phase transition in binary constraint satisfaction problems. Artificial Intelligence\u00a081(1-2), 155\u2013181 (1996)","journal-title":"Artificial Intelligence"},{"issue":"1","key":"31_CR17","doi-asserted-by":"publisher","first-page":"93","DOI":"10.1093\/logcom\/14.1.93","volume":"14","author":"J. Thornton","year":"2004","unstructured":"Thornton, J., Beaumont, M., Sattar, A., Maher, M.: A local search approach to modelling and solving Interval Algebra problems. Journal of Logic and Computation\u00a014(1), 93\u2013112 (2004)","journal-title":"Journal of Logic and Computation"},{"key":"31_CR18","doi-asserted-by":"publisher","first-page":"297","DOI":"10.1016\/0004-3702(92)90011-L","volume":"58","author":"P. Beek van","year":"1992","unstructured":"van Beek, P.: Reasoning about qualitative temporal information. Artificial Intelligence\u00a058, 297\u2013326 (1992)","journal-title":"Artificial Intelligence"},{"key":"31_CR19","doi-asserted-by":"publisher","first-page":"132","DOI":"10.1111\/j.1467-8640.1990.tb00130.x","volume":"6","author":"P. Beek van","year":"1990","unstructured":"van Beek, P., Cohen, R.: Exact and approximate reasoning about temporal relations. Computational Intelligence\u00a06, 132\u2013144 (1990)","journal-title":"Computational Intelligence"},{"key":"31_CR20","doi-asserted-by":"crossref","first-page":"1","DOI":"10.1613\/jair.232","volume":"4","author":"P. Beek van","year":"1996","unstructured":"van Beek, P., Manchak, D.W.: The design and experimental analysis of algorithms for temporal reasoning. Journal of Artificial Intelligence Research\u00a04, 1\u201318 (1996)","journal-title":"Journal of Artificial Intelligence Research"},{"key":"31_CR21","unstructured":"Vilain, M., Kautz, H.: Constraint propagation algorithms for temporal reasoning. In: AAAI 1986, pp. 377\u2013382 (1986)"},{"key":"31_CR22","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"441","DOI":"10.1007\/3-540-45349-0_32","volume-title":"Principles and Practice of Constraint Programming - CP 2000","author":"T. Walsh","year":"2000","unstructured":"Walsh, T.: SAT v CSP. In: Dechter, R. (ed.) CP 2000. LNCS, vol.\u00a01894, pp. 441\u2013456. Springer, Heidelberg (2000)"}],"container-title":["Lecture Notes in Computer Science","Principles and Practice of Constraint Programming - CP 2006"],"original-title":[],"link":[{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/11889205_31.pdf","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2020,11,17]],"date-time":"2020-11-17T19:51:27Z","timestamp":1605642687000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/11889205_31"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2006]]},"ISBN":["9783540462675","9783540462682"],"references-count":22,"URL":"https:\/\/doi.org\/10.1007\/11889205_31","relation":{},"ISSN":["0302-9743","1611-3349"],"issn-type":[{"value":"0302-9743","type":"print"},{"value":"1611-3349","type":"electronic"}],"subject":[],"published":{"date-parts":[[2006]]}}}