FORMATS-FTRTFT 2004 START ConferenceManager    

Some Progress in Satisfiabilty Checking for Difference Logic

S. Cotton, E. Asarin, O. Maler and P. Niebert

Presented at Formal Modelling and Analysis of Timed Systems - Formal Techniques in Real-Time and Fault Tolerant System (FORMATS-FTRTFT 2004), Grenoble, France, September 22-24, 2004


In this paper we report a new SAT solver for difference logic, a propositional logic enriched with timing constraints. The main novelty of our solver is a tighter integration of the incremental analysis of numerical conflicts with the process of boolean conflict analysis. This and other imprvements lead to significant performance gains in some classes of problems.

START Conference Manager (V2.47.2)