Skip to main content

SAT-Based Procedures for Temporal Reasoning

  • Conference paper
Recent Advances in AI Planning (ECP 1999)

Part of the book series: Lecture Notes in Computer Science ((LNAI,volume 1809))

Included in the following conference series:

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.

This is a preview of subscription content, log in via an institution to check access.

Access this chapter

Chapter
USD 29.95
Price excludes VAT (USA)
  • Available as PDF
  • Read on any device
  • Instant download
  • Own it forever
eBook
USD 39.99
Price excludes VAT (USA)
  • Available as PDF
  • Read on any device
  • Instant download
  • Own it forever
Softcover Book
USD 54.99
Price excludes VAT (USA)
  • Compact, lightweight edition
  • Dispatched in 3 to 5 business days
  • Free shipping worldwide - see info

Tax calculation will be finalised at checkout

Purchases are for personal use only

Institutional subscriptions

Preview

Unable to display preview. Download preview PDF.

Unable to display preview. Download preview PDF.

References

  1. Allen, J., Kautz, H., Pelavin, R. (eds.): Reasoning about Plans. Morgan Kaufmann, San Francisco (1991)

    MATH  Google Scholar 

  2. Brusoni, V., Console, L., Pernici, B., Terenziani, P.: LaTeR: An Efficient, General Purpose Manager of Temporal Information. IEEE Software (1996)

    Google Scholar 

  3. Buro, M., Buning, H.: Report on a SAT competition. Technical Report 110, University of Paderborn, Germany (November 1992)

    Google Scholar 

  4. 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)

    Google Scholar 

  5. Chleq, N.: Efficient algorithms for networks of quantitative temporal constraints. In: Proceedings of CONSTRAINTS 1995, April 1995, pp. 40–45 (1995)

    Google Scholar 

  6. D’Agostino, M.: Are Tableaux an Improvement on Truth-Tables? Journal of Logic, Language and Information 1, 235–252 (1992)

    Article  MATH  MathSciNet  Google Scholar 

  7. Davis, M., Putnam, H.: A computing procedure for quantification theory. Journal of the ACM 7, 201–215 (1960)

    Article  MATH  MathSciNet  Google Scholar 

  8. Dechter, R., Meiri, I., Pearl, J.: Temporal constraint networks. Artificial Intelligence 49(1-3), 61–95 (1991)

    Article  MATH  MathSciNet  Google Scholar 

  9. Freeman, J.W.: Improvements to propositional satisfiability search algorithms. PhD thesis, University of Pennsylvania (1995)

    Google Scholar 

  10. 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)

    Google Scholar 

  11. 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

  12. Haralick, R.M., Elliott, G.L.: Increasing Tree Search Efficiency for Constraint Satisfaction Problems. Acta Informatica 14, 263–313 (1980)

    Google Scholar 

  13. 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)

    Google Scholar 

  14. Koubarakis, M.: The complexity of query evaluation in indefinite temporal constraint databases. Theoretical Computer Science 171(1-2), 25–60 (1997)

    Article  MATH  MathSciNet  Google Scholar 

  15. Prosser, P.: Hybrid algorithms for the constraint satisfaction problem. Computational Intelligence 9(3), 268–299 (1993)

    Article  Google Scholar 

  16. Smullyan, R.M.: First-Order Logic. Springer, NY (1968)

    MATH  Google Scholar 

  17. Stergiou, K., Koubarakis, M.: Back tracking algorithms for disjunctions of temporal constraints. In: Proc. AAAI (1998)

    Google Scholar 

Download references

Author information

Authors and Affiliations

Authors

Editor information

Editors and Affiliations

Rights and permissions

Reprints 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

Publish with us

Policies and ethics