带求和算子的实数存在性理论
The Existential Theory of the Reals with Summation Operators
AI总结：
本文围绕实数存在性理论引入简洁类 succ-∃R，用非确定性实数 RAM 刻画该类并证明其与 ∃R 分离，同时确定若干逻辑与概率推理问题的完全性，并证明仅添加指数求和所得类 ∃R^Σ 包含于 PSPACE。
摘要：
为了刻画 Pearl 因果层级中概率推理与因果推理的可满足性问题的计算复杂度，arXiv:2305.09508 [cs.AI] 引入了一个新的自然类，称为 succ-∃R。该类可视为基于实数存在性理论（ETR）的、已被深入研究的类 ∃R 的简洁（succinct）变体。与 ∃R 类似，succ-∃R 是介于 NEXP 与 EXPSPACE 之间的中间类，其中 NEXP 和 EXPSPACE 分别是 NP 和 PSPACE 的指数版本。本文的主要贡献有三方面。第一，我们用非确定性实数 RAM 机器刻画 succ-∃R 类，并为实数 RAM 建立了结构复杂性理论结果，包括平移定理和层级定理。值得注意的是，我们证明了 ∃R 与 succ-∃R 的分离。第二，我们考察了存在性二阶逻辑片段和概率独立逻辑的模型检测与可满足性问题的复杂度。我们证明了其中若干问题是 succ-∃R-完全的，而此前这些问题已知的最优复杂度下界和上界分别为 NEXP-难和 EXPSPACE。第三，虽然 succ-∃R 是用普通（非简洁）ETR 实例加上指数求和以及一种可索引指数多个变量的机制来刻画的，但在本文中我们证明：当只添加指数求和时，相应的类 ∃R^Σ 包含于 PSPACE。我们猜想该包含关系是严格的，因为该类等价于向多项式时间非确定性实数 RAM 添加一个 VNP-谕示。反过来，向 ETR 添加指数乘积则得到 PSPACE。此外，我们研究了概率推理的可满足性问题，并附加了小模型要求，证明该问题对 ∃R^Σ 是完全的。
英文摘要：
To characterize the computational complexity of satisfiability problems for probabilistic and causal reasoning within the Pearl's Causal Hierarchy, arXiv:2305.09508 [cs.AI] introduce a new natural class, named succ-$\exists$R. This class can be viewed as a succinct variant of the well-studied class $\exists$R based on the Existential Theory of the Reals (ETR). Analogously to $\exists$R, succ-$\exists$R is an intermediate class between NEXP and EXPSPACE, the exponential versions of NP and PSPACE. The main contributions of this work are threefold. Firstly, we characterize the class succ-$\exists$R in terms of nondeterministic real RAM machines and develop structural complexity theoretic results for real RAMs, including translation and hierarchy theorems. Notably, we demonstrate the separation of $\exists$R and succ-$\exists$R. Secondly, we examine the complexity of model checking and satisfiability of fragments of existential second-order logic and probabilistic independence logic. We show succ-$\exists$R- completeness of several of these problems, for which the best-known complexity lower and upper bounds were previously NEXP-hardness and EXPSPACE, respectively. Thirdly, while succ-$\exists$R is characterized in terms of ordinary (non-succinct) ETR instances enriched by exponential sums and a mechanism to index exponentially many variables, in this paper, we prove that when only exponential sums are added, the corresponding class $\exists$R^Σ is contained in PSPACE. We conjecture that this inclusion is strict, as this class is equivalent to adding a VNP-oracle to a polynomial time nondeterministic real RAM. Conversely, the addition of exponential products to ETR, yields PSPACE. Additionally, we study the satisfiability problem for probabilistic reasoning, with the additional requirement of a small model and prove that this problem is complete for $\exists$R^Σ.
机构、总结、中文摘要均由AI分析而来，可能存在错误，请以论文正文为准。
