In this paper, we present an algorithm for finding utilitarian optimal solutions to Simple and Disjunctive Temporal Problems
with Preferences (STPPs and DTPPs) based on Benders’ decomposition and adopting SAT techniques. In our approach, each temporal
constraint is replaced by a Boolean indicator variable and the decomposed problem is solved by a tightly integrated STP solver and SAT solver. Several hybridization techniques
that take advantage of each solver’s strengths are introduced. Finally, empirical evidence is presented to demonstrate the
effectiveness of our method compared to other algorithms.