An Interdisciplinary Experimental Evaluation on the Disjunctive Temporal Problem

We report on an extensive experimental evaluation on the Disjunctive Temporal Problem, where we adapted state-of-the-art Satisfiability Modulo Theories (SMT) encodings into the frameworks of Mixed Integer Linear Programming (MILP), (Circuit) Satisfiability (SAT), and Constraint Programming (CP). We considered 6 SMT solvers, 4 MILP solvers, 3 SAT solvers, and 3 CP solvers, broadly-recognized for their technologies. We compared all of them on several sets of benchmarks. As well as considering 2 random sets in the literature, we generated 3 new industrial and 3 new computationally-hard sets of benchmarks, which we make publicly available online. In particular, we analyzed 9885 instances, each processed on average about 33 times. Overall, SMT is confirmed to be the current best technology, but also MILP can perform very well, for instance on some random instances, on which it can be up to 2x faster than SMT. On a single machine, this experimental evaluation would have taken 598.97 days.