SAT Solving Pratt's Difference Logic

difference constraints of the form x - y < c for numeric variables x and y,
constants c and constraints < or <=.  The satisfiability problem for difference
logic is recognized as an important class of constraints for many verification
systems, suitable for bounded model checking of timed automata, bounds checking
dynamic data structures such as stacks and queues, and determining
schedulability of job shop problems.

In this seminar we present an overview of techniques for SAT solving difference
logic.  In the course of this overview we will discuss methods in state of the
art boolean SAT solvers, variations on methods for determining satisfiability
of conjunctions of difference constraints, and also methods for translating DL
formula to propositional logic.  We will then present and evaluate various
ways of combining solutions to these problems to solve the DL satisfiability
problem.