DTP on Constraints

Finally the paper entitled “An interdisciplinary experimental evaluation on the disjunctive temporal problem” has been published on Constraints! We submitted it in July 2022, and it was accepted at the beginning of January 2023.

In this work, we considered state-of-the-art Satisfiability Modulo Theories (SMT) encodings of the Disjunctive Temporal Problem and we adapted into the frameworks of Mixed Integer Linear Programming (MILP), (Circuit) Satisfiability (SAT), and Constraint Programming (CP). To compare these approaches, we employed both commercial and open source solvers which broadly recognized or regularly compete in public challenges. We used several sets of benchmarks: two (random) available in the literature, and six (3 new industrial and 3 new computationally-hard) generated by us.

From the results, we could observe that:

• in general, CP and SAT are not the technologies to use;
• on random DTP instances, Gurobi and CPLEX, both with the Switch MILP Encoding, require 96% time less with respect to Yices with the SMT Naïve Encoding (i.e., they are 2x faster);
• on a set of computationally-hard instances, Gurobi with the MILP Switch Encoding with Bounded Domains outperforms MathSAT with the SMT Naïve encoding, by requiring 26.26% less time;
• however, MILP encodings need to be handled carefully in order to limit the magnitude of big-M and understand which cuts really help; also, MILP solvers suffer from numerical issues;
• on all other benchmark sets, except for fhcpcs-tcsp where all technologies failed within the timeout, SMT is confirmed to be the current best technology to tackle, in general, DTP and its special case of Temporal Constraint Satisfaction Problem; in particular, Yices is the most promising solver, to be used with the SMT Naïve Encoding and the SMT Hole Encoding when solving, respectively, DTP and TCSP;

In conclusion, at the time of writing this paper, the way to efficiently solve DTP/TCSP is SMT or MILP.

We hope that this evaluation, which puts together techniques and solvers from the areas of AI, Operations Research, and Theoretical Computer Science, will encourage further study and development of advanced techniques for DTP. For this reason, we make publicly available on a GitHub repository all new instances in order to foster future research.