The Hardness of Reasoning about Probabilities and Causality

1 Introduction

Satisfiability problems play a key role in a broad range of research fields, including AI, since many real-life tasks can be reduced in a natural and efficient way to instances of satisfiability expressed in a suitable formal language. A prominent example is the Boolean satisfiability problem (SAT) whose instances represent Boolean formulas of propositional logic and ask whether there exists an assignment that satisfies a given formula. It is well known that any decision problem in the complexity class NP can be reduced in polynomial time to the SAT problem, see [Garey and Johnson, 1979].

In this work, we investigate satisfiability problems (and their validity counterparts) whose instance formulas allow expressing many tasks in probabilistic and causal inference. The formulas are specified in languages commonly used in pure probabilistic and interventional reasoning. In particular, the probabilistic language, called in Pearl's Causal Hierarchy 1 the associational one, consists of Boolean combinations of (in)equalities involving pure probabilities as, e.g., P(y|x)

1 See [Pearl and Mackenzie, 2018] for a first-time introduction to the topic.

which 2 can ask how likely is Y = y given that observing X = x? An example formula in this language is the following single equality

which expresses the fact that the joint distribution can be factorized as P(u, x, z, y) = P(u)P(x|u)P(z|x)P(y|z, u), for all values u, x, z, y. The causal language extends the probabilistic language by allowing additionally to use terms involving Pearl's do-operator [Pearl, 2009] as, e.g., P(y|do(x)) which can ask hypothetical questions such as how likely would Y = y be given an intervention setting X to x? An example formula in this language is the single equality

which allows estimating the (total) causal effect of the intervention X = x on outcome variable Y = y via the prominent front-door adjustment [Pearl, 1995]. It is well known that this formalism enables inference of properties that are impossible to reason about from correlational data using a purely probabilistic framework [Shpitser and Pearl, 2008; Bareinboim et al., 2022].

Similarly as in the classical SAT, both languages allow natural, polynomial-time reductions of many tasks in probabilistic and causal inference to the satisfiability (or validity) problems. Prominent examples can be establishing properties of structural causal models [Glymour et al., 2014; Pearl, 2009; Koller and Friedman, 2009; Elwert, 2013] which endow researchers with graphical structures (also called causal Bayesian networks) to encode conditional independences and causal assumptions as a directed acyclic graph (DAG). For instance, the problem to decide, for a given DAG G and variables X, Y,Z, whether in every structural causal model compatible with the structure G, the causal effect of X on Y can be inferred via front-door adjustment (2) can be reduced in polynomial time to the validity problem. Indeed, for any G,X, Y,Z, one can compute a formula φ whose size is bounded by a polynomial in the number of nodes of G, such that the front-door adjustment is applicable, if and only if, φ is valid. E.g., for the DAG G:

2 In our paper, by P(y|x), P(y|do(x)), etc., we mean P(Y=y|X=x), P(Y=y|do(X=x)), etc.

the formula φ looks as follows (ψ1 ∧ ψ2) ⇒ φfda, where φfda is the equality (2) representing the front-door adjustment, ψ1 is the equality (1) encoding the probability factorization, and ψ2 is a conjunction of equalities, whose conjuncts encode edge orientations. E.g., X → Z can be expressed as

The correctness of this reduction follows from the fact, that a structural causal model over X, Y, Z, U is supplemented with the above DAG G if ψ1 ∧ ψ2 encodes G. Interestingly, using do-calculus, one can prove that the front-door adjustment is applicable for the discussed instance which means that the formula (ψ1 ∧ ψ2) ⇒ φfda is valid.

1.1 Our Contribution

Despite its importance, computational complexity aspects of the satisfiability problems for the general probabilistic and causal languages remain unexplored. In our work, we investigate these issues and establish, for the first time, the exact computational complexity of the satisfiability problem for probabilistic languages, denoted as SATprob, and for the interventional level of the causal hierarchy, denoted as SATinterven. They simultaneously indicate the complexity of the validity problems for these languages.

Our results are based on a novel extension of the wellstudied complexity class ∃R which, loosely speaking, consists of problems that are polynomial time reducible to deciding whether a system of polynomial (in)equalities over real unknowns has a solution. The class ∃R includes, in an obvious way, NP and, what is highly nontrivial, it is contained in PSPACE [Grigoriev and Vorobjov, 1988; Canny, 1988; Schaefer, 2009]. However, none of the inclusions NP ⊆ ∃R ⊆ PSPACE are known to be strict. Our new complexity class, named succ∃R, can be viewed as a succinct variant of ∃R and it is an intermediate class between the exponential versions of NP and PSPACE:

The main contribution of this paper is to show that deciding the satisfiability of both probabilistic reasoning and reasoning about causal interventions is complete for succ∃R:

Theorem 1.1 (Main). The satisfiability problems SATprob and SATinterven are succ∃R-complete.

Since succ∃R contains all problems decidable in nondeterministic exponential time, this shows a significant jump in complexity compared to the classic SAT problem for propositional logic which is known to be NP-complete.

1.2 The Existential Theory of the Reals

The Existential Theory of the Reals (ETR) asks, given a Boolean combination of (in)equalities of multivariate polynomials, called a sentence, whether there exists an assignment of real numbers to the variables of the polynomials that satisfies the combination of (in)equalities? The example

illustrates a yes instance of ETR because (x, y) = (1, 1) is a solution of the sentence. The theory forms its own complexity class ∃R which is defined as the closure of the ETR under polynomial time many-one reductions. The importance of ∃R is underlined by the fact, that many meaningful problems including algebraic, geometric, graph- and game-theory, machine learning, and continuous constraint satisfaction problems, have been classified as complete for ∃R, see e.g. [Schaefer and ˇStefankoviˇc, 2017; Abrahamsen et al., 2018; Garg et al., 2018; Abrahamsen et al., 2021; Miltzow and Schmiermann, 2022]. Moreover, assuming NP ̸= ∃R which is widely believed, the ∃R-completeness of a problem reflects the limitation on the use of algorithmic approaches to solve the problem, as, e.g., dynamic programming, divide and conquer, tree-width based algorithms, or SAT-solver approaches which are applicable for instances of NP-complete problems. The succ∃R-completeness of SATprob and SATinterven (Theorem 1.1) imply even stronger algorithmic limitations than could be deduced from the ∃R-completeness results of [Moss´e et al., 2022] (discussed below) which concerns, however, some restricted variants of the languages.

1.3 Previous Work on the Hardness of Satisfiability Problems

In the past decades, several research groups have studied the computational complexity aspects of satisfiability problems for some limited languages of probabilistic and causal inference. In their pioneering work, Fagin et al. [1990] consider a language for reasoning about pure probabilities, which consists of Boolean combinations of linear (in)equalities over probabilities, like P(X=1 ∨ X=2) + 2P(Y=1) ≤ 1/3 ∧ P(Y=1) ≥ 2/3. The authors provide a complete axiomatization for the logic and show that the problem of deciding satisfiability is NP-complete which, surprisingly, is no worse than that of propositional logic. Later on, further studies explored the complexity aspects of probability logics [Abadi and Halpern, 1994; Speranski, 2013] and reasoning about causal models [Halpern, 2000; Eiter and Lukasiewicz, 2002; Aleksandrowicz et al., 2017].

Most germane to our work are the recent studies of Ibeling and Icard [2020] and Moss´e et al. [2022] which extended the formalism of [Fagin et al., 1990], providing the more expressive languages for the second (interventional) and third (counterfactual) level of Pearl's Causal Hierarchy. The languages consist of Boolean combinations of polynomial (in)equalities over pure probabilities or over probabilities involving the do-operator, respectively. In particular, they allow to express conditioning, as, e.g., P(y|x) = P(y, x)/P(x). But the languages limit the use of marginalization since the summation operator Σ over the domain of random variables, as used, e.g., in Eq. (1)-(3), is not allowed. Consequently, to express the marginal distribution of a variable Y over a subset of variables {Z1, . . . ,Zm} ⊆ {X1, . . . ,Xn}, as ∑z1,...,zm P(y, z1, . . . , zm), in the language without summation requires an extension P(y, Z1=0, . . . , Zm=0) + . . . + P(y,Z1=1, . . . ,Zm=1) of exponential size in m. (In the expression, we assume that the Zi are binary variables). Similarly, P(y|do(x)) = ∑z P(y|x, z)P(z) is expressed equivalently as P(y|do(x)) = P(y|x,Z=0)P(Z=0) +

P(y|x,Z=1)P(Z=1). While this might be acceptable for one variable Z, the expansion of the sums grows exponentially when we have several variables. Therefore, having an explicit summation operator is highly desirable.

Ibeling and Icard [2020] and Moss´e et al. [2022] give complete axiomatizations of these languages and investigate the computational complexity of the satisfiability problem for each language. In particular, they prove that, although the languages for interventional and counterfactual inference are more expressive than the ones for probabilistic reasoning, the computational complexities of the satisfiability problem for the logics are both ∃R-complete. Combining these results with ours, we obtain a precise complexity theoretic classification of the satisfiability problems for all three levels of Pearl's Causal Hierarchy combined with various languages for terms involving probabilities (proven by † : Fagin et al. [1990], ‡ : Moss´e et al. [2022]):

While the languages of [Moss´e et al., 2022] are capable of fully expressing quantitative probabilistic reasoning, respectively, do-calculus reasoning for causal effects, as discussed above, due to the lack of the summation operator Σ, they do not capture the standard notation used commonly in probabilistic and causal inference. Consequently, to analyze the computational complexity aspects of the inference, languages that exploit the standard notation need to be used. Indeed, for the computational complexity, the key issue is how the instances are represented since the time or space complexities are functions in the length of the input. For example, if the language as in [Moss´e et al., 2022] would be used (instead of the succinct one with summation operator), then the time complexity of many algorithms, including, e.g., the seminal Shpitser and Pearl [2006] algorithm to estimate the interventional distribution, would jump from polynomial to exponential. Another problem would also be to construct polynomial time reductions to the SAT problems since using the succinct encodings as, e.g., in Eq. (1)-(3), would not be allowed.

Structure of this Paper. The remainder of this work is dedicated to proving Theorem 1.1. After providing preliminaries (Sec. 2 and 3), we introduce the class succ∃R in Sec. 4 and provide the first complete problems for succ∃R in Sec. 5. In Sec. 6, we prove the membership of SATprob and SATinterven in the class succ∃R and their succ∃R-hardness. The omitted proofs can be found in the appendix of a companion paper [van der Zander et al., 2023].

2 Preliminaries

2.1 Syntax of Probabilistic and Causal Languages

The syntax used in this paper extends the definitions in [Ibeling and Icard, 2020; Moss´e et al., 2022] for the languages of the first two levels of Pearl's Causal Hierarchy. We consider discrete distributions and represent the values of the random variables as Val = {0, 1, . . . , c - 1} and denote by X the set of all (endogenous) random variables. By capital letters X1,X2,..., we denote the individual variables and assume, w.l.o.g., that they all share the same domain Val . A value of Xi is denoted by xi or a natural number.

In order to reason about the (in)equalities of arithmetic terms involving probability expressions, we need to define languages describing probabilities, languages describing arithmetic terms, and languages describing (in)equalities. The first languages characterize probabilistic and causal events as Boolean conditions over the values of (endogenous) random variables:

where X ∈ X, and x is either in Val or is a summation variable as defined below.

To make the notation more convenient for our analysis, we use [Lint] in the syntax above to describe an intervention on certain variables. The operator [·]δ creates a new post-intervention model and the assigned propositional formula δ only applies to the new model. Thus, for example, P([X=x]Y=y), which, using do-notation can be expressed as P(Y=y|do(X=x)), denotes the probability that the variable Y equals y in the model after the intervention do(X=x). Since ⊤ means that no intervention has been applied, we can assume that Lprop ⊆ Lpost-int.

Inserting the primitives into arithmetic expressions, we get the language T(L), where, for L ∈ {Lprop,Lpost-int}, δ ∈ L, and δ′ ∈ Lprop, any e ∈ T(L) is formed by the grammar 3 :

The probabilities of the form P(δ) or P(δ|δ′ ), are called primitives or (atomic) terms.

In the summation operator ∑x in definition (5), we have a dummy variable x which ranges over all values 0, 1,..., c-1. The summation ∑x e is a purely syntactical concept which represents the sum e[0/x] + e[1/x] + ... + e[c - 1/x], where, by e[v/x], we mean the expression in which all occurrences of x are replaced with value v. E.g., for Val = {0, 1}, the expression 4 ∑x P(Y=1,X=x) semantically represents P(Y=1,X=0) + P(Y=1,X=1). We note that the dummy variable x is not a (random) variable in the usual sense and that its scope is defined in the standard way.

Finally, we define the languages of Boolean combinations of inequalities, following the grammar, where e, e′ are expressions in T(Lprop) for prob and T(Lpost-int) for causal, respectively:

Together with conjunctions, the comparisons yield an equality relation. Moreover, for the atomic formula X=x in probabilities as, e. g. P(X=x), we use a common abbreviation P(x) if this does not lead to confusion. Thus, for example, Eq. (1) builds the correct formula in the language Lprob and Eq. (2) and (3) are the correct formulas in Linterven.

3 This is a recursive definition where, e.g., e + e′ means, for e, e′ ∈ T(L), the expression e + e′ is also in T(L).

4 As usually, P(Y =1, X=x), etc., means P(Y =1 ∧ X=x), etc.

Although the language and its operations can appear rather restricted, all the usual elements of probabilistic and causal formulas can be encoded. Namely, equality is encoded as greater-or-equal in both directions, e.g. P(x) = P(y) means P(x) ≥ P(y) ∧ P(y) ≥ P(x). Subtraction or divisions can be encoded by moving a term to the other side of the equation, e.g., P(x) - P(y) = P(z) means P(x) = P(z) + P(y), and P(x)/P(y) = P(z) means P(x) = P(z)P(y). Any positive integer can be encoded from the fact P(⊤) ≡ 1, e.g. 4 ≡ (1 + 1)(1 + 1) ≡ (P(⊤) + P(⊤))(P(⊤) + P(⊤)). The number 0 can be encoded as inconsistent probability, i.e., P(X=1 ∧ X=2). Note that these encodings barely change the size of the expressions, so allowing or disallowing these additional operators does not affect any complexity results involving these expressions.

2.2 Semantics

We define a structural causal model (SCM) as in [Pearl, 2009, Sec. 3.2]. An SCM is a tuple M = (F, P, U,X), such that V = U ∪ X is a set of variables partitioned into exogenous (unobserved) variables U = {U1, U2,...} and endogenous variables X. The tuple F = {F1,..., Fn} consists of functions such that function Fi calculates the value of variable Xi from the values (x, u) of other variables in V as Fi(xi1 ,..., xik , ui) 5 . P specifies a probability distribution of all exogenous variables U. Since variables X depend deterministically on the exogenous variables via functions Fi, F and P define the obvious joint probability distribution of X.

For any atomic Lint-formula Xi=xi (which, in our notation, means do(Xi=xi)), we denote by FXi=xi the functions obtained from F by replacing Fi with the constant function Fi(v) := xi. We generalize this definition for any interventions specified by α ∈ Lint in a natural way and denote as Fα the resulting functions.

For any φ ∈ Lprop, we write F, u |= φ if φ is satisfied for values of X calculated from the values u. For [α]φ ∈ Lpost-int, we write F, u |= [α]φ if Fα, u |= φ. Finally, for ψ ∈ Lpost-int, let SM(ψ) = {u | F, u |= ψ}. We assume, as is standard, the measurability of Mwhich guarantees that SM(ψ) is always measurable.

We define �e�M recursively in a natural way, starting with atomic terms as follows: �P(ψ)�M = P(SM(ψ)), resp. �P([α]φ|φ′ )�M = P (SM([α](φ∧φ′ )))/P (SM([α]φ′ )). For two expressions e1 and e2, we define M |= e1 ≤ e2, if and only if, �e1�M ≤ �e2�M. The semantics for negation and conjunction are defined in the usual way, giving the semantics for M |= φ for any formula.

2.3 Complexity Notation

We use the well-known complexity classes NP, PSPACE, NEXPTIME, EXPSPACE, and ∃R [Arora and Barak, 2009]. For two computational problems A, B, we will write A ≤p B if A can be reduced to B in polynomial time, which means A is not harder to solve than B. A problem A is complete for a complexity class C, if A ∈ C and, for every other problem B ∈ C, it holds B ≤p A. By co-C we denote the class of all problems A such that its complements A belong to C.

5 We consider recursive models, that is, we assume the endogenous variables are ordered such that variable Xi (i.e. function Fi) is not affected by any Xj with j > i.

3 Satisfiability Problems

The decision problems SATinterven and SATprob takes as input a formula φ in language Linterven and in Lprob, respectively, and asks whether there exists a model M such that M |= φ. Analogously, we define the validity problems for languages Linterven and Lprob of deciding whether, for a given φ, M |= φ holds for all models M. From the definitions, it is obvious that causal variants of the problems are at least as hard as the prob counterparts.

To give a first intuition about the expressive power of the SATprob problem, we prove the following result which shows that SATprob can encode any problem in NEXPTIME efficiently.

The remaining part of the paper is devoted to proving the main result (Theorem 1.1) showing that the satisfiability problems are complete for the new class succ∃R. Since a formula φ is not valid, if and only if ¬φ is satisfiable and ¬φ is in Lprob or in Linterven, respectively, we can conclude from Theorem 1.1:

Corollary 3.2. The validity problems for the languages Lprob and Linterven are complete for co-succ∃R, which is related to standard classes as follows: co-NEXPTIME ⊆ co-succ∃R ⊆ EXPSPACE .

4 The Existential Theory of the Reals, Succinctly

The existential theory of the reals ETR is the set of true sentences of the form∃x1 . . . ∃xnφ(x1, . . . , xn). (6)

φ is a quantifier-free Boolean formula over the basis {∨, ∧, ¬} and a signature consisting of the constants 0 and 1, the functional symbols + and ·, and the relational symbols <, ≤, and =. The sentence is interpreted over the real numbers in the standard way.

All operations have an arity of at most two, so we can represent φ as a binary tree. The leaves of the tree are labeled with variables or constants, the inner nodes are labeled with +, ·, =, <, ≤, ∧, ∨, or ¬. ¬-nodes have in-degree one, and all other inner nodes have in-degree two.

We now define succinct encodings of instances for ETR. Succinct encodings have been studied for problems in NP, see e.g. [Papadimitriou, 1994]. The input is now a Boolean circuit C computing a function {0, 1}N → {0, 1}M , which encodes the input instance. For example, an instance of the well-known 3-SAT problem is some standard encoding of a given 3-CNF formula. In the succinct version of 3-SAT, we are given a circuit C. C encodes a 3-CNF formula ψ in the following way: C(i) is an encoding of the ith clause of ψ. In this way, one can encode an exponentially large 3-SAT formula ψ (with up to 2N clauses) . The succinct encoding typically induces a complexity jump: The succinct version of the 3-SAT problem is NEXPTIME-complete. The same is true for many other NP-complete problems [Papadimitriou, 1994].

In the case of ETR, the formula φ is now given succinctly by a Boolean circuit C. The circuit C computes a function {0, 1}N → {0, 1}M . The input is (an encoding of) a node v of the formula and the output C(v) contains the label of the node as well as its parent and its children (encoded as a string in binary). In this way, we can represent a formula that is exponentially large in the size of the circuit.

Example 4.1. Consider the formula ∃x1 : x21 = 1 + 1 ("2 has a square root over the reals"). As an instance of ETR, this formula would be encoded as a binary string in some standard way. Figure 1 shows the binary tree underlying the formula. There are seven nodes, which we can represent as integers 1, . . . , 7. As a succETR instance, the formula will be given by a circuit C, computing a function {1, . . . , 7} → {=, +, ·, 0, 1, x1} × {0, 1, . . . , 7}3 describing the tree locally. For instance, C(1) = (=, 0, 2, 3), means the following: the label of the node 1 is =. It has no parent, that is, it is the root, which is indicated by giving 0 as the parent. The left child is 2 and the right child is 3. In the same way C(4) = (x1, 2, 0, 0), which means that the node 4 is a leaf with parent 2 and it is labeled with the variable x1. We can represent the integers ≤ 7 as bit strings of length N = 3 and the tuples C(i), e.g., (=, 0, 2, 3) or (x1, 2, 0, 0), can be encoded as bit strings of some length M. Thus, C can be considered a function C : {0, 1}N → {0, 1}M . Note that we cannot use more variables than the formula has nodes, thus to encode the tuple C(i), we need at most M ≤ (3 + N) + 3N bits: in the first entry, we need 3 +N bits to encode a label +, ·, =, <, ≤, ∧, ∨, and ¬ or an index j of a variable xj; to encode each of the remaining components, N bits suffice. It is clear that one can construct such a circuit C. When the formula is large but also structured, then the circuit C can be much smaller than the formula itself.

Definition 4.2 (succETR). succETR is the set of all Boolean circuits C that encode a true sentence φ as in (6) as follows. Assume that C computes a function {0, 1}N → {0, 1}M . Then {0, 1}N is the node set of the tree underlying φ and C(i) is the encoding of the description of node i, consisting of the label of i, its parent, and its two children. The variables in the formula are x1, . . . , x2N .

The number of variables is formally always a power of 2.

If we need fewer variables, we simply do not use them in the formula. We still quantify over all of them, but this is no problem. In the same way, the number of nodes is always a power of 2. If we need fewer nodes, we can define a special value for C(i), which marks node i as unused.

We will always assume that all negations are pushed to the lowest level of the formula and then they are absorbed in the arithmetic terms, i.e., ¬(s = t) becomes (s < t) ∨ (t < s), ¬(s < t) becomes t ≤ s and ¬(s ≤ t) becomes t < s. Furthermore, we can remove the comparisons ≤, since we can replace s ≤ t by (s < t) ∨ (s = t).

Remark 4.3. In the non-succinct case, eliminating the negations by pushing them to the bottom is no problem, as it can be done explicitly. In the succinct case, it seems that we need to assume that already the given input has this property.

Finally, based on the succETR problem, we define the succinct version of ∃R as follows:

Definition 4.4. succ∃R is the class of all problems that are polynomial time reducible to succETR.

succ∃R is related to known complexity classes as follows.

Theorem 4.5. NEXPTIME ⊆ succ∃R ⊆ EXPSPACE.

5 First Complete Problems for succ∃R

In this section, we present the first problems which are complete for succ∃R. The key role plays the problem Σvi-ETR which we need to prove the membership of SATinterven in the class succ∃R in Proposition 6.1.

QUAD is the problem to decide whether a given family of quadratic multivariate polynomials has a common root. Here the polynomials are given as lists of monomials. The coefficient is represented as a quotient of two integers. QUAD is a complete problem for the class ∃R of all problems that are reducible to ETR [Schaefer and ˇStefankoviˇc, 2017].

The succinct version succQUAD is defined as follows: We get a Boolean circuit C as input computing a function {0, 1}K × {0, 1}N → {0, 1}M . C(x, y) is an encoding of the yth monomial of the xth equation.

We allow that a monomial appears several times in these lists and the coefficients all add up, so the final polynomials are the sum of all monomials in the list.

Lemma 5.1. succETR ≤p succQUAD. Furthermore, the reduction only creates quadratic polynomials with at most four monomials and coefficients ±1.

Σvi-ETR is defined like ETR, but we add to the signature an additional summation operator. This is a unary operator ∑bxj=a . Consider an arithmetic term given by a tree with the top gate ∑bxj=a . Let t(x1, . . . , xn) be the term computed at the child of the top gate. Then the new term computes ∑be=a t(x1, . . . , xj-1, e, xj+1, . . . , xn), that is, we replace the variable xj by a summation variable e, which then runs from a to b.

Furthermore, we allow a new form of variable indexing in Σvi-ETR, namely variables of the form xn(xj1 ,...,xjm ): This can only be used when variables xj1 , . . . , xjm occur in the scope of summation operators and are replaced by summation variables e1, . . . , em with summation range {0, 1}.

xn(xj1 ,...,xjm ) is interpreted as the variable with index given by e1, . . . , em interpreted as a number in binary.

Instances of Σvi-ETR are not given succinctly by a circuit. However, the ability to write down exponential sums succinctly makes the problem as hard as succETR. We get

which yields:

Theorem 5.3. The problems succQUAD and Σvi-ETR are succ∃R-complete.

6 Proof of the Main Theorem

Equipped with the tools provided in the previous sections, we are ready to prove our main result (Theorem 1.1) by showing:

We first show the membership of SATprob in the class succ∃R proving the following reduction:

Proposition 6.1. SATinterven ≤p Σvi-ETR.

Due to the transitivity of ≤p and by Theorem 5.3, we get that SATinterven ≤p succETR. Moreover, since SATprob ≤p SATinterven, (7) follows.

For (8), it is sufficient to show the succ∃R-hardness of SATprob. We prove this in Proposition 6.5. To this aim, we introduce the problem succETR1/8,+,× [-1/8,1/8] and we prove the succ∃R-hardness of this problem.

Definition 6.2 (Abrahamsen et al., 2017). In the problem ETRc,+,×, where c ∈ R, we are given a set of real variables {x1,..., xn} and a set of equations of the form xi = c, xi1 + xi2 = xi3 , xi1 xi2 = xi3 , for i, i1, i2, i3 ∈ [n]. The goal is to decide whether the system of equations has a solution. The problem, where we also require that x1,..., xn ∈ [a, b], for some a, b ∈ R, is denoted by ETRc,+,× [a,b] .

Lemma 6.3 (Abrahamsen et al., 2017). ETR1,+,× and ETR1/8,+,× [-1/8,1/8] are ∃R-complete.

Let succETRc,+,× and succETRc,+,× [a,b] denote the succinct versions of ETRc,+,× and ETRc,+,× [a,b] , respectively. We assume that their instances are represented as seven Boolean circuits C0,C1,...,C6 : {0, 1}M → {0, 1}N such that C0(j) gives the index of the variables in the jth equation of type xi = 1/8, C1(j),C2(j),C3(j) give the indices of variables in the jth equation of the type xi1 + xi2 = xi3 , and C4(j),C5(j),C6(j) give the indices of variables in the jth equation of the type xi1 xi2 = xi3 . Without loss of generality, we can assume that an instance has the same number 2M of equations of each type; If not, one of the equations can be duplicated as many times as needed.

To establish the lemma, we first show that succQUAD ≤p succETR1,+,× and then prove that succETR1,+,× ≤p succETR1/8,+,× [-1/8,1/8] (see [van der Zander et al., 2023]).

Now we are ready to prove the succ∃R-hardness of SATprob through the following reduction:

Proof. Let us assume that the instance of succETR1/8,+,× [-1/8,1/8] is represented by seven Boolean circuits C0,C1,...,C6 : {0, 1}M → {0, 1}N as described above. Let the variables of the instance be indexed as xe1,...,eN , with ei ∈ {0, 1} for i ∈ [N]. Below, we often identify the bit sequence b1,..., bL by an integer j, with 0 ≤ j ≤ 2L - 1, the binary representation of which is b1...bL and vice versa.

The instance of the problem succETR1/8,+,× [-1/8,1/8] is satisfiable if and only if:

We construct a system of equations in the language Lprob and prove that there exists a model which satisfies the equations if and only if the formula (9) is satisfiable.

Let X0,X1,...,XN be binary random variables. We will model each real variable xe1,...,eN as a term involving the conditional probability P(X0=0 | X1=e1,...,XN=eN) as follows:

This guarantees that qe1,...,eN ∈ [-1/8, 1/8]. In our construction, the existential quantifiers in the formula (9) correspond to the existence of a probability distribution P(X0,X1,...,XN) which determines the values qe1,...,eN . This means that the formula (9) is satisfiable if and only if there exists a model for the equation:

The challenging task which remains to be solved is to express the terms qCi(j) in the language Lprob. Below we provide a system of equations that achieves this goal.

To model a Boolean formula encoded by a node of Ci, with i = 0, 1,..., 6, we use arithmetization to go from logical formulas to polynomials over terms involving probabilities of the form P(δ). We start with input nodes v ∈ {0, 1} and model them as events δv such that P(δv) = 1 if and only if v = 1. For every internal node v of Ci, we proceed as follows. If v is labeled with ¬ and u is a child of v, then we define an event δv such that P(δv) = 1 - P(δu). If v is labeled with ∧ and u and w are children of v, then we specify an event δv such that P(δv) = P(δu)P(δw). Finally, if v is labeled with ∨ and u and w are children of v, then P(δv) = 1 - (1 - P(δu))(1 - P(δw)). Thus, if v is an output node of a circuit Ci, then, for Ci fed with input j = b1...bM ∈ {0, 1}M , we have v = 1 if and only if P(δv) = 1. We define the events as follows.

Let ui,1,..., ui,M be the input nodes of Ci and let, for every node v of Ci, the sequence ℓv1 ,..., ℓvkv denotes the indices of the leaves ui,ℓv1 ,..., ui,ℓvkv of the sub-circuit with root v. Note that, for an input ui,k, the index ℓui,k 1 = k and kui,k = 1. To define the events, for every node v, we introduce a sequence of M new binary random variables Xv,1...,Xv,M and provide an equation that enforces the properties described above. The probabilities used in the equations involve, for a node v, only the variables indexed with ℓv1 ,..., ℓvkv ; The remaining variables are irrelevant.

For the kth input node ui,k and the variable Xui,k,k, we require

For every internal node v of Ci, if v is labeled with ¬ and u is a child of v, then we define the equation:

If v has label ∧ and w and z are children of v, then we define

where the indices jk, j ′k′ ∈ {1,...kv} are defined as jk := i for ℓwk = ℓvi and j ′k′ := i for ℓzk′ = ℓvi .

If v is labeled with ∨, we encode it as a negation of ∧ after negating the children of v.

Let ˆui,1,..., ˆui,N be the output nodes of Ci. For the kth output v = ˆui,k and for an Ci's input j = b1...bM, we denote by oi,k(j) the expression

which represents the value of the kth output bit of Ci(j) in such a way that the bit is equal to ek if and only if the probability oi,k(j) = ek. We illustrate this concept in Example 6.6. Finally, for i = 0, 1,..., 6 and j = b1...bM ∈ {0, 1}M , let

where E is a new binary random variable with P(E=0) = 0 and P(E=1) = 1. The crucial property of this encoding is that: For all i = 0, 1,..., 6 and j = b1...bM ∈ {0, 1}M , it is true that α(i, j) = qCi(j).

Now, we replace every term qCi(j) in the Eq. (10) by α(i, j) and get the following final equation in the language Lprob:

This completes the proof since it is true that the formula (9) is satisfiable if and only if there exists a model which satisfies Eq. (11)-(13) and Eq. (14). Obviously, the size of the resulting system of equations is polynomial in the size |C0| + |C1| +... + |C6| of the input instance and the system can be computed in polynomial time.

Example 6.6. Consider a Boolean circuit C with three input nodes u1, u2, u3, internal nodes v,w, and one output node ˆu as shown in Fig. 2. The relevant variables used to encode the output bit are: Xu1,1,Xu2,2,Xu3,3, assigned to the input nodes, as well as Xv,1,Xv,2 and Xw,2,Xw,3 and Xˆu,1,Xˆu,2,Xˆu,3, assigned to v, to w, and ˆu, respectively. Then, assuming the constraints expressed in Eq. (11)- (13) are satisfied, for any b1, b2, b3 ∈ {0, 1}, the probability o(j = b1b2b3) := P(Xˆu,1=b1,Xˆu,2=b2,Xˆu,3=b3) can be estimated as follows:

which is 0 if C(b1, b2, b3) = (b1 ∧ b2) ∧ (b2 ∨ b3) = 0, and it is equal to 1 if C(b1, b2, b3) = 1.

7 Discussion

We have analyzed the complexity of deciding whether a system of (in)equalities involving probabilistic and causal formulas is satisfiable using standard languages, allowing formulas with summations. We have shown that the problems are complete for a new complexity class succ∃R. Using these results, we could conclude that the complexity of the validity problem, asking whether a Boolean combination of (in)equalities involving pure probabilities and interventional expressions is valid, is complete for the class co-succ∃R.

Any ∃R-complete problem can probably be turned into a succ∃R-complete one by encoding the input succinctly. Although we do not know other published succ∃R-complete problems, the situation is similar to the relation of NP and NEXPTIME. The succinct versions of almost all NP-complete problems are NEXPTIME-complete. We think that succ∃R is so natural that further complete problems not coming from ∃R-complete ones will be found in the future.

Acknowledgments

This work was supported by the Deutsche Forschungsgemeinschaft (DFG) grant 471183316 (ZA 1244/1-1).

Contribution Statement

Markus Bl¨aser and Maciej Li´skiewicz are equally last authors.