Search Results

Documents authored by van der Zander, Benito


Document
The Existential Theory of the Reals with Summation Operators

Authors: Markus Bläser, Julian Dörfler, Maciej Liśkiewicz, and Benito van der Zander

Published in: LIPIcs, Volume 322, 35th International Symposium on Algorithms and Computation (ISAAC 2024)


Abstract
To characterize the computational complexity of satisfiability problems for probabilistic and causal reasoning within Pearl’s Causal Hierarchy, van der Zander, Bläser, and Liśkiewicz [IJCAI 2023] introduce a new natural class, named succ-∃ℝ. This class can be viewed as a succinct variant of the well-studied class ∃ℝ based on the Existential Theory of the Reals (ETR). Analogously to ∃ℝ, succ-∃ℝ 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-∃ℝ in terms of nondeterministic real Random-Access Machines (RAMs) and develop structural complexity theoretic results for real RAMs, including translation and hierarchy theorems. Notably, we demonstrate the separation of ∃ℝ and succ-∃ℝ. Secondly, we examine the complexity of model checking and satisfiability of fragments of existential second-order logic and probabilistic independence logic. We show succ-∃ℝ-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-∃ℝ 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 ∃ℝ^Σ 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. Furthermore, we study the satisfiability problem for probabilistic reasoning, with the additional requirement of a small model, and prove that this problem is complete for ∃ℝ^Σ.

Cite as

Markus Bläser, Julian Dörfler, Maciej Liśkiewicz, and Benito van der Zander. The Existential Theory of the Reals with Summation Operators. In 35th International Symposium on Algorithms and Computation (ISAAC 2024). Leibniz International Proceedings in Informatics (LIPIcs), Volume 322, pp. 13:1-13:19, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2024)


Copy BibTex To Clipboard

@InProceedings{blaser_et_al:LIPIcs.ISAAC.2024.13,
  author =	{Bl\"{a}ser, Markus and D\"{o}rfler, Julian and Li\'{s}kiewicz, Maciej and van der Zander, Benito},
  title =	{{The Existential Theory of the Reals with Summation Operators}},
  booktitle =	{35th International Symposium on Algorithms and Computation (ISAAC 2024)},
  pages =	{13:1--13:19},
  series =	{Leibniz International Proceedings in Informatics (LIPIcs)},
  ISBN =	{978-3-95977-354-6},
  ISSN =	{1868-8969},
  year =	{2024},
  volume =	{322},
  editor =	{Mestre, Juli\'{a}n and Wirth, Anthony},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.ISAAC.2024.13},
  URN =		{urn:nbn:de:0030-drops-221407},
  doi =		{10.4230/LIPIcs.ISAAC.2024.13},
  annote =	{Keywords: Existential theory of the real numbers, Computational complexity, Probabilistic logic, Models of computation, Existential second order logic}
}
Questions / Remarks / Feedback
X

Feedback for Dagstuhl Publishing


Thanks for your feedback!

Feedback submitted

Could not send message

Please try again later or send an E-mail