Title
Solving strong controllability of temporal problems with uncertainty using SMT
Abstract
Temporal Problems (TPs) represent constraints over the timing of activities, as arising in many applications such as scheduling and temporal planning. A TP with uncertainty (TPU) is characterized by activities with uncontrollable duration. Different classes of TPU are possible, depending on the Boolean structure of the constraints: we have simple (STPU), constraint satisfaction (TCSPU), and disjunctive (DTPU) temporal problems with uncertainty. In this paper 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. Our approach casts the problem in the framework of Satisfiability Modulo Theory (SMT), where the uncertainty of durations can be modeled by means of universal quantifiers. The use of quantifier elimination techniques leads to quantifier-free encodings, which are in turn solved with efficient SMT solvers. We obtain the first practical and comprehensive solution for strong controllability. We provide a family of efficient encodings, that are able to exploit the specific structure of the problem. The approach has been implemented, and experimentally evaluated 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.
Year
DOI
Venue
2015
10.1007/s10601-014-9167-5
Constraints
Keywords
Field
DocType
Temporal problems,Strong controllability,Temporal reasoning under uncertainty,Satisfiability modulo theory
Quantifier elimination,Discrete mathematics,Constraint satisfaction,Mathematical optimization,Controllability,Scheduling (computing),Modulo,Satisfiability,Exploit,Mathematics
Journal
Volume
Issue
ISSN
20
1
1383-7133
Citations 
PageRank 
References 
17
0.70
29
Authors
3
Name
Order
Citations
PageRank
Alessandro Cimatti15064323.15
Andrea Micheli219014.08
Marco Roveri3167896.70