×

Modelling and solving temporal reasoning as propositional satisfiability. (English) Zbl 1184.68485

Summary: Representing and reasoning about time dependent information is a key research issue in many areas of computer science and artificial intelligence. One of the best known and widely used formalisms for representing interval-based qualitative temporal information is Allen’s interval algebra (IA). The fundamental reasoning task in IA is to find a scenario that is consistent with the given information. This problem is in general NP-complete. In this paper, we investigate how an interval-based representation, or IA network, can be encoded into a propositional formula of Boolean variables and/or predicates in decidable theories. Our task is to discover whether satisfying such a formula can be more efficient than finding a consistent scenario for the original problem. There are two basic approaches to modelling an IA network: one represents the relations between intervals as variables and the other represents the end-points of each interval as variables. By combining these two approaches with three different Boolean satisfiability (SAT) encoding schemes, we produced six encoding schemes for converting IA to SAT. In addition, we also showed how IA networks can be formulated into satisfiability modulo theories (SMT) formulae based on the quantifier-free integer difference logic (QF-IDL). These encodings were empirically studied using randomly generated IA problems of sizes ranging from 20 to 100 nodes. A general conclusion we draw from these experimental results is that encoding IA into SAT produces better results than existing approaches. More specifically, we show that the new point-based 1-D support SAT encoding of IA produces consistently better results than the other alternatives considered. In comparison with the six different SAT encodings, the SMT encoding came fourth after the point-based and interval-based 1-D support schemes and the point-based direct scheme. Further, we observe that the phase transition region maps directly from the IA encoding to each SAT or SMT encoding, but, surprisingly, the location of the hard region varies according to the encoding scheme. Our results also show a fixed performance ranking order over the various encoding schemes.

MSC:

68T27 Logic in artificial intelligence
68Q25 Analysis of algorithms and problem complexity
68T20 Problem solving in the context of artificial intelligence (heuristics, search strategies, etc.)
PDFBibTeX XMLCite
Full Text: DOI Link

References:

[1] Allen, J. F., Maintaining knowledge about temporal intervals, Communications of the ACM, 26, 832-843 (1983) · Zbl 0519.68079
[2] Anbulagan, D. Nghia Pham, J. Slaney, A. Sattar, Old resolution meets modern SLS, in: Proceedings of the Twentieth National Conference on Artificial Intelligence (AAAI-05), 2005, pp. 354-359; Anbulagan, D. Nghia Pham, J. Slaney, A. Sattar, Old resolution meets modern SLS, in: Proceedings of the Twentieth National Conference on Artificial Intelligence (AAAI-05), 2005, pp. 354-359
[3] A. Armando, C. Castellini, E. Giunchiglia, SAT-based procedures for temporal reasoning, in: Proceedings of the Fifth European Conference on Planning, 2000, pp. 97-108; A. Armando, C. Castellini, E. Giunchiglia, SAT-based procedures for temporal reasoning, in: Proceedings of the Fifth European Conference on Planning, 2000, pp. 97-108 · Zbl 1098.68693
[4] A. Armando, C. Castellini, E. Giunchiglia, M. Idini, M. Maratea, TSAT++: An open platform for satisfiability modulo theories, in: Proceedings of the Second Workshop on Pragmatics of Decision Procedures in Automated Reasoning (PDPAR-04), 2004; A. Armando, C. Castellini, E. Giunchiglia, M. Idini, M. Maratea, TSAT++: An open platform for satisfiability modulo theories, in: Proceedings of the Second Workshop on Pragmatics of Decision Procedures in Automated Reasoning (PDPAR-04), 2004 · Zbl 1272.68369
[5] A. Armando, C. Castellini, E. Giunchiglia, M. Maratea, A SAT-based decision procedure for the boolean combination of difference constraints, in: Proceedings of the Seventh International Conference on Theory and Applications of Satisfiability Testing SAT 2004, Selected Revised Papers, Lecture Notes in Computer Science, vol. 3542, 2004, pp. 16-29; A. Armando, C. Castellini, E. Giunchiglia, M. Maratea, A SAT-based decision procedure for the boolean combination of difference constraints, in: Proceedings of the Seventh International Conference on Theory and Applications of Satisfiability Testing SAT 2004, Selected Revised Papers, Lecture Notes in Computer Science, vol. 3542, 2004, pp. 16-29 · Zbl 1122.68583
[6] R. Béjar, F. Manyà, Solving the round robin problem using propositional logic, in: Proceedings of the Seventeenth National Conference on Artificial Intelligence (AAAI-00), 2000, pp. 262-266; R. Béjar, F. Manyà, Solving the round robin problem using propositional logic, in: Proceedings of the Seventeenth National Conference on Artificial Intelligence (AAAI-00), 2000, pp. 262-266
[7] C. Bessière, E. Hebrard, T. Walsh, Local consistencies in SAT, in: Proceedings of the Sixth International Conference on Theory and Applications of Satisfiability Testing SAT 2003, Selected Revised Papers, Lecture Notes in Computer Science, vol. 2919, 2003, pp. 299-314; C. Bessière, E. Hebrard, T. Walsh, Local consistencies in SAT, in: Proceedings of the Sixth International Conference on Theory and Applications of Satisfiability Testing SAT 2003, Selected Revised Papers, Lecture Notes in Computer Science, vol. 2919, 2003, pp. 299-314
[8] P. Cheeseman, B. Kanefsky, W.M. Taylor, Where the really hard problems are, in: Proceedings of the Twelfth International Joint Conference on Artificial Intelligence (IJCAI-91), 1991, pp. 331-337; P. Cheeseman, B. Kanefsky, W.M. Taylor, Where the really hard problems are, in: Proceedings of the Twelfth International Joint Conference on Artificial Intelligence (IJCAI-91), 1991, pp. 331-337 · Zbl 0747.68064
[9] Crawford, J. M.; Auton, L. D., Experimental results on the crossover point in random 3-SAT, Artificial Intelligence, 81, 1-2, 31-57 (1996) · Zbl 1508.68324
[10] Dechter, R., Constraint Processing (2003), Morgan Kaufmann: Morgan Kaufmann San Francisco
[11] Dechter, R.; Meiri, I.; Pearl, J., Temporal constraint networks, Artificial Intelligence, 49, 1-3, 61-95 (1991) · Zbl 0737.68070
[12] Dixon, H. E.; Ginsberg, M. L.; Parkes, A. J., Generalizing Boolean satisfiability I: Background and survey of existing work, Journal of Artificial Intelligence Research, 21, 193-243 (2004) · Zbl 1080.68661
[13] B. Dutertre, L. Mendonça de Moura, A fast linear-arithmetic solver for DPLL(T), in: Proceedings of the Eighteenth International Conference on Computer Aided Verification, 2006, pp. 81-94; B. Dutertre, L. Mendonça de Moura, A fast linear-arithmetic solver for DPLL(T), in: Proceedings of the Eighteenth International Conference on Computer Aided Verification, 2006, pp. 81-94
[14] N. Eén, N. Sörensson, An extensible SAT solver, in: Proceedings of the Sixth International Conference on Theory and Applications of Satisfiability Testing (SAT-03), Selected Revised Papers, Lecture Notes in Computer Science, vol. 2919, 2003, pp. 502-518; N. Eén, N. Sörensson, An extensible SAT solver, in: Proceedings of the Sixth International Conference on Theory and Applications of Satisfiability Testing (SAT-03), Selected Revised Papers, Lecture Notes in Computer Science, vol. 2919, 2003, pp. 502-518
[15] Freuder, E. C., Synthesizing constraint expressions, Communication of ACM, 21, 11, 958-966 (1978) · Zbl 0386.68065
[16] Freuder, E. C., A sufficient condition for backtrack-free search, Journal of ACM, 29, 1, 24-32 (1982) · Zbl 0477.68063
[17] A.M. Frisch, T.J. Peugniez, Solving non-Boolean satisfiability problems with stochastic local search, in: Proceedings of the Seventeenth International Joint Conference on Artificial Intelligence (IJCAI-01), 2001, pp. 282-290; A.M. Frisch, T.J. Peugniez, Solving non-Boolean satisfiability problems with stochastic local search, in: Proceedings of the Seventeenth International Joint Conference on Artificial Intelligence (IJCAI-01), 2001, pp. 282-290
[18] I.P. Gent, Arc consistency in SAT, in: Proceedings of the Fifteenth European Conference on Artificial Intelligence (ECAI-02), 2002, pp. 121-125; I.P. Gent, Arc consistency in SAT, in: Proceedings of the Fifteenth European Conference on Artificial Intelligence (ECAI-02), 2002, pp. 121-125
[19] I.P. Gent, T. Walsh, The SAT phase transition, in: Proceedings of the Eleventh European Conference on Artificial Intelligence (ECAI-94), 1994, pp. 105-109; I.P. Gent, T. Walsh, The SAT phase transition, in: Proceedings of the Eleventh European Conference on Artificial Intelligence (ECAI-94), 1994, pp. 105-109
[20] Ghiathi, K.; Ghassem-Sani, G., Using satisfiability in temporal planning, WSEAS Transactions on Computers, 3, 4, 963-969 (2004)
[21] Golumbic, M. C.; Shamir, R., Complexity and algorithms for reasoning about time: A graph-theoretic approach, Journal of ACM, 1108-1133 (1993) · Zbl 0795.68095
[22] Haralick, R. M.; Elliott, G. L., Increasing tree search efficiency for constraint satisfaction problems, Artificial Intelligence, 14, 3, 263-313 (1980)
[23] Hooker, J. N., Needed: an empirical science of algorithms, Operations Research, 42, 2, 201-212 (1994) · Zbl 0805.90119
[24] H.H. Hoos, SAT-encodings, search space structure, and local search performance, in: Proceedings of the Sixteenth International Joint Conference on Artificial Intelligence (IJCAI-99), 1999, pp. 296-302; H.H. Hoos, SAT-encodings, search space structure, and local search performance, in: Proceedings of the Sixteenth International Joint Conference on Artificial Intelligence (IJCAI-99), 1999, pp. 296-302
[25] F. Hutter, D.A.D. Tompkins, H.H. Hoos, Scaling and probabilistic smoothing: Efficient dynamic local search for SAT, in: Proceedings of the Eighth International Conference on Principles and Practice of Constraint Programming (CP-02), 2002, pp. 233-248; F. Hutter, D.A.D. Tompkins, H.H. Hoos, Scaling and probabilistic smoothing: Efficient dynamic local search for SAT, in: Proceedings of the Eighth International Conference on Principles and Practice of Constraint Programming (CP-02), 2002, pp. 233-248
[26] H. Kautz, D. McAllester, B. Selman, Encoding plans in propositional logic, in: Proceedings of the Fifth International Conference on Principles of Knowledge Representation and Reasoning (KR-96), 1996, pp. 374-384; H. Kautz, D. McAllester, B. Selman, Encoding plans in propositional logic, in: Proceedings of the Fifth International Conference on Principles of Knowledge Representation and Reasoning (KR-96), 1996, pp. 374-384
[27] H. Kautz, Y. Ruan, D. Achlioptas, C. Gomes, B. Selman, M. Stickel, Balance and filtering in structured satisfiable problems, in: Proceedings of the Seventeenth International Joint Conference on Artificial Intelligence (IJCAI-01), 2001, pp. 351-358; H. Kautz, Y. Ruan, D. Achlioptas, C. Gomes, B. Selman, M. Stickel, Balance and filtering in structured satisfiable problems, in: Proceedings of the Seventeenth International Joint Conference on Artificial Intelligence (IJCAI-01), 2001, pp. 351-358 · Zbl 0985.90509
[28] H. Kautz, B. Selman, Pushing the envelope: Planning, propositional logic, and stochastic search, in: Proceedings of the Thirteenth National Conference on Artificial Intelligence (AAAI-96), 1996, pp. 1194-1201; H. Kautz, B. Selman, Pushing the envelope: Planning, propositional logic, and stochastic search, in: Proceedings of the Thirteenth National Conference on Artificial Intelligence (AAAI-96), 1996, pp. 1194-1201
[29] Ladkin, P.; Reinefeld, A., Effective solution of qualitative interval constraint problems, Artificial Intelligence, 57, 1, 105-124 (1992)
[30] P. Ladkin, A. Reinefeld, A symbolic approach to interval constraint problems, in: Artificial Intelligence and Symbolic Mathematical Computation, 1993, pp. 65-84; P. Ladkin, A. Reinefeld, A symbolic approach to interval constraint problems, in: Artificial Intelligence and Symbolic Mathematical Computation, 1993, pp. 65-84
[31] Ladkin, P.; Reinefeld, A., Fast algebraic methods for interval constraint problems, Annals of Mathematics and Artificial Intelligence, 19, 383-411 (1997) · Zbl 0880.68012
[32] C.M. Li, Anbulagan, Look-ahead versus look-back for satisfiability problems, in: Proceedings of the Third International Conference on Principles and Practice of Constraint Programming (CP-97), 1997, pp. 341-355; C.M. Li, Anbulagan, Look-ahead versus look-back for satisfiability problems, in: Proceedings of the Third International Conference on Principles and Practice of Constraint Programming (CP-97), 1997, pp. 341-355
[33] Mackworth, A. K., Consistency in networks of relations, Artificial Intelligence, 8, 1, 99-118 (1977) · Zbl 0341.68061
[34] D. Mitchell, B. Selman, H. Levesque, Hard and easy distributions of SAT problems, in: Proceedings of the Tenth National Conference on Artificial Intelligence (AAAI-92), 1992, pp. 459-465; D. Mitchell, B. Selman, H. Levesque, Hard and easy distributions of SAT problems, in: Proceedings of the Tenth National Conference on Artificial Intelligence (AAAI-92), 1992, pp. 459-465
[35] M.W. Moskewicz, C.F. Madigan, Y. Zhao, L. Zhang, S. Malik, Chaff: Engineering an efficient SAT solver, in: Proceedings of the 38th Design Automation Conference (DAC-01), 2001, pp. 530-535; M.W. Moskewicz, C.F. Madigan, Y. Zhao, L. Zhang, S. Malik, Chaff: Engineering an efficient SAT solver, in: Proceedings of the 38th Design Automation Conference (DAC-01), 2001, pp. 530-535
[36] Nebel, B., Solving hard qualitative temporal reasoning problems: Evaluating the efficiency of using the ORD-Horn class, Constraints, 1, 3, 175-190 (1997) · Zbl 0870.68138
[37] Nebel, B.; Bürckert, H.-J., Reasoning about temporal relations: A maximal tractable subclass of Allen’s Interval Algebra, Journal of ACM, 42, 1, 43-66 (1995) · Zbl 0886.68077
[38] D. Nghia Pham, J. Thornton, A. Sattar, Modelling and solving temporal reasoning as satisfiability, in: Proceedings of the 4th International Workshop on Modelling and Reformulating Constraint Satisfaction Problems, 2005, pp. 117-131; D. Nghia Pham, J. Thornton, A. Sattar, Modelling and solving temporal reasoning as satisfiability, in: Proceedings of the 4th International Workshop on Modelling and Reformulating Constraint Satisfaction Problems, 2005, pp. 117-131 · Zbl 1184.68485
[39] D. Nghia Pham, J. Thornton, A. Sattar, Towards an efficient SAT encoding for temporal reasoning, in: Proceedings of the Twelfth International Conference on the Principles and Practice of Constraint Programming (CP-06), 2006, pp. 421-436; D. Nghia Pham, J. Thornton, A. Sattar, Towards an efficient SAT encoding for temporal reasoning, in: Proceedings of the Twelfth International Conference on the Principles and Practice of Constraint Programming (CP-06), 2006, pp. 421-436
[40] D. Nghia Pham, J. Thornton, A. Sattar, A. Ishtaiwi, SAT-based versus CSP-based constraint weighting for satisfiability, in: Proceedings of the Twentieth National Conference on Artificial Intelligence (AAAI-05), 2005, pp. 455-460; D. Nghia Pham, J. Thornton, A. Sattar, A. Ishtaiwi, SAT-based versus CSP-based constraint weighting for satisfiability, in: Proceedings of the Twentieth National Conference on Artificial Intelligence (AAAI-05), 2005, pp. 455-460
[41] S. Prestwich, Local search on SAT-encoded colouring problems, in: Proceedings of the Sixth International Conference on Theory and Applications of Satisfiability Testing (SAT-03), Selected Revised Papers, Lecture Notes in Computer Science, vol. 2919, 2003, pp. 105-119; S. Prestwich, Local search on SAT-encoded colouring problems, in: Proceedings of the Sixth International Conference on Theory and Applications of Satisfiability Testing (SAT-03), Selected Revised Papers, Lecture Notes in Computer Science, vol. 2919, 2003, pp. 105-119 · Zbl 1204.68208
[42] Prosser, P., An empirical study of phase transitions in binary constraint satisfaction problems, Artificial Intelligence, 81, 1-2, 81-109 (1996) · Zbl 1523.68093
[43] A.K. Pujari, G. Vijaya Kumari, A. Sattar, INDU: An interval and duration network, in: Proceedings of the Twelfth Australian Joint Conference on Artificial Intelligence, 1999, pp. 291-303; A.K. Pujari, G. Vijaya Kumari, A. Sattar, INDU: An interval and duration network, in: Proceedings of the Twelfth Australian Joint Conference on Artificial Intelligence, 1999, pp. 291-303
[44] S. Ranise, C. Tinelli, The Satisfiability Modulo Theories Library (SMT-LIB), www.SMT-LIB.org; S. Ranise, C. Tinelli, The Satisfiability Modulo Theories Library (SMT-LIB), www.SMT-LIB.org
[45] Renz, J.; Nebel, B., Efficient methods for qualitative spatial reasoning, Journal of Artificial Intelligence Research, 15, 289-318 (2001) · Zbl 0994.68106
[46] B. Selman, H. Kautz, D. McAllester, Ten challenges in propositional reasoning and search, in: Proceedings of the Fifteenth International Joint Conference on Artificial Intelligence (IJCAI-97), 1997, pp. 50-54; B. Selman, H. Kautz, D. McAllester, Ten challenges in propositional reasoning and search, in: Proceedings of the Fifteenth International Joint Conference on Artificial Intelligence (IJCAI-97), 1997, pp. 50-54
[47] Smith, B. M.; Dyer, M. E., Locating the phase transition in binary constraint satisfaction problems, Artificial Intelligence, 81, 1-2, 155-181 (1996) · Zbl 1508.68348
[48] Thornton, J.; Beaumont, M.; Sattar, A.; Maher, M., A local search approach to modelling and solving Interval Algebra problems, Journal of Logic and Computation, 14, 1, 93-112 (2004) · Zbl 1085.68154
[49] J. Thornton, D. Nghia Pham, S. Bain, V. Ferreira Jr., Additive versus multiplicative clause weighting for SAT, in: Proceedings of the Twentieth National Conference on Artificial Intelligence (AAAI-04), 2004, pp. 191-196; J. Thornton, D. Nghia Pham, S. Bain, V. Ferreira Jr., Additive versus multiplicative clause weighting for SAT, in: Proceedings of the Twentieth National Conference on Artificial Intelligence (AAAI-04), 2004, pp. 191-196
[50] Tsamardinos, I.; Pollack, M., Efficient solution techniques for disjunctive temporal reasoning problems, Artificial Intelligence, 151, 1, 43-89 (2003) · Zbl 1082.68825
[51] van Beek, P., Reasoning about qualitative temporal information, Artificial Intelligence, 58, 297-326 (1992) · Zbl 0782.68106
[52] van Beek, P.; Cohen, R., Exact and approximate reasoning about temporal relations, Computational Intelligence, 6, 132-144 (1990)
[53] van Beek, P.; Manchak, D. W., The design and experimental analysis of algorithms for temporal reasoning, Journal of Artificial Intelligence Research, 4, 1-18 (1996) · Zbl 0900.68389
[54] M. Vilain, H. Kautz, Constraint propagation algorithms for temporal reasoning, in: Proceedings of the Fifth National Conference on Artificial Intelligence (AAAI-86), 1986, pp. 377-382; M. Vilain, H. Kautz, Constraint propagation algorithms for temporal reasoning, in: Proceedings of the Fifth National Conference on Artificial Intelligence (AAAI-86), 1986, pp. 377-382
[55] T. Walsh, SAT v CSP, in: Proceedings of the Sixth International Conference on Principles and Practice of Constraint Programming (CP-00), 2000, pp. 441-456; T. Walsh, SAT v CSP, in: Proceedings of the Sixth International Conference on Principles and Practice of Constraint Programming (CP-00), 2000, pp. 441-456
This reference list is based on information provided by the publisher or from digital mathematics libraries. Its items are heuristically matched to zbMATH identifiers and may contain data conversion errors. In some cases that data have been complemented/enhanced by data from zbMATH Open. This attempts to reflect the references listed in the original paper as accurately as possible without claiming completeness or a perfect matching.