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求解背景下提供了实验评估。