Blaine Nelson, T. K. Satish Kumar
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.
Subjects: 3.6 Temporal Reasoning; 15.2 Constraint Satisfaction
Submitted: Jun 27, 2008