Disjunctive temporal networks with uncertainty via SMT: Recent results and directions

Many Planning and Scheduling systems are designed assuming that the system under control is able to decide the duration of all the activities being executed. However, in many application scenarios this assumption is not acceptable because the actual timing of actions is not under direct control of the plan executor. Hence, new Planning and Scheduling techniques are needed to deal with this temporal uncertainty explicitly. In this paper, we summarize and systematize a series of works in which we addressed this uncertainty problem in the realm of temporal network scheduling. We show how Satisfiability Modulo Theory (SMT) solvers can be exploited to quickly solve different kinds of query in this setting. In particular, we focus on the framework of Disjunctive Temporal Networks with Uncertainty and address the three degrees of controllability for the fully-disjunctive class of problems, solving several open problems in the literature and experimentally showing the performance of the developed techniques. Finally, we outline and discuss several foreseeable directions of research in this field.