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.

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