FMplex: Exploring a Bridge between Fourier-Motzkin and Simplex

TL;DR

FMplex introduces a novel quantifier elimination method for linear real arithmetic that reduces complexity by combining Fourier-Motzkin elimination with case splitting, closely relating to the simplex algorithm, and demonstrates practical effectiveness in SMT solving.

Contribution

The paper presents FMplex, a new algorithm that improves Fourier-Motzkin elimination by reducing complexity and aligning with the simplex method, with experimental validation in SMT contexts.

Findings

Reduces worst-case complexity from doubly to singly exponential.

Establishes strong correspondence between FMplex and the simplex algorithm.

Provides experimental evidence of effectiveness in SMT solving.

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).