We present a method of determining the satisfiability of a Boolean combination
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.