Abstract:

Decision procedures for disjunctive linear arithmetic and restrictions of
this logic (e.g. Equality logic) are traditionally divided into two stages.
In the first stage, the formula is transformed into a set of clauses
('case-splitting'), each of which contains a conjunction of predicates. In
the second stage, each clause is solved separately with some (polynomial)
decision procedure. Since there may be an exponential number of cases,
case-splitting is the bottleneck of this method. In the last few years,
several procedures that avoid explicit case-splitting have been proposed,
most of which are based on graph algorithms.

The talk will begin with a survey of several of these methods and a
description of a related graph-theoretic open problem. It will then focus on
a reduction from disjunctive linear arithmetic to SAT, based on the
Fourier-Motzkin variable elimination technique.