Some Progress in Satisfiability Checking for Difference Logic

Abstract. 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 improvements lead to significant performance gains for some classes of problems.

• Type: Conference
• Year: 2004
• Where: FORMATS
• Authors: Scott Cotton, Eugene Asarin, Oded Maler, Peter Niebert
• Keywords: Boolean Conflict Analysis, Formal Methods, FORMATS 2004, Propositional Logic, Significant Performance Gains