Abstract
Many applications, such as scheduling and temporal planning, require the solution of Temporal Problems (TP’s) representing constraints over the timing of activities. A TP with uncertainty (TPU) is characterized by activities with uncontrollable duration. Depending on the Boolean structure of the constraints, we have simple (STPU), constraint satisfaction (TCSPU), and disjunctive (DTPU) temporal problems with uncertainty.
In this work we tackle the problem of strong controllability, i.e. finding an assignment to all the controllable time points, such that the constraints are fulfilled under any possible assignment of uncontrollable time points. We work in the framework of Satisfiability Modulo Theory (SMT), where uncertainty is expressed by means of universal quantifiers. We obtain the first practical and comprehensive solution for strong controllability: the use of quantifier elimination techniques leads to quantifier-free encodings, which are in turn solved with efficient SMT solvers.
We provide a detailed experimental evaluation of our approach over a large set of benchmarks. The results clearly demonstrate that the proposed approach is feasible, and outperforms the best state-of-the-art competitors, when available.
This is a preview of subscription content, log in via an institution to check access.
Access this chapter
Tax calculation will be finalised at checkout
Purchases are for personal use only
Preview
Unable to display preview. Download preview PDF.
Similar content being viewed by others
References
Dechter, R., Meiri, I., Pearl, J.: Temporal constraint networks. Artif. Intell. 49, 61–95 (1991)
Vidal, T., Fargier, H.: Handling contingency in temporal constraint networks: from consistency to controllabilities. Journal of Experimental Theoretical Artificial Intelligence 11, 23–45 (1999)
Barrett, C.W., Sebastiani, R., Seshia, S.A., Tinelli, C.: Satisfiability modulo theories. In: Handbook of Satisfiability, pp. 825–885. IOS Press (2009)
Bruttomesso, R., Cimatti, A., Franzén, A., Griggio, A., Sebastiani, R.: The MathSAT 4 SMT Solver. In: Gupta, A., Malik, S. (eds.) CAV 2008. LNCS, vol. 5123, pp. 299–303. Springer, Heidelberg (2008)
Cimatti, A., Griggio, A., Sebastiani, R., Schaafsma, B.: The MathSAT5 SMT solver (2011), http://mathsat.fbk.eu
de Moura, L., Bjørner, N.: Z3: An Efficient SMT Solver. In: Ramakrishnan, C.R., Rehof, J. (eds.) TACAS 2008. LNCS, vol. 4963, pp. 337–340. Springer, Heidelberg (2008)
Dutertre, B., de Moura, L.: The Yices SMT solver (2006), Tool paper at http://yices.csl.sri.com/tool-paper.pdf
Bruttomesso, R., Pek, E., Sharygina, N., Tsitovich, A.: The OpenSMT Solver. In: Esparza, J., Majumdar, R. (eds.) TACAS 2010. LNCS, vol. 6015, pp. 150–153. Springer, Heidelberg (2010)
Niemelä, I.: Integrating Answer Set Programming and Satisfiability Modulo Theories. In: Erdem, E., Lin, F., Schaub, T. (eds.) LPNMR 2009. LNCS, vol. 5753, p. 3. Springer, Heidelberg (2009)
Franzén, A., Cimatti, A., Nadel, A., Sebastiani, R., Shalev, J.: Applying SMT in symbolic execution of microcode. In: Bloem, R., Sharygina, N. (eds.) Formal Methods in Computer-Aided Design - FMCAD, pp. 121–128. IEEE (2010)
Godefroid, P., Levin, M.Y., Molnar, D.A.: Automated whitebox fuzz testing. In: Network and Distributed System Security Symposium - NDSS. The Internet Society (2008)
Kleene, S.: Mathematical Logic. J. Wiley & Sons (1967)
Moskewicz, M.W., Madigan, C.F., Zhao, Y., Zhang, L., Malik, S.: Chaff: Engineering an Efficient SAT Solver. In: Design Automation Conference - DAC, pp. 530–535. ACM Press, New York (2001)
Schrijver, A.: Theory of Linear and Integer Programming. J. Wiley & Sons (1998)
Loos, R., Weispfenning, V.: Applying linear quantifier elimination. Computer Journal 36, 450–462 (1993)
Monniaux, D.: A Quantifier Elimination Algorithm for Linear Real Arithmetic. In: Cervesato, I., Veith, H., Voronkov, A. (eds.) LPAR 2008. LNCS (LNAI), vol. 5330, pp. 243–257. Springer, Heidelberg (2008)
Allen, J.F.: Maintaining knowledge about temporal intervals. Communication of the ACM 26, 832–843 (1983)
Tsamardinos, I., Pollack, M.E.: Efficient solution techniques for disjunctive temporal reasoning problems. Artificial Intelligence 151, 43–89 (2003)
Peintner, B., Venable, K.B., Yorke-Smith, N.: Strong Controllability of Disjunctive Temporal Problems with Uncertainty. In: Bessière, C. (ed.) CP 2007. LNCS, vol. 4741, pp. 856–863. Springer, Heidelberg (2007)
Armando, A., Castellini, C., Giunchiglia, E.: SAT-Based Procedures for Temporal Reasoning. In: Biundo, S., Fox, M. (eds.) ECP 1999. LNCS, vol. 1809, pp. 97–108. Springer, Heidelberg (2000)
de la Tour, T.B.: Minimizing the Number of Clauses by Renaming. In: Stickel, M.E. (ed.) CADE 1990. LNCS, vol. 449, pp. 558–572. Springer, Heidelberg (1990)
Planken, L., de Weerdt, M., van der Krogt, R.: Computing all-pairs shortest paths by leveraging low treewidth. Journal of Artificial Intelligence Research (JAIR) 43, 353–388 (2012)
Venable, K.B., Volpato, M., Peintner, B., Yorke-Smith, N.: Weak and dynamic controllability of temporal problems with disjunctions and uncertainty. In: Workshop on Constraint Satisfaction Techniques for Planning & Scheduling, pp. 50–59 (2010)
Cimatti, A., Micheli, A., Roveri, M.: Solving Temporal Problems using SMT: Weak Controllability. In: Hoffmann, J., Selman, B. (eds.) American Association for Artificial Intelligence - AAAI. AAAI Press (2012)
Morris, P.H., Muscettola, N., Vidal, T.: Dynamic control of plans with temporal uncertainty. In: Nebel, B. (ed.) International Joint Conference on Artificial Intelligence - IJCAI, pp. 494–502. Morgan Kaufmann (2001)
Barrett, C., Deters, M., de Moura, L., Oliveras, A., Stump, A.: 6 Years of SMT-COMP. Journal of Automated Reasoning (to appear, 2012)
Cotton, S., Maler, O.: Fast and Flexible Difference Constraint Propagation for DPLL(T). In: Biere, A., Gomes, C.P. (eds.) SAT 2006. LNCS, vol. 4121, pp. 170–183. Springer, Heidelberg (2006)
Dutertre, B., de Moura, L.: A Fast Linear-Arithmetic Solver for DPLL(T). In: Ball, T., Jones, R.B. (eds.) CAV 2006. LNCS, vol. 4144, pp. 81–94. Springer, Heidelberg (2006)
Author information
Authors and Affiliations
Editor information
Editors and Affiliations
Rights and permissions
Copyright information
© 2012 Springer-Verlag Berlin Heidelberg
About this paper
Cite this paper
Cimatti, A., Micheli, A., Roveri, M. (2012). Solving Temporal Problems Using SMT: Strong Controllability. In: Milano, M. (eds) Principles and Practice of Constraint Programming. CP 2012. Lecture Notes in Computer Science, vol 7514. Springer, Berlin, Heidelberg. https://doi.org/10.1007/978-3-642-33558-7_20
Download citation
DOI: https://doi.org/10.1007/978-3-642-33558-7_20
Publisher Name: Springer, Berlin, Heidelberg
Print ISBN: 978-3-642-33557-0
Online ISBN: 978-3-642-33558-7
eBook Packages: Computer ScienceComputer Science (R0)