Efficient DTPP solving with a reduction-based approach

Abstract

Disjunctive Temporal Problems with Preferences (DTPPs) extend DTPs with piece-wise constant preference functions associated to each constraint of the form l ≤ x − y ≤ u, where x, y are (real or integer) variables, and l, u are numeric constants. The goal is to find an assignment to the variables of the problem that maximizes the sum of the preference values of satisfied DTP constraints, where such values are obtained by aggregating the preference functions of the satisfied constraints in it under a “max” semantic. The state-of-the-art approach in the field, implemented in the DTPP solver MAXILITIS, extends the approach of the DTP solver EPILITIS. In this paper we present an alternative approach that reduces DTPPs to Maximum Satisfiability of a set of Boolean combination of constraints of the form $l \Join x-y \Join u$ , $\Join\in\{\lt,\le\}$ , that extends previous work that dealt with constant preference functions only. Results obtained with the Satisfiability Modulo Theories (SMT) solver YICES on randomly generated DTPPs show that our approach is competitive to, and can be faster than, MAXILITIS.