We study formal languages which are capable of fully expressing quantitative probabilistic reasoning and do-calculus reasoning for causal effects, from a computational complexity perspective. We focus on satisfiability problems whose instance formulas allow expressing many tasks in probabilistic and causal inference. The main contribution of this work is establishing the exact computational complexity of these satisfiability problems. We introduce a new natural complexity class, named succ$\exists$R, which can be viewed as a succinct variant of the well-studied class $\exists$R, and show that the problems we consider are complete for succ$\exists$R. Our results imply even stronger algorithmic limitations than were proven by Fagin, Halpern, and Megiddo (1990) and Moss\'{e}, Ibeling, and Icard (2022) for some variants of the standard languages used commonly in probabilistic and causal inference.

翻译：我们从计算复杂性的角度，研究能够完全表达定量概率推理及因果效应的do-演算推理的形式语言。重点关注可满足性问题，其实例公式能表达概率与因果推断中的许多任务。本文的主要贡献在于确定了这些可满足性问题的精确计算复杂性。我们引入了一个新的自然复杂性类，命名为succ$\exists$R，它可被视为已被充分研究的复杂性类$\exists$R的一种简洁变体，并证明了我们所考虑的问题对于succ$\exists$R是完全的。这一结果比Fagin, Halpern和Megiddo (1990)以及Mossé, Ibeling和Icard (2022)针对概率与因果推断中常用标准语言某些变体所证明的结论，揭示了更强的算法局限性。