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）研究成果的扩展版本。