Solving strong controllability of temporal problems with uncertainty using SMT

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.