In this paper, we address the complexity barrier inherent in Fourier-Motzkin elimination (FME) and cylindrical algebraic decomposition (CAD) when eliminating a block of (existential) quantifiers. To mitigate this, we propose exploiting structural sparsity in the variable dependency graph of quantified formulas. Utilizing tools from parameterized algorithms, we investigate the role of treewidth, a parameter that measures the graph's tree-likeness, in the process of quantifier elimination. A novel dynamic programming framework, structured over a tree decomposition of the dependency graph, is developed for applying FME and CAD, and is also extensible to general quantifier elimination procedures. Crucially, we prove that when the treewidth is a constant, the framework achieves a significant exponential complexity improvement for both FME and CAD, reducing the worst-case complexity bound from doubly exponential to single exponential. Preliminary experiments on sparse linear real arithmetic (LRA) and nonlinear real arithmetic (NRA) benchmarks confirm that our algorithm outperforms the existing popular heuristic-based approaches on instances exhibiting low treewidth.

翻译：本文针对傅里叶-莫茨金消元（FME）与柱形代数分解（CAD）在消去一组（存在）量词时固有的复杂度障碍展开研究。为缓解此问题，我们提出利用量化公式变量依赖图中存在的结构稀疏性。借助参数化算法领域的工具，我们探究了树宽度——一种衡量图结构树状相似度的参数——在量词消解过程中的作用。我们开发了一种基于依赖图树分解结构的新型动态规划框架，用于实施FME与CAD方法，该框架亦可扩展至一般量词消解过程。关键性结论表明，当树宽度为常数时，该框架能为FME与CAD带来显著的指数级复杂度改进，将最坏情况复杂度界限从双重指数级降至单指数级。在稀疏线性实数算术（LRA）与非线性实数算术（NRA）基准测试上的初步实验证实，对于具有低树宽度特征的实例，我们的算法性能优于当前主流的启发式方法。