FMplex: Exploring a Bridge between Fourier-Motzkin and Simplex

Logical Methods in Computer Science, vol. Volume 21, Issue 2

Abstract

In this paper we present a 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. This is an extended version of the authors' work previously published at the fourteenth International Symposium on Games, Automata, Logics, and Formal Verification (GandALF 2023).

Authors 4

1. Valentin Promies Aachen

   RWTH Aachen University

   Affiliation as printed

   RWTH Aachen University , Germany

2. Jasper Nalbach Aachen

   RWTH Aachen University

   Affiliation as printed

   RWTH Aachen University , Germany

3. Erika Ábrahám
   Affiliation as printed

   300 , San Francisco , CA 94105 , USA , or Eisenacher Strasse 2 , 10777 Berlin , Germany

4. Paul Kobialka

   University of Oslo

   Affiliation as printed

   University of Oslo , Norway