FMplex: A Novel Method for Solving Linear Real Arithmetic Problems
Jasper Nalbach (RWTH Aachen University, Germany), Valentin Promies, (RWTH Aachen University, Germany), Erika \'Abrah\'am (RWTH Aachen University,, Germany), Paul Kobialka (University of Oslo, Norway)
TL;DR
FMplex is a new quantifier elimination method for linear real arithmetic that reduces complexity and improves SMT solving efficiency by adapting Fourier-Motzkin elimination with case splitting.
Contribution
It introduces FMplex, a novel adaptation of Fourier-Motzkin elimination with case splitting, reducing complexity from doubly to singly exponential for SMT solving.
Findings
Reduces worst-case complexity from doubly to singly exponential.
Demonstrates effectiveness through experimental evaluation.
Aligns with the simplex algorithm for SMT solving.
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.
Peer Reviews
No public reviews on file for this paper yet. If you reviewed it on a platform where reviews are public (OpenReview, ICLR, NeurIPS, ICML), you can paste yours below so the community can read it here.
Videos
No videos yet. Explain this paper in a talk, walkthrough, or lecture? Add one.