一句话：提出 FMplex，用量词消去处理线性实数算术合取，通过分支将最坏复杂度从双指数降至单指数。
本文研究线性实数算术约束合取式的量词消去问题。作者以 Fourier-Motzkin 变量消去法为基础，引入情况分裂（case splitting），将最坏情况复杂度从双指数级降低到单指数级。该过程适配到 SMT 求解时与单纯形算法有强烈对应，因此称为 FMplex。除理论分析外，作者还在 SMT 求解场景中进行了实验评估。论文是作者此前发表于 GandALF 2023 工作的扩展版。
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).
DOI 原文 · arXiv · PDF（开放获取） · DBLP
@article{PromiesNAK25,
title = {FMplex: Exploring a Bridge between Fourier-Motzkin and Simplex},
author = {Valentin Promies and Jasper Nalbach and Erika Ábrahám and Paul Kobialka},
journal = {Logical Methods in Computer Science},
volume = {Volume 21, Issue 2},
year = {2025},
doi = {10.46298/lmcs-21(2:6)2025}
}