FMplex: A Novel Method for Solving Linear Real Arithmetic Problems

Electronic Proceedings in Theoretical Computer Science, vol. 390, pp. 16–32

Abstract

In this paper we introduce a novel quantifier elimination method for conjunctions of linear real arithmetic constraints.Our algorithm is based on the Fourier-Motzkin variable elimination procedure, but by case splitting we are able to reduce the worst-case complexity from doubly to singly exponential.The adaption of the procedure for SMT solving has strong correspondence to the simplex algorithm, therefore we name it FMplex.Besides the theoretical foundations, we provide an experimental evaluation in the context of SMT solving.

Authors 4

1. Jasper Nalbach Aachen

   University of Oslo · RWTH Aachen University

   Affiliation as printed

   RWTH Aachen University, Germany

   University of Oslo, Norway

2. Valentin Promies Aachen

   University of Oslo · RWTH Aachen University

   Affiliation as printed

   RWTH Aachen University, Germany

   University of Oslo, Norway

3. Erika Ábrahám Aachen

   University of Oslo · RWTH Aachen University

   Affiliation as printed

   RWTH Aachen University, Germany

   University of Oslo, Norway

4. Paul Kobialka Aachen

   University of Oslo · RWTH Aachen University

   Affiliation as printed

   University of Oslo, Norway

   RWTH Aachen University, Germany