FMplex: A Novel Method for Solving Linear Real Arithmetic Problems

Jasper Nalbach
(RWTH Aachen University, Germany) 		Valentin Promies
(RWTH Aachen University, Germany) 		Erika Ábrahám
(RWTH Aachen University, Germany) 		Paul Kobialka
(University of Oslo, Norway)

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.

In Antonis Achilleos and Dario Della Monica: Proceedings of the Fourteenth International Symposium on Games, Automata, Logics, and Formal Verification (GandALF 2023), Udine, Italy, 18-20th September 2023, Electronic Proceedings in Theoretical Computer Science 390, pp. 16–32.
The extended version of this paper can be found at https://arxiv.org/abs/2309.03138.
Published: 30th September 2023.
ArXived at: https://dx.doi.org/10.4204/EPTCS.390.2 bibtex PDF
References in reconstructed bibtex, XML and HTML format (approximated).
Comments and questions to: eptcs@eptcs.org
For website issues: webmaster@eptcs.org