Satisfiability Checking with Difference Constraints

of difference constraints in the form x - y <= c.  In particular, we work
within the DPLL[T] framework for satisfiability checking modulo theories, and
present a novel theory solver for the theory of difference constraints.  In
applying the solver to both scheduling and circuit timing problems, we show
that using semi-lazy, incomplete constraint propogation significantly
outperforms methods which make use of either complete propogation or no
propogation.