Valentin Promies ; Jasper Nalbach ; Erika Ábrahám ; Paul Kobialka - FMplex: Exploring a Bridge between Fourier-Motzkin and Simplex

lmcs:13362 - Logical Methods in Computer Science, April 21, 2025, Volume 21, Issue 2 - https://doi.org/10.46298/lmcs-21(2:6)2025
FMplex: Exploring a Bridge between Fourier-Motzkin and SimplexArticle

Authors: Jasper Nalbach ; Valentin Promies ; Erika Ábrahám ; Paul Kobialka

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


    Volume: Volume 21, Issue 2
    Published on: April 21, 2025
    Accepted on: February 21, 2025
    Submitted on: April 8, 2024
    Keywords: Computer Science - Symbolic Computation

    Consultation statistics

    This page has been seen 363 times.
    This article's PDF has been downloaded 329 times.