Abstract
In this paper we study the consistency problem for a set of disjunctive temporal constraints [Stergiou and Koubarakis, 1998]. We propose two SAT-based procedures, and show that—on sets of binary randomly generated disjunctive constraints—they perform up to 2 orders of magnitude less consistency checks than the best procedure presented in [Stergiou and Koubarakis, 1998]. On these tests, our experimental analysis confirms Stergiou and Koubarakis’s result about the existence of an easy-hard-easy pattern whose peak corresponds to a value in between 6 and 7 of the ratio of clauses to variables.
Access this chapter
Tax calculation will be finalised at checkout
Purchases are for personal use only
Preview
Unable to display preview. Download preview PDF.
References
Allen, J., Kautz, H., Pelavin, R. (eds.): Reasoning about Plans. Morgan Kaufmann, San Francisco (1991)
Brusoni, V., Console, L., Pernici, B., Terenziani, P.: LaTeR: An Efficient, General Purpose Manager of Temporal Information. IEEE Software (1996)
Buro, M., Buning, H.: Report on a SAT competition. Technical Report 110, University of Paderborn, Germany (November 1992)
Cheng, C.-C., Smith, S.F.: Generating feasible schedules under complex metric constraints. In: Proceedings of the Twelfth National Conference on Artificial Intelligence (AAAI 1994), Seattle, Washington, USA, vol. 2, pp. 1086–1091. AAAI Press/MIT Press (1994)
Chleq, N.: Efficient algorithms for networks of quantitative temporal constraints. In: Proceedings of CONSTRAINTS 1995, April 1995, pp. 40–45 (1995)
D’Agostino, M.: Are Tableaux an Improvement on Truth-Tables? Journal of Logic, Language and Information 1, 235–252 (1992)
Davis, M., Putnam, H.: A computing procedure for quantification theory. Journal of the ACM 7, 201–215 (1960)
Dechter, R., Meiri, I., Pearl, J.: Temporal constraint networks. Artificial Intelligence 49(1-3), 61–95 (1991)
Freeman, J.W.: Improvements to propositional satisfiability search algorithms. PhD thesis, University of Pennsylvania (1995)
Giunchiglia, F., Sebastiani, R.: Building decision procedures for modal logics from propositional decision procedures - the case study of modal K. In: McRobbie, M.A., Slaney, J.K. (eds.) CADE 1996. LNCS, vol. 1104. Springer, Heidelberg (1996)
Giunchiglia, E., Giunchiglia, F., Tacchella, A.: SAT- Based Decision Procedures for Classical Modal Logics. Accepted for publication in Journal of Automated Reasoning (2000), Available at http://www.mrg.dist.unige.it/~enrico
Haralick, R.M., Elliott, G.L.: Increasing Tree Search Efficiency for Constraint Satisfaction Problems. Acta Informatica 14, 263–313 (1980)
Jonsson, P., Bäckström, C.: A linear- programming approach to temporal reasoning. In: Proceedings of the Thirteenth National Conference on Artificial Intelligence and the Eighth Innovative Applications of Artificial Intelligence Conference, Menlo Park, August 4-8, pp. 1235–1241. AAAI Press / MIT Press (1996)
Koubarakis, M.: The complexity of query evaluation in indefinite temporal constraint databases. Theoretical Computer Science 171(1-2), 25–60 (1997)
Prosser, P.: Hybrid algorithms for the constraint satisfaction problem. Computational Intelligence 9(3), 268–299 (1993)
Smullyan, R.M.: First-Order Logic. Springer, NY (1968)
Stergiou, K., Koubarakis, M.: Back tracking algorithms for disjunctions of temporal constraints. In: Proc. AAAI (1998)
Author information
Authors and Affiliations
Editor information
Editors and Affiliations
Rights and permissions
Copyright information
© 2000 Springer-Verlag Berlin Heidelberg
About this paper
Cite this paper
Armando, A., Castellini, C., Giunchiglia, E. (2000). SAT-Based Procedures for Temporal Reasoning. In: Biundo, S., Fox, M. (eds) Recent Advances in AI Planning. ECP 1999. Lecture Notes in Computer Science(), vol 1809. Springer, Berlin, Heidelberg. https://doi.org/10.1007/10720246_8
Download citation
DOI: https://doi.org/10.1007/10720246_8
Publisher Name: Springer, Berlin, Heidelberg
Print ISBN: 978-3-540-67866-3
Online ISBN: 978-3-540-44657-6
eBook Packages: Springer Book Archive