CircuitTSAT: A Solver for Large Instances of the Disjunctive Temporal Problem

All Papers

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 "CircuitTSAT." 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 generality of our approach and its potential usefulness in dealing with more expressive constraints.