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