Deciding Disjunctive Linear Arithmetic with SAT

Original · EN

Disjunctive Linear Arithmetic (DLA) is a major decidable theory that is supported by almost all existing theorem provers. The theory consists of Boolean combinations of predicates of the form Σⱼ₌₁ⁿaⱼ· xⱼ ≤ b, where the coefficients aⱼ, the bound b and the variables x₁ >... xₙ are of type Real (R). We show a reduction to propositional logic from disjunctive linear arithmetic based on Fourier-Motzkin elimination. While the complexity of this procedure is not better than competing techniques, it has practical advantages in solving verification problems. It also promotes the option of deciding a combination of theories by reducing them to this logic. Results from experiments show that this method has a strong advantage over existing techniques when there are many disjunctions in the formula.