CircuitTSAT: a solver for large instances of the disjunctive temporal problem
Blaine A. Nelson, T. K. Satish Kumar · 2008
In this paper, we report on a new solver for large instances of the Disjunctive Temporal Problem (DTP). Our solver is based primarily on the idea of employing “compact ” circuit-based representations of disjunctive temporal constraints (akin to ripple-carry adders used in computer arithmetic operations). These circuit-based representations are in turn converted to CNF clauses of a SAT instance, and a powerful SAT solver is subsequently employed to efficiently solve the resulting SAT instance. We refer to this efficient DTP solver as “Cir-cuitTSAT. ” A thorough empirical evaluation of CircuitTSAT shows that it significantly outperforms TSAT++ and Yices on a wide range of DTP instances. We also comment on the gen-erality of our approach and its potential usefulness in dealing with more expressive constraints.