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

翻译：本文提出了一种针对线性实数算术约束合取的量词消去方法。我们的算法基于傅里叶-莫茨金变量消去过程，但通过引入情况分割，成功将最坏情况复杂度从双重指数级降低至单指数级。该过程在适配SMT求解时与单纯形算法存在显著对应关系，故将其命名为FMplex。除理论基础的阐述外，我们还在SMT求解背景下进行了实验评估。本文是作者先前发表于第十四届博弈、自动机、逻辑与形式验证国际研讨会（GandALF 2023）工作的扩展版本。