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

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


This page is copyrighted by AAAI. All rights reserved. Your use of this site constitutes acceptance of all of AAAI's terms and conditions and privacy policy.