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.

翻译：本文提出了一种新的量词消去方法，用于处理线性实数算术约束的合取。我们的算法基于傅里叶-莫茨金变量消去过程，但通过情况分裂，能够将最坏情况复杂度从双指数降低为单指数。该过程在SMT求解中的适配与单纯形算法有紧密对应关系，因此我们将其命名为FMplex。除理论基础外，我们还提供了在SMT求解背景下的实验评估。