Causal Explanations for Stratified Datalog

Causal Explanations for Stratified Datalog ∗ Ratan Bahadur Thapa1 † ,

arXiv:2608.21141v1 [cs.DB] 21 Aug 2026

1

Institute for Artificial Intelligence, University of Stuttgart, Germany 2 University of Southampton, United Kingdom

Abstract Rule-based reasoning with exceptions requires causal explanations that account for both present and absent facts. For positive Datalog, monotonicity allows minimal supports to determine deletion causality. Stratified negation removes that property because inserting or deleting a fact may create or destroy an answer. We study actual causes, responsibility, and robustness for safe and stratified Datalog under perfect-model semantics and interventions over a finite set of mutable extensional facts. We prove that minimal supports and inclusion-minimal outcome-changing interventions do not determine causality, while robustness radius one may coexist with unbounded minimum contingencies. Our main result characterizes the minimum contingency size of a candidate fact by compatible prime implicants for the observed and opposite outcomes. The characterization conservatively recovers support-based causality for positive Datalog and yields path–cut characterizations for blocked recursive reachability. For fixed nonrecursive stratified programs, we establish data-complexity NP-completeness for cause recognition, robustness, and responsibility, and coNP-completeness for intervention-response equivalence between two such programs.

1

Introduction

Rule-based systems often derive conclusions subject to exceptions. An eligibility decision may require a qualification and the absence of an exclusion; an access decision may hold unless a revocation is derived; and a diagnosis may remain valid unless a contraindication is established. Explaining such conclusions requires reasoning about both present and absent facts. Stratified datalog gives such rules a deterministic declarative semantics while retaining recursion and polynomial-time data evaluation (Abiteboul, Hull, and Vianu 1995; Apt, Blair, and Walker 1988). We study causal explanation for a ground conclusion over a finite set of mutable extensional facts. At an observed input, we ask which present or absent fact can become pivotal under a contingency, how strongly it is responsible, and how many changes are required to reverse the answer. To make these questions concrete, we begin with an example that introduces the relevant causal quantities. Consider ∗ †

Steffen Staab1,2

With Extended Proofs and Supplementary Results Corresponding Author: ratan.thapa@ki.uni-stuttgart.de

the Datalog program Πex approve(x) ← eligible(x), ¬blocked(x), blocked(x) ← violation(x), blocked(x) ← highRisk(x), ¬reviewed(x).

(⋆)

Let Dx = ∅, E = {highRisk(a)}, A = approve(a), and U = {eligible(a), violation(a), highRisk(a), reviewed(a)}, where Dx is the fixed extensional database whose facts cannot be changed, E is the observed mutable input, U is the finite set of mutable extensional facts that may be inserted or deleted, and A is the ground goal. An intervention J ⊆ U is applied by changing the membership in E of every atom in J. Thus, the intervention toggles every atom in J, inserting those absent from E and deleting those present in E. At E, the goal A is false. The singleton intervention J = {eligible(a)} leaves it false: since highRisk(a) is present and reviewed(a) is absent, the last rule derives blocked(a). Inserting reviewed(a) alone also leaves A false because eligibility is absent. However, inserting both reviewed(a) and eligible(a) makes A true, because eligibility and review are present and violation is absent. Thus, eligible(a) is an actual cause of the false outcome with a contingency Γ = {reviewed(a)} for that cause. The responsibility of a cause with minimum contingency size k is 1/(k + 1). Since the contingency Γ is minimum and |Γ| = 1, the responsibility of eligible(a) is 1/(|Γ| + 1) = 1/2. Robustness is the minimum size of an intervention that reverses the observed outcome. Therefore, the robustness value is 2 in this instance because the above intervention of size |J| = 2 makes A true, whereas no singleton intervention does. The program Πex also explains why absence conditions matter. The absence of eligible(a) at E is sufficient for the false outcome. The true outcome requires eligible(a) and the absence of violation(a), together with either the absence of highRisk(a) or the presence of reviewed(a). The false and true conditions disagree on the value of eligible(a). Once this atom is treated as the candidate cause, either deleting highRisk(a) or inserting reviewed(a) before toggling it yields a minimum contingency of size one. To illustrate deletionbased causality, consider instead E ′ = {eligible(a), highRisk(a), reviewed(a)}. Then, approve(a) holds under Πex at the alternative observed state E ′ . A fact in the observed state is a deletion cause if

deleting it reverses the outcome, possibly after a contingency that alone preserves the outcome. Deleting reviewed(a) activates the blocking rule and therefore makes the approval false. Thus, in the alternative observed state E ′ , reviewed(a) is a deletion cause with the empty contingency Γ = ∅. This nonmonotonic behavior shows why the positiveDatalog support representation does not extend to stratified negation. A minimal support is an inclusion-minimal set of mutable facts deriving an answer; by monotonicity, an answer holds exactly when its input contains one. In the deletionbased causality, the resulting support hypergraph determines deletion causes, responsibility, and robustness (Thapa and Staab 2026). Under stratified negation, minimal supports omit necessary absences, and inclusion-minimal outcomechanging interventions can omit atoms pivotal only at states farther from the observation. We prove that neither representation determines actual causes or responsibilities and that a robustness radius of one can coexist with unbounded minimum contingencies. Database causality defines actual causes, contingencies, and responsibility for query answers and non-answers (Meliou et al. 2010a,b), while prime implicants encode inclusionminimal partial assignments forcing a Boolean outcome (Darwiche and Ji 2022; Dubslaff et al. 2022). Featurecausality accounts minimize simultaneous changes containing the candidate without requiring the remaining changes alone to preserve the observed outcome. We instead pair compatible observed- and opposite-outcome implicants containing complementary candidate literals. Compatibility enforces this intermediate-state condition, and minimum pair cost gives the minimum contingency size for every finite Boolean response. For stratified Datalog, we construct both prime families compositionally through stratum-wise perfect-model evaluation. For blocked recursive reachability, we derive path–cut pairs and an exact responsibility formula. Our contributions are as follows: (i) in Section 4, we prove that minimal supports and inclusion-minimal outcomechanging interventions do not determine causality, establish an unbounded separation between robustness and minimum contingency size, and prove the compatible prime-pair characterization and its positive Datalog specialization; (ii) in Section 5, we derive the recursive path–cut characterization and exact responsibility formula, and show that explicit prime families may be exponential although the corresponding causal quantities remain polynomial-time computable; and (iii) in Section 6, we establish data-complexity bounds for fixed programs and goal predicates, with the databaselevel objects supplied as input.

2

Related Work

Database causality studies causes, contingencies, and responsibility for answers and non-answers (Meliou et al. 2010a,b; Bertossi and Salimi 2017). For conjunctive queries, answer causality typically deletes present tuples, whereas nonanswer causality inserts missing tuples. We allow both operations at one observed state in recursive stratified programs. Closely related work uses minimal supports and transversals to characterize deletion-based causality, responsibility, and robustness for positive recursive Datalog (Thapa and Staab

2026). Corollary 2 recovers those positive- Datalog characterizations from compatible prime implicants. Resilience and deletion propagation also study minimum deletions for monotone queries (Freire et al. 2015; Buneman, Khanna, and Tan 2002). Responsibility measures for conjunctive queries with negation include weighted sums of minimal supports (Bienvenu, Figueira, and Lafourcade 2026). We instead study pivotality under arbitrary contingencies and mixed interventions, including recursion. Theorem 1 shows that minimal supports do not determine the minimum contingency size of a designated atom. Provenance games and graphs represent successful and failed rule applications under negation (Köhler, Ludäscher, and Zinn 2013; Lee et al. 2017). Semiring approaches represent recursive derivations and input annotations (Deutch et al. 2014; Bourgaux et al. 2022; Grädel and Tannen 2025; Zhao et al. 2024). Prime implicants instead capture minimal partial assignments forcing the semantic outcome. Prime implicants also characterize sufficient reasons and feature explanations (Darwiche and Ji 2022; Dubslaff et al. 2022). Existing feature accounts minimize sets of features changed simultaneously, including the candidate. Our contingency semantics additionally requires that changing only the noncandidate atoms in the set preserves the observed outcome before the candidate is toggled. Compatible prime pairs enforce this intermediate-state requirement. Unlike structural-model and causal probabilistic approaches (Halpern and Pearl 2005; Chockler and Halpern 2004; Vennekens 2011), we treat the program as a deterministic specification, intervene on extensional atoms, and evaluate the goal in its perfect model.

3

Datalog and Interventions

Let ΣE and ΣI be disjoint finite signatures of extensional and intensional predicates, respectively, each with fixed arity. We allow nullary predicates and use nullary ΣI predicates as Boolean goals. A safe Datalog rule with negation has the form H ← B1 , . . . , Bm , ¬C1 , . . . , ¬Cn , where H is the ΣI head atom, the Bi are positive body atoms, the ¬Cj are negative body literals, each Bi and Cj is an ΣE - or ΣI -atom, and every variable in H and Cj occurs in some Bi . A finite Datalog program Π is stratified if some map λ : ΣE ∪ ΣI → N, with λ(S) = 0 for every S ∈ ΣE , satisfies λ(S) ≤ λ(R) whenever a rule with head predicate R contains a positive body atom with predicate S, and λ(S) < λ(R) whenever it contains a negative body literal with predicate S. Stratum-wise least-fixpoint evaluation yields the unique perfect model P(Π ∪ D) for every finite ΣE -database D (Apt, Blair, and Walker 1988; Abiteboul, Hull, and Vianu 1995). We call Π safe and stratified if every rule in Π is safe and Π is stratified. Definition 1. An intervention instance is a tuple I = (Π, Dx , U, E, A), where Π is a safe stratified program, Dx is a finite exogenous ΣE -database, U is a finite set of mutable ground ΣE -atoms

disjoint from Dx , E ⊆ U is the distinguished observed state, and A is a ground ΣI -atom. Any F ⊆ U is a state and represents exactly the mutable atoms present as facts, and we write  1, A ∈ P(Π ∪ Dx ∪ F ), (1) ansI (F ) = 0, A ∈ / P(Π ∪ Dx ∪ F ). x

The active domain contains the constants in Π, D , U, and A. We omit the subscript I when the instance is understood. For an intervention J ⊆ U and a state F ⊆ U , applying J yields F △ J = (F \ J) ∪ (J \ F ). Each atom in J is toggled: atoms in F ∩ J are deleted, and atoms in J \ F are inserted. The finite domain U specifies the admissible interventions. Example 1. Consider the program Πex in (⋆). Let U = {eligible(a), violation(a), highRisk(a), reviewed(a)}, E = {highRisk(a)} and A = approve(a), and let Iex = (Πex , ∅, U , E, A). Since eligible(a) ∈ / E, we have ansIex (E) = 0. Let J = {reviewed(a)}. Applying J to the observed state gives F = E △ J = {highRisk(a), reviewed(a)}. Since eligible(a) ∈ / F , the answer remains false: ansIex (F ) = 0. Now let J ′ = {eligible(a)}. Applying J ′ to F gives F △ J ′ = {eligible(a), highRisk(a), reviewed(a)}. In this state, eligible(a) and reviewed(a) hold, whereas violation(a) does not hold. Thus, ansIex (F △J ′ ) = 1. Hence, the additional intervention J ′ changes the answer from false to true. Definition 2. Let b = ans(E) and τ ∈ U , where b ∈ {0, 1} is the observed outcome at E. The mutable atom τ is an actual cause of outcome b at E if some contingency Γ ⊆ U \ {τ } satisfies ans(E △ Γ) = b and ans(E △ (Γ ∪ {τ })) = 1 − b. (2) It is counterfactual if Γ = ∅ satisfies (2). Let κE (τ ) be the minimum contingency size, with value ∞ when none exists, and let the responsibility of τ at E  1/(κE (τ ) + 1), κE (τ ) < ∞, RespE (τ ) = (3) 0, κE (τ ) = ∞. The robustness radius is Rob(E) = min{ |J| | ans(E △ J) = 1 − b },

(4)

with value ∞ when ans is constant. Every quantity is relative to U: enlarging the mutable domain may introduce new contingencies. We therefore compare programs only over a common intervention domain.

4

Causal Representation

We first prove that support-based summaries lose contingency information under negation. We then state the Boolean representation needed for the exact causal characterization.

For S ⊆ U, we call S a positive support if ans(S) = 1, and minimal if no proper subset has outcome 1. Let SuppI be the family of minimal supports. For the observed state E, let FlipI (E) = Min⊆ {J ⊆ U | ansI (E △ J) ̸= ansI (E)}, where Min⊆ selects the inclusion-minimal members. Theorem 1. There are intervention instances I1 and I2 with fixed nonrecursive stratified programs and common (Dx , U, E, A) such that SuppI1 = SuppI2 and FlipI1 (E) = FlipI2 (E), but their actual-cause families and responsibilities at E differ. Example 2. Let p = P (c), q = Q(c), and r = R(c). Consider Dx = ∅, U = {p, q, r}, E = ∅, A = Goal and the response functions f1 , f2 : 2U → {0, 1} f1 (F ) = 1 ⇐⇒ p ∈ F ∧ (q ∈ F ⇐⇒ r ∈ F ), f2 (F ) = 1 ⇐⇒ p ∈ F.

(5)

Then, the following program Π1 computes the first response: Goal Goal

← ←

P (c), ¬Q(c), ¬R(c), P (c), Q(c), R(c).

(6)

Let Π2 = {Goal ← P (c)} and Ij = (Πj , Dx , U, E, A) for j ∈ {1, 2}. The program Π2 computes f2 (F ). Both have the unique minimal support {p} and FlipI (E) = {{p}}. In the Π1 , however, q and r are causes with contingencies {p, r} and {p, q}, respectively, and each has responsibility 1/3. The response f2 is independent of q and r. Thus, supports and all inclusion-minimal interventions do not determine contingency causality. The separation persists at unbounded contingency distance. Theorem 2. There is a fixed nonrecursive stratified program such that, for every n ≥ 2, an intervention instance of size O(n) has observed outcome 0, robustness radius 1, one inclusion-minimal outcome-changing intervention, and n further actual causes, each with minimum contingency size n and responsibility 1/(n + 1). Example 3. Let a1 , . . . , an be exogenous items, let g be a mutable gate, and let si = Sel(ai ) be mutable selections, and let S = {s1 , . . . , sn }. The fixed program is Some ← Item(x), Sel(x), Missing ← Item(x), ¬Sel(x), None ← ¬Some, All ← ¬Missing, Goal ← g, None, Goal ← g, All.

(7)

For every mutable state F , perfect-model evaluation gives ans(F ) = 1 ⇐⇒ g ∈ F ∧ F ∩ S ∈ {∅, S}. At E = ∅, toggling g alone derives the goal through None, so Rob(E) = 1 and {g} is the unique inclusionminimal outcome-changing intervention. For si , the contingency {g} ∪ {sj | j ̸= i} produces a mixed selection and preserves outcome 0; toggling si makes every item selected and derives the goal through All. Any pivotal state for si must contain the gate and every other selection, proving minimum

size n. Thus, a unit robustness radius and a unique inclusionminimal outcome-changing intervention provide no bound on the contingency size of another cause; the corresponding nonzero responsibility tends to zero. In particular, for every ε > 0 there is such an instance with Rob(E) = 1, one inclusion-minimal outcome-changing intervention, and a cause of responsibility below ε. A term over U isVa pair C V = (P, N ) of disjoint subsets of U. It represents τ ∈P τ ∧ τ ∈N ¬τ : a member τ ∈ P represents the positive Boolean literal τ , and a member τ ∈ N represents the negative Boolean literal ¬τ . A state F satisfies C, written F |= C, if P ⊆ F and N ∩ F = ∅. We write (P ′ , N ′ ) ⪯ (P, N ) if P ′ ⊆ P and N ′ ⊆ N . For τ ∈ U, let ℓE (τ ) = τ if τ ∈ E and ℓE (τ ) = ¬τ otherwise; let ℓcE (τ ) denote its complementary literal. Definition 3. For b ∈ {0, 1}, a term C is a b-implicant if ∀F ⊆ U , F |= C =⇒ ans(F ) = b. It is prime if no proper subterm is a b-implicant. The family of all prime b-implicants is denoted by PrimebI . We also call prime 1-implicants prime truth conditions and prime 0-implicants prime falsity conditions. For the rule Goal ← P (c), ¬Q(c), the unique prime truth condition is ({P (c)}, {Q(c)}), while the prime falsity conditions are (∅, {P (c)}) and ({Q(c)}, ∅). Thus, negative and positive literals necessary for truth and falsity, respectively. Two terms conflict if one contains a literal and the other contains its complement; otherwise, they are compatible. For a term family C, let Dual(C) contain the ⪯-minimal terms that conflict with every member of C. The following finite Boolean fact is standard (Crama and Hammer 2011). Proposition 1. For every state F ⊆ U and b ∈ {0, 1}, ans(F ) = b ⇐⇒ ∃C ∈ PrimebI (F |= C), Prime1−b = Dual(PrimebI ). I

(8)

(9) Theorem 2 has an exact prime representation. Its two prime truth conditions are Cnone = ({g}, S) and Call = ({g} ∪ S, ∅), and its prime falsity conditions are (∅, {g}) and ({si }, {sj }) (i ̸= j). The first falsity term closes the gate; every other falsity term forces a mixed selection. At E = ∅, choose i ̸= j. The literal ℓE (si ) = ¬si occurs in ({sj }, {si }), whereas Call contains its complementary literal si . Replacing si by ¬si in Call and merging the terms requires g and all sj with j ̸= i. Their distance from E is n, recovering the minimum contingency in Theorem 2. Thus, the opposite-prime pairing captures a cause that neither minimal truth conditions at the observed state nor nearest outcome changes retain. Prime families admit a finite compositional iteration, although the explicit term families may be exponential. For a ground intensional atom H, let PrimebI (H) denote the prime b-implicants of its Boolean response. Let mi be the number of ground intensional atoms in stratum i. Proposition 2. For every stratum i and every ground intensional atom H in that stratum, the simultaneous prime-family iteration reaches (Prime1I (H), Prime0I (H)) after at most mi stages.

The proposition is a supporting construction rather than the causal characterization: it establishes that the semantic prime families can be obtained from stratified evaluation, while Theorem 3 identifies the information needed for minimum contingencies. For brevity, let e = eligible(a), v = violation(a), h = highRisk(a), and r = reviewed(a). For Iex from Example 1, direct minimization gives  Prime1Iex (approve(a)) = ({e}, {v, h}), ({e, r}, {v}) ,  Prime0Iex (approve(a)) = (∅, {e}), ({v}, ∅), ({h}, {r}) . (10) The terms describe semantic input conditions rather than particular rule derivations. For a term C = (P, N ), let dE (C) = |P \ E| + |N ∩ E|. (11) The value is the number of literals of C not satisfied by E, equivalently the minimum number of toggles required to reach a state satisfying C. Let C τ replace the literal on τ by its complement when C contains a literal on τ . For compatible terms, let (P, N ) ⊔ (P ′ , N ′ ) = (P ∪ ′ P , N ∪ N ′ ). We write dE,−τ (P, N ) = |(P \ E) \ {τ }| + |(N ∩ E) \ {τ }|. The minimum of an empty family is ∞. Let QbE,τ contain all pairs (C, D) ∈ PrimebI × Prime1−b such that C contains I ℓE (τ ), D contains ℓcE (τ ), and C is compatible with Dτ . Let KE (τ ) = min dE,−τ (C ⊔ Dτ ), (12) (C,D)∈QbE,τ

Theorem 3. Let b = ans(E) and τ ∈ U. 1. The mutable atom τ is an actual cause at E iff some C ∈ PrimebI contains ℓE (τ ). 2. κE (τ ) = KE (τ ). The responsibility is RespE (τ ) = 1/(KE (τ ) + 1) when KE (τ ) < ∞, and RespE (τ ) = 0 otherwise. 3. (13) Rob(E) = min dE (D). D∈Prime1−b I

Item (2) is the central representation result. For the upper bound, take C, D from QbE,τ and toggle exactly the noncandidate atoms whose literals in C ⊔ Dτ are not satisfied by E. The resulting state satisfies C, retains outcome b, and its τ -neighbour satisfies D, with outcome 1 − b. For the lower bound, let Γ be a minimum contingency. By Equation (8), choose a prime b-implicant C satisfied by E △ Γ and a prime (1 − b)-implicant D satisfied by the adjacent state. The terms contain complementary literals on τ , are compatible after replacing the literal on τ in D by its complement, and contain at most |Γ| literals outside τ that are not satisfied by E. Both inequalities yield KE (τ ) = κE (τ ). The cause and robustness clauses use the same adjacent-state construction. The compatible current-outcome term in Equation (12) is essential. Let opp δE (τ ) = min{dE,−τ (D) | D ∈ Prime1−b , I (14) c D contains ℓE (τ )}. The quantity considers only a nearest opposite-outcome condition.

Proposition 3. There is a fixed nonrecursive stratified program and an intervention instance with an actual cause τ opp such that δE (τ ) = 1 but κE (τ ) = 2. Example 4. Let U = {p, q, r}, E = {p, r} (abbreviations as in Eq. 5), and let Π3 be the fixed program containing Goal Goal

← ←

¬P (c), ¬R(c), ¬Q(c), ¬R(c),

(15)

Let I3 = (Π3 , ∅, U , E, Goal). Its response is ¬r ∧ (¬p ∨ ¬q). The prime falsity conditions are ({r}, ∅) and ({p, q}, ∅), and the prime truth conditions are (∅, {p, r}) and (∅, {q, r}). For candidate atom p, the nearest opposite condition (∅, {p, r}) contains outside p only the literal ¬r, which is not satisfied by opp E; thus δE (p) = 1. Toggling only r, however, reaches {p}, where the outcome is already true. The contingency {q, r} reaches {p, q}, where the outcome remains false, and toggling p reaches {q}, where it becomes true. Neither singleton contingency works; therefore, κE (p) = 2. The compatible pair ({p, q}, ∅) and (∅, {p, r}) recovers the two required contingency changes. Thus, nearest opposite conditions alone do not determine responsibility. For Π1 from Example 2, at E = ∅, pairing the prime 0-implicant ({q}, {r}), which contains ℓE (r) = ¬r, with the prime 1-implicant ({p, q, r}, ∅) yields the compatible term ({p, q}, {r}). Equation (12) then gives κE (r) = 2 and RespE (r) = 1/3, although {p} is the only inclusionminimal outcome-changing intervention. The preceding examples derive causal quantities from compatible prime implicants, however, these quantities do not determine the full intervention response at one observed state. We write 1[φ] for the indicator of φ. Let U = {p, q, r} and E = {p}. The responses 1. f1 (F ) = 1[p ∈ F ] and 2. f2 (F ) = 1[p ∈ F or {q, r} ⊆ F ] have the same sole cause p, with responsibility 1, and robustness radius 1 at E, but disagree at F = {q, r}. Let I = (Π, Dx , U, E, A) and I ′ = (Π′ , Dx , U, E, A) be instances that differ only in their programs. We call the replacement of Π by Π′ intervention-preserving if ansI (F ) = ansI ′ (F ) for every F ⊆ U . Corollary 1. The replacement is intervention-preserving iff Prime1I = Prime1I ′ , and equivalently iff Prime0I = Prime0I ′ . Corollary 2 recovers the positive-Datalog support characterization (Thapa and Staab 2026). For a family S ⊆ 2U , let Tr(S) = Min⊆ {T ⊆ U | ∀S ∈ S, T ∩ S ̸= ∅}. We use Tr(∅) = {∅} and Tr(S) = ∅ when ∅ ∈ S. Corollary 2. If Π is positive, then Prime1I = {(S, ∅) | S ∈ SuppI }, Prime0I = {(∅, T ) | T ∈ Tr(SuppI )}.

(16)

At E = U , Theorem 3 therefore gives the positive-Datalog characterizations of causes, responsibility, and deletion robustness.

5

Blocked Reachability

We now derive a recursion-specific theory in which the two prime families have distinct graph meanings. Consider the fixed stratified program Πbr : Path(x, y) ← Edge(x, y), ¬Block(x, y), Path(x, y) ← Edge(x, z), ¬Block(x, z), Path(z, y). (17) Let H = (V, L) be a finite simple directed graph of potential edges. Let s, t ∈ V be distinct. A potential path is a nonempty simple directed s-t path in H, written π : s ⇝ t. An edge cut is a set K ⊆ L meeting every potential path; K = ∅ is permitted. For e = (u, v) ∈ L, write Ee = Edge(u, v) and Be = Block(u, v), and let UH = {Ee , Be | e ∈ L}. For E ⊆ UH , consider IH,E = (Πbr , ∅, UH , E, Path(s, t)). Let LF = {e ∈ L | Ee ∈ F and Be ∈ / F }. An edge is active in state F exactly when it belongs to LF , and HF = (V, LF ) is the active graph. Presence of Ee and absence of Be enable e; absence of Ee and presence of Be disable e. For a potential path π, let Cπ = ({Ee | e ∈ π}, {Be | e ∈ π}). For an inclusion-minimal directed s-t edge cut K, let α : K → {edge, block} select one disabling literal for each cut edge. We call the pair (K, α) a mode-labelled cut, and let D(K,α) = ({Be | e ∈ K, α(e) = block}, {Ee | e ∈ K, α(e) = edge}). For a state E whose active graph contains a directed s-t path, let λHE (s, t) denote the minimum size of a directed s-t edge cut in HE . Theorem 4. For every finite simple directed graph H = (V, L), every pair of distinct vertices s, t ∈ V , and every state E ⊆ UH , the associated blocked-reachability instance IH,E satisfies: 1. the prime 1-implicants are exactly the terms Cπ ; 2. the prime 0-implicants are exactly the terms D(K,α) ; 3. if HE contains an s-t path, then Rob(E) = λHE (s, t),

(18)

4. if HE contains no s-t path, then X
Rob(E) = min 1[Ee ∈ / E] + 1[Be ∈ E] , (19) π:s⇝t

e∈π

where the minimum of an empty path family is ∞; 5. if ans(E) = 1, then Ee is a cause exactly when Ee ∈ E and e lies on a potential s-t path, and Be is a cause exactly when Be ∈ / E and e lies on such a path; if ans(E) = 0, then Ee is a cause exactly when Ee ∈ / E and e lies on a potential path, and Be is a cause exactly when Be ∈ E and e lies on a potential path. For the truth direction, every Cπ forces π to be active. Conversely, let C = (P, N ) be a prime truth implicant and complete it by making every unmentioned edge absent and every unmentioned blocker present. The completion satisfies C, so it contains an active path π. Every enabling literal of π already occurs in C; hence, Cπ ⪯ C, and primeness

gives C = Cπ . For falsity, complete a prime term by making every unmentioned edge present and every unmentioned blocker absent. Its explicitly disabled edges meet every directed s-t path and therefore contain a cut. Primeness retains an inclusion-minimal cut and exactly one disabling literal per cut edge, yielding D(K,α) . The nearest opposite term gives the robustness formulas. Destroying a true answer disables a- set of active edges forming an s–t cut in HE , whereas creating a false answer activates a potential path. The cause clauses select the literals ℓE (τ ) occurring in the corresponding path or cut terms. Consider one directed diamond with paths π1 = (x1 , x2 ) and π2 = (y1 , y2 ). Its prime truth conditions are Cπ1 and Cπ2 . The inclusion-minimal edge cuts are Kij = {xi , yj } such that i, j ∈ {1, 2}. Each of the four cuts admits four mode labellings. For example, D(K11 ,α) = ({Bx1 }, {Ey1 }) after choosing blocker presence on x1 and edge absence on y1 . The term forces both paths to fail while leaving every other edge and blocker unconstrained. Removing either literal reactivates a path in a suitable completion, thus the term is prime. The two robustness clauses differ even on small graphs. Suppose λHE (s, t) = 2. Toggling the two edge facts of a minimum cut changes the answer, while no single toggle does; therefore, Rob(E) = 2. For a false state with one potential path π = (f1 , f2 ), assume Ef1 ∈ E, Bf1 ∈ / E, Ef2 ∈ / E, and Bf2 ∈ E. The path has activation cost two: inserting Ef2 and deleting Bf2 creates the answer. Equation (19) proves minimality without enumerating interventions. Blockers participate symmetrically. If a unique potential path has all edge facts present and exactly one blocker Be present, the answer is false and deleting Be activates the path. Thus, Be is counterfactual for the non-answer. If the blocker is absent in a true state, inserting it can instead destroy the answer after a contingency disables all alternative paths. For a path π, let X
aE (π) = 1[Ef ∈ / E] + 1[Bf ∈ E] f ∈π

be its activation cost. For a mode-labelled cut (K, α), let X 1[Ef ∈ E], α(f ) = edge, cE (K, α) = 1[Bf ∈ / E], α(f ) = block. f ∈K

For τ = Ee , let m(τ ) = edge, and for τ = Be , let m(τ ) = block. Let Weτ contain the triples (π, K, α) such that π is a simple s-t path, K is an inclusion-minimal s-t edge cut, π ∩ K = {e}, and α(e) = m(τ ). The minimum over an empty family is ∞. Theorem 5. Let τ ∈ {Ee , Be }. Assume either that ans(E) = 1 and ℓE (τ ) is an enabling literal for e, or that ans(E) = 0 and ℓE (τ ) is a disabling literal for e. Then,
κE (τ ) = min τ aE (π) + cE (K, α) − 1 . (20) (π,K,α)∈We

If the stated polarity condition fails, κE (τ ) = ∞.

The path and cut must intersect only at the candidate edge: any other common edge contributes conflicting enabling and disabling literals. At e, the path and cut use complementary literals of the candidate; exactly one disagrees with the observed state, which accounts for the subtraction of one. All remaining disagreements are contingency changes. Theorem 3 then gives equality with the minimum contingency size. The cause criterion depends on potential paths, rather than only on the observed derivation. Consider potential paths π1 = (x1 , x2 ) = s → a → t and π2 = (y1 , y2 ) = s → b → t. Let E contain the edge atoms for x1 , x2 , y1 , omit the edge atom for y2 , and contain no blockers. Only π1 is active. For τ = Ey1 , choose π = π2 , K = {x1 , y1 }, and let α select edge absence on both cut edges. Then, 1. aE (π) = 1, cE (K, α) = 2 and 2. κE (τ ) = 1 + 2 − 1 = 2. Thus, Ey1 has responsibility 1/3, although no active path uses it. The corresponding contingency deletes Ex1 and inserts Ey2 ; the second path then sustains the answer, and toggling Ey1 destroys it. Minimum cut (Ford Jr and Fulkerson 1956) computes true-outcome robustness; Equation (19) is shortest path with weights wE (e) = 1[Ee ∈ / E] + 1[Be ∈ E] ∈ {0, 1, 2}. For the directed-diamond family in Corollary 3, the potential graph is acyclic. In a directed acyclic graph, e = (u, v) lies on a potential s-t path exactly when u is reachable from s and t is reachable from v: a repeated vertex in the concatenation would form a directed cycle. Thus, two graph searches decide actual-cause recognition for that family. Corollary 3. There is a fixed recursive stratified program and an explicitly represented family (In )n≥1 of intervention instances of size O(n) such that, given In , a mutable state F ⊆ Un , and a candidate atom τ ∈ Un , the value ansIn (F ), the cause status of τ at En , and Rob(En ) are computable in time polynomial in |In |, while |Prime1In | = 2^n .

6

Complexity

We construct a polynomial-size Boolean circuit for the response and establish the complexity of the causal decision problems. For a fixed safe stratified program and fixed goal predicate, with a ground goal atom A whose constants are part of the input, we construct circuit CΠ,Dx ,U ,A in polynomial time by grounding Π over the active domain and unrolling each stratum. The circuit has one input Xτ for each τ ∈ U. For F ⊆ U , let XF ∈ {0, 1}U be its characteristic vector, defined by XF (τ ) = 1 iff τ ∈ F . Then, ∀F ⊆ U ,

CΠ,Dx ,U ,A (XF ) = ans(F ),

(21)

The circuit size is polynomial in |Dx | + |U| + |A|. One gate represents each ground intensional atom at each immediateconsequence stage. Lower strata supply completed gates to negated intensional body atoms. Induction on stages and strata proves (21). For data complexity, the program Π and the goal predicate are fixed, while Dx , U, E, A and, when applicable, τ ∈ U and

binary k ≤ |U| form the input. The problems Cause, Robust, and Responsibility ask whether τ is a cause, Rob(E) ≤ k, and κE (τ ) ≤ k, respectively; equivalently, Responsibility asks whether RespE (τ ) ≥ 1/(k + 1). Theorem 6. For each problem below, there exists a fixed safe nonrecursive stratified program for which the problem is NP-complete in data complexity. 1. Cause, for an initially absent designated atom and a false observed outcome. 2. Robust, for a false observed outcome. 3. Responsibility, for an initially absent designated atom. Membership guesses the contingency or intervention and evaluates the fixed program on the required states. The cause reduction uses exogenous facts Var(x), Pos(c, x), Neg(c, x), and Clause(c), mutable assignment atoms True(x), and an initially absent mutable atom Switch. One fixed program contains Sat(c) ← Pos(c, x), True(x), Sat(c) ← Neg(c, x), Var(x), ¬True(x), Bad ← Clause(c), ¬Sat(c), Goal ← Switch, ¬Bad.

(22)

At the empty observed state, a contingency chooses precisely the variables assigned true; negated body atoms interpret every other variable as false. Before toggling Switch, the goal remains false. After the toggle, the goal holds exactly when no clause derives Bad, which is equivalent to satisfaction of the encoded formula. Thus, the designated atom is a cause exactly for satisfiable instances. For robustness, we reduce from Vertex Cover restricted to nonempty graphs; the restriction remains NP-complete by adding one disjoint edge and increasing the threshold by one. Exogenous edges and initially present mutable atoms Keep(v) feed the fixed rules Bad ← Edge(u, v), Keep(u), Keep(v), Goal ← ¬Bad.

(23)

Initially, every vertex is kept, and Bad holds whenever the input graph has an edge. Deleting a family S of keep-atoms removes Bad exactly when every edge has an endpoint in S; hence, S is a vertex cover. For responsibility, extend U by the initially absent candidate τ = Switch; under Goal ← Switch, ¬Bad, it becomes pivotal precisely after deleting a vertex cover. The minimum contingency size is therefore the minimum cover size. Each reduction uses a fixed nonrecursive stratified program and is linear in the input size. The reductions also expose the quantitative meaning of the thresholds. Consider the conjunctive normal form (CNF) formula x ∧ y, encoded by two unit clauses. At the empty mutable state, Switch is absent and the goal is false. The contingency {True(x), True(y)} satisfies both clauses while preserving the false goal; inserting Switch then derives the goal. No smaller contingency satisfies the formula, so the switch has minimum contingency size 2 and responsibility 1/3. For robustness, let the exogenous graph be a triangle and let every Keep-atom be present. Deleting one keep-atom leaves one edge with both endpoints kept, whereas deleting any two removes every such edge. Thus, the observed false

goal has robustness radius 2, equal to the minimum vertexcover size. These instances separate polynomial evaluation of a fixed rule program from the combinatorial search over admissible inputs. For fixed programs Π1 , Π2 over a common extensional signature and designated goal predicate, with possibly different auxiliary intensional predicates, Response-Equivalence takes common (Dx , U, A). Let ansj be the response induced by Πj ; it asks whether, ∀F ⊆ U , ans1 (F ) = ans2 (F ). Theorem 7. Response-Equivalence is coNP-complete in data complexity for two fixed nonrecursive stratified programs. A nonequivalence certificate is one mutable state on which the two fixed programs disagree. For hardness, assume encoding a CNF formula by exogenous clause and positive- and negative-occurrence relations and mutable truth-assignment atoms. The first fixed program derives the goal exactly on satisfying assignments; the second fixed program is over the same declared signature and contains no rule with head Goal, thus it never derives the goal. Their responses agree on all mutable states exactly when the formula is unsatisfiable. The construction is linear in the formula encoding. Therefore, even severe syntactic restrictions do not make universal preservation of intervention behavior tractable. Together with the separation at the observed state above, the theorem distinguishes preservation at one observed state from preservation over the full intervention domain.

7

Conclusion

We have studied causal explanations for stratified Datalog under perfect-model semantics and interventions over a finite set of mutable extensional facts. We have shown that minimal supports and inclusion-minimal outcome-changing interventions do not determine causality under negation. Using compatible prime implicants for the observed and opposite outcomes, we have characterized minimum contingencies, actual causes, responsibility, and robustness. Our characterization recovers the positive-Datalog minimal-support theory, yields path–cut formulas for blocked recursive reachability, and characterizes intervention-response preservation for replacements over a fixed exogenous database, mutable domain, and goal. Finally, we establish NP- and coNPcompleteness results for fixed nonrecursive stratified programs. Several problems remain open. These include identifying tractable fragments, designing parameterized algorithms for bounded contingency size or treewidth, computing compatible prime pairs without explicit enumeration, and extending the semantics to undefined truth values and multiple models. Acknowledgments. This work is funded by the German Research Foundation (DFG) – SFB 1574 Circular Factory– 471687386. Declaration on the Use of Generative AI. GPT-5.6 Luna was used to improve language and readability. The authors reviewed and verified all AI-assisted edits and remain responsible for the content.

References Abiteboul, S.; Hull, R.; and Vianu, V. 1995. Foundations of databases, volume 8. Addison-Wesley Reading. Apt, K. R.; Blair, H. A.; and Walker, A. 1988. Towards a theory of declarative knowledge. In Foundations of deductive databases and logic programming, 89–148. Elsevier. Bertossi, L.; and Salimi, B. 2017. Causes for query answers from databases: Datalog abduction, view-updates, and integrity constraints. International Journal of Approximate Reasoning, 90: 226–252. Bienvenu, M.; Figueira, D.; and Lafourcade, P. 2026. Responsibility Measures for Conjunctive Queries with Negation. In International Conference on Database Theory (ICDT). Bourgaux, C.; Bourhis, P.; Peterfreund, L.; and Thomazo, M. 2022. Revisiting Semiring Provenance for Datalog. In Proceedings of the International Conference on Principles of Knowledge Representation and Reasoning, volume 19, 91–101. Buneman, P.; Khanna, S.; and Tan, W.-C. 2002. On propagation of deletions and annotations through views. In Proceedings of the twenty-first ACM SIGMOD-SIGACT-SIGART symposium on Principles of database systems, 150–158. Chockler, H.; and Halpern, J. Y. 2004. Responsibility and blame: A structural-model approach. Journal of Artificial Intelligence Research, 22: 93–115. Crama, Y.; and Hammer, P. L. 2011. Boolean Functions: Theory, Algorithms, and Applications, volume 142 of Encyclopedia of Mathematics and its Applications. New York, NY, USA: Cambridge University Press. ISBN 978-0-52184751-3. Darwiche, A.; and Ji, C. 2022. On the computation of necessary and sufficient explanations. In Proceedings of the AAAI Conference on Artificial Intelligence, volume 36, 5582–5591. Deutch, D.; Milo, T.; Roy, S.; and Tannen, V. 2014. Circuits for Datalog Provenance. In ICDT, volume 3, 201–212. Dubslaff, C.; Weis, K.; Baier, C.; and Apel, S. 2022. Causality in Configurable Software Systems. In ICSE’22: Proceedings of the 44th International Conference on Software Engineering, 325–337. Association for Computing Machinery, Inc. Ford Jr, L. R.; and Fulkerson, D. R. 1956. Maximal flow through a network. Canadian journal of Mathematics, 8: 399–404. Freire, C.; Gatterbauer, W.; Immerman, N.; and Meliou, A. 2015. The complexity of resilience and responsibility for self-join-free conjunctive queries. Proceedings of the VLDB Endowment, 9(3). Grädel, E.; and Tannen, V. 2025. Provenance analysis and semiring semantics for first-order logic. In Model Theory, Computer Science, and Graph Polynomials: Festschrift in Honor of Johann A. Makowsky, 351–401. Springer. Halpern, J. Y.; and Pearl, J. 2005. Causes and explanations: A structural-model approach. Part I: Causes. The British journal for the philosophy of science.

Köhler, S.; Ludäscher, B.; and Zinn, D. 2013. First-Order Provenance Games. In Search of Elegance in the Theory and Practice of Computation, 8000: 382–399. Lee, S.; Koehler, S.; Ludaescher, B.; and Glavic, B. 2017. Efficiently Computing Provenance Graphs for Queries with Negation. arXiv:1701.05699. Meliou, A.; Gatterbauer, W.; Halpern, J. Y.; Koch, C.; Moore, K. F.; and Suciu, D. 2010a. Causality in databases. IEEE Data Engineering Bulletin, 33(3): 59–67. Meliou, A.; Gatterbauer, W.; Moore, K. F.; and Suciu, D. 2010b. The Complexity of Causality and Responsibility for Query Answers and non-Answers. Proceedings of the VLDB Endowment, 4(1). Thapa, R. B.; and Staab, S. 2026. Causality and Minimal Supports in Recursive Datalog. In Rules and Reasoning: 10th International Joint Conference, RuleML+ RR 2026, Vilnius, Lithuania. https://arxiv.org/abs/2607.16443. Vennekens, J. 2011. Actual causation in cp-logic. Theory and Practice of Logic Programming, 11(4-5): 647–662. Zhao, H.; Deep, S.; Koutris, P.; Roy, S.; and Tannen, V. 2024. Evaluating Datalog over Semirings: A Groundingbased Approach. Proceedings of the ACM on Management of Data, 2(2): 1–26.

Extended Proofs and Supplementary Results A

Supplementary Results

We collect additional Boolean consequences, conservative specializations, and solver reductions used by the main results. For a family SuppI of minimal positive supports, consider the standard monotone positive-support decomposition ans(F ) = 1

if and only if

∃S ∈ SuppI (S ⊆ F ).

(25)

For transversals, we use Tr(∅) = {∅} and Tr(H) = ∅ when ∅ ∈ H. Proposition 4. A fixed nonrecursive stratified program violates (25). At the empty observed state, some atom is an actual cause although it belongs to no inclusion-minimal intervention that changes the observed outcome. Proposition 5. There is a fixed nonrecursive stratified program whose prime truth implicant contains a negative literal and whose prime falsity implicant contains a positive literal. V W Let ϵ = (∅, ∅), 1 = ({ϵ}, ∅), and 0 = (∅, {ϵ}). We use the identities ∅ = 1 and ∅ = 0; an empty rule body therefore receives 1, and an empty family of alternative rules receives 0. For term families C and D, let Min⪯ select their ⪯-minimal members, and let C ⊗ D = Min⪯ {C ⊔ D|C ∈ C, D ∈ D, C, D compatible}. For pairs X = (T , F) and Y = (T ′ , F ′ ), let
X ⊓ Y = T ⊗ T ′ , Dual(T ⊗ T ′ ) ,
(26) X ∨PI Y = Dual(F ⊗ F ′ ), F ⊗ F ′ , ¬X = (F, T ). A mutable extensional atom u receives ({({u}, ∅)}, {(∅, {u})}); an exogenous true atom receives 1; and every other extensional atom receives 0. For a ground intensional atom H, let PrimebI (H) denote the prime implicants of F 7→ 1[H ∈ P(Π ∪ Dx ∪ F )]. Ground Π over the active domain. For a stratum i, let mi be its number of ground intensional atoms and initialize Vi0 (H) = 0. At stage t + 1, combine each ground rule body by ⊓, combine alternative rules and Vit (H) by ∨PI , use Vit for positive atoms in stratum i, use final pairs for lower-stratum atoms, and apply ¬ to negated atoms. For a Boolean response f : 2U → {0, 1}, let Primeb (f ) denote its prime b-implicants. The identities stated in Proposition 6 are standard Boolean prime-implicant operations (Crama and Hammer 2011). Proposition 6. For Boolean responses f and g over U, Prime1 (f ∧ g) = Prime1 (f ) ⊗ Prime1 (g), Prime0 (f ∨ g) = Prime0 (f ) ⊗ Prime0 (g), Prime0 (f ∧ g) = Dual(Prime1 (f ) ⊗ Prime1 (g)), Prime1 (f ∨ g) = Dual(Prime0 (f ) ⊗ Prime0 (g)), Primeb (¬f ) = Prime1−b (f ).

(27)

Proposition 7. For τ ∈ U, the following conditions are equivalent: 1. some state F satisfies ans(F ) ̸= ans(F △ {τ }); 2. some member of Prime1I contains a literal on τ ; 3. some member of Prime0I contains a literal on τ ; and 4. τ is counterfactual at some state. Let RelI contain the atoms satisfying Proposition 7. For every F, J ⊆ U, ans(F △ J) = ans(F △ (J ∩ RelI )). Corollary 4. For intervention instances with common Dx , U, E, and A, equality of either prime-implicant family is equivalent to response equality on every mutable state. Response equality implies equality of actual causes, responsibilities, and robustness radii at E. Corollary 5. Assume that Π is positive, and let b = ans(E). 1. If b = 1, every actual cause belongs to E, and τ ∈ E is a cause exactly when it occurs in a minimal support; and 2. If b = 0, every actual cause belongs to U \ E, and τ ∈ / E is a cause exactly when it occurs in a minimal transversal of SuppI .

For Πbr from Equation (17), an atom whose literal satisfied by a true state enables its edge is counterfactual exactly when every active s-t path uses that edge. An atom whose literal satisfied by a false state disables its edge is counterfactual exactly when, on some potential path, the complementary activation literal of the candidate is the only activation literal not satisfied by the state. For a fixed program and fixed goal predicate, Implicant takes (Dx , U, A, C, b), where C = (P, N ) satisfies P, N ⊆ U and P ∩ N = ∅, and where b ∈ {0, 1}; it asks whether C is a b-implicant. For two fixed programs over a common extensional signature and common designated goal predicate, Response-Equivalence asks whether their responses agree on every state over a common mutable domain. Proposition 8. For every fixed safe stratified program and fixed goal predicate, the ground goal atom A, including its constants, is input. A polynomial-time construction maps (Dx , U, A) to a Boolean circuit CΠ,Dx ,U ,A , with one input Xτ for each τ ∈ U, such that ∀F ⊆ U , CΠ,Dx ,U ,A (χF ) = ans(F ), where χF is the characteristic function of F . The circuit size is polynomial in |Dx | + |U | + |A|. Let eu = χE (u). For Boolean values x, y ∈ {0, 1}, x ⊕ y = 1 exactly when x ̸= y. Let X ⊕τ be obtained from X by complementing coordinate τ . Proposition 9. Let C = CΠ,Dx ,U ,A and b = ans(E). 1. Rob(E) ≤ k exactly when X C(X) = 1 − b and (Xu ⊕ eu ) ≤ k (28) u∈U

is satisfiable; and 2. κE (τ ) ≤ k exactly when Xτ = eτ ,

C(X) = b,

C(X ⊕τ ) = 1 − b

and

X

(Xu ⊕ eu ) ≤ k

u∈U \{τ }

(29)

is satisfiable. Removing the cardinality constraint decides Cause. Proposition 10. There are two fixed nonrecursive stratified Datalog programs over a common (Dx , U, E, A) with the same actual causes, responsibilities, and robustness radius at E, but different responses on 2U . Theorem 8. Implicant is coNP-complete in data complexity for a fixed nonrecursive stratified program. Hardness holds for the empty term and outcome 0.

B

Extended Proofs of Main Results

Proof of Theorem 1 We compute both responses on all mutable states, derive their support and baseline-change families, and then determine minimum contingency of every candidate at the observed state. Let Π1 be the program in Equation (6), let Π2 = {Goal ← P (c)}, and let I1 = (Π1 , ∅, {p, q, r}, ∅, Goal)

and

I2 = (Π2 , ∅, {p, q, r}, ∅, Goal).

For every F ⊆ {p, q, r}, ansI1 (F ) = 1 ⇐⇒ (p ∈ F ∧ q ∈ / F ∧r ∈ / F ) ∨ (p ∈ F ∧ q ∈ F ∧ r ∈ F ), ansI2 (F ) = 1 ⇐⇒ p ∈ F.

(31)

Minimal supports. For each instance, ans({p}) = 1 and ans(∅) = 0, thus {p} is a minimal support. Every true state of either instance contains p. Therefore, no support omitting p exists, and every support properly containing {p} is nonminimal. Thus, SuppI1 = SuppI2 = {{p}}.

(32)

Minimal outcome changes. The observed state is E = ∅, and both observed outcomes are 0. For I1 , the true intervention states are {p} and {p, q, r}; the latter properly contains the former. For I2 , every true intervention state contains p, and {p} is true. Thus, FlipI1 (E) = FlipI2 (E) = {{p}}. (33) Candidate p. For both instances, ans(E) = 0 and ans(E △ {p}) = 1. Thus, p is counterfactual, κIE1 (p) = κIE2 (p) = 0, and both responsibility values are 1. Candidate q in I1 . Let Γq = {p, r}. Equation (31) gives ansI1 (E △ Γq ) = ansI1 ({p, r}) = 0,

and

ansI1 (E △ (Γq ∪ {q})) = ansI1 ({p, q, r}) = 1.

Thus, κIE1 (q) ≤ 2. The contingencies excluding q of size at most one are ∅, {p}, and {r}. Their adjacent outcome pairs before and after toggling q are, respectively, (0, 0), (1, 0) and (0, 0). None satisfies (2). Therefore, κIE1 (q) = 2 and RespIE1 (q) = 1/3. Candidate r in I1 . Let Γr = {p, q}. Then, ansI1 (E △ Γr ) = ansI1 ({p, q}) = 0,

and

ansI1 (E △ (Γr ∪ {r})) = ansI1 ({p, q, r}) = 1.

The contingencies excluding r of size at most one are ∅, {p}, and {q}, with adjacent outcome pairs (0, 0), (1, 0) and (0, 0). Thus, κIE1 (r) = 2 and RespIE1 (r) = 1/3. Candidates q and r in I2 . The second response depends only on p. For every contingency excluding q, toggling q preserves membership of p, and therefore preserves the outcome. For every contingency excluding r, toggling r also preserves membership of p, and therefore preserves the outcome. κIE2 (q) = κIE2 (r) = ∞, and RespIE2 (q) = RespIE2 (r) = 0. Equations (32) and (33), together with the computed responsibility values, prove the theorem. Proof of Theorem 2 For each n, we derive the response of the fixed program, identify all inclusion-minimal outcome-changing interventions, and prove matching upper and lower bounds on each designated contingency. For n ≥ 2, let Dx = {Item(ai )|1 ≤ i ≤ n} and U = {g} ∪ {si |1 ≤ i ≤ n}, where si = Sel(ai ), and let E = ∅. Use the fixed program (7). It is safe and nonrecursive. A stratification places extensional predicates in stratum 0, Some and Missing in stratum 1, and None, All, and Goal in stratum 2. For a state F ⊆ U , let SF = F ∩ {s1 , . . . , sn }. Perfect-model evaluation gives Some ∈ P(Π ∪ Dx ∪ F ) ⇐⇒ SF ̸= ∅, Missing ∈ P(Π ∪ Dx ∪ F ) ⇐⇒ SF ̸= {s1 , . . . , sn },

(36)

ans(F ) = 1 ⇐⇒ g ∈ F ∧ SF = ∅ ∨ SF = {s1 , . . . , sn } . The observed outcome is 0. Equation (36) gives ans({g}) = 1, thus Rob(E) ≤ 1. No intervention of size 0 changes the outcome, hence Rob(E) = 1. Let J be an inclusion-minimal outcome-changing intervention. Since E = ∅, its reached state is J, and Equation (36) gives g ∈ J. If SJ = ∅, then J = {g}. If SJ = {s1 , . . . , sn }, then {g} ⊊ J already has outcome 1, contrary to inclusion-minimality. Thus, FlipI (E) = {{g}}. (37) For i ∈ {1, . . . , n}, let Γi = {g}∪{sj |j ̸= i}. The reached state has a nonempty proper selection family, thus ans(E△Γi ) = 0. After toggling si , every selection is present and Equation (36) gives outcome 1. Hence, si is a cause and κE (si ) ≤ |Γi | = n. For the reverse inequality, let Γ be any contingency witnessing that si is a cause. Since si ∈ / E and si ∈ / Γ, the state E △ Γ omits si , while E △ (Γ ∪ {si }) contains it. The latter state has outcome 1. By Equation (36), it must contain g, and its selection family cannot be empty because it contains si . Therefore, it contains every sj . Thus, {g} ∪ {sj |j ̸= i} ⊆ Γ,

|Γ| ≥ n.

We obtain κE (si ) = n and RespE (si ) = 1/(n + 1) for every i. The database and mutable domain have size O(n), while the program is fixed. Proof of Proposition 1 Let b ∈ {0, 1}. We prove the prime cover, the duality identity, and response determination. Prime cover and forward direction. Assume ans(F ) = b. The complete term CF = (F, U \ F ) has exactly one satisfying state. Indeed, G |= CF implies F ⊆ G and G ∩ (U \ F ) = ∅; hence, G ⊆ F and G = F . Thus, CF is a b-implicant. The family of subterms of CF has cardinality at most 2|F | 2|U \F | and is finite. The nonempty family of b-implicant subterms therefore has a ⪯-minimal member C. By Definition 3, C ∈ PrimebI . Since C ⪯ CF and F |= CF , we have F |= C. Prime cover and reverse direction. Assume F |= C for some C ∈ PrimebI . The implicant condition in Definition 3 applies to every satisfying state, in particular to F . Hence, ans(F ) = b. The two directions establish (8). Duality, inclusion Prime1−b ⊆ Dual(PrimebI ). Let D ∈ Prime1−b . For every C ∈ PrimebI , the terms C and D conflict. If I I they were compatible, their merged term would admit a state F satisfying both, and the two implicant conditions would give ans(F ) = b and ans(F ) = 1 − b, a contradiction. Let SD = {D′ ⪯ D | D′ conflicts with every C ∈ PrimebI }. The family is nonempty because D ∈ SD , and it is finite because D has finitely many subterms. Choose a ⪯-minimal D0 ∈ SD . We show that D0 is a (1 − b)-implicant. Let F |= D0 . If ans(F ) = b, the prime cover yields C ∈ PrimebI with F |= C.

The common satisfying state F would make C and D0 compatible, contradicting D0 ∈ SD . Thus, ans(F ) = 1 − b for every F |= D0 . We now have a (1 − b)-implicant D0 ⪯ D. Since D is prime, D0 = D. The minimality of D0 in SD is exactly the minimality required by Dual(PrimebI ), thus D ∈ Dual(PrimebI ). Duality, inclusion Dual(PrimebI ) ⊆ Prime1−b . Let D ∈ Dual(PrimebI ), and let F |= D. If ans(F ) = b, the prime cover I yields C ∈ PrimebI with F |= C, contradicting the defining conflict condition for D. Therefore, ans(F ) = 1 − b, and D is a (1 − b)-implicant. Among the finitely many (1 − b)-implicant subterms of D, choose a prime one D0 ⪯ D. The inclusion proved above gives D0 ∈ Dual(PrimebI ). Since D is minimal among terms conflicting with every member of PrimebI , we have D ⪯ D0 . Together with D0 ⪯ D, antisymmetry gives D = D0 , and hence D ∈ Prime1−b . Equation (9) follows. I Response determination. Let instances I1 and I2 share (Dx , U, A). If Prime1I1 = Prime1I2 , then for every F ⊆ U, ansI1 (F ) = 1 ⇐⇒ ∃C ∈ Prime1I1 (F |= C) ⇐⇒ ∃C ∈ Prime1I2 (F |= C) ⇐⇒ ansI2 (F ) = 1. Since both responses are Boolean, equality of their truth values implies full response equality. If Prime0I1 = Prime0I2 , then for every F ⊆ U , ansI1 (F ) = 0 ⇐⇒ ∃C ∈ Prime0I1 (F |= C) ⇐⇒ ∃C ∈ Prime0I2 (F |= C) ⇐⇒ ansI2 (F ) = 0. Booleanity again gives full response equality. Conversely, response equality makes the implicant predicate identical for every term and every polarity; the common subterm order then makes primeness identical. Thus, both prime families are equal. Duality also shows that equality of either polarity entails equality of the other. Proof of Proposition 2 Recall the stratification thus that all intensional predicates have positive strata and the used intensional t strata are 1, . . . , s. For a mutable state F ⊆ U, let Mi,F be the family of ground intensional atoms in stratum i obtained after t applications of the inflationary immediate-consequence operator for that stratum. Extensional facts and the completed relations of lower strata remain constant during that iteration. For a ground stratum-i atom H, let t hH,t (F ) = 1 ⇐⇒ H ∈ Mi,F .

We prove, simultaneously for every stratum-i atom H, Vit (H) = Prime1 (hH,t ), Prime0 (hH,t )

(38)

by outer induction on i and inner induction on t. Outer induction . For every j < i and every ground atom L in stratum j, the final pair computed for L equals the prime pair of its completed perfect-model response. For i = 1, no lower intensional stratum exists, thus the hypothesis is vacuous. 0 Inner base case. For every F , Mi,F = ∅. Thus, hH,0 is the constant-zero response. Its prime 1-family is empty, and its unique prime 0-implicant is the empty term ϵ. Therefore,

Vi0 (H) = 0 = ∅, {ϵ} = Prime1 (hH,0 ), Prime0 (hH,0 ) . Inner induction . Assume (38) for every ground atom in stratum i at stage t. Let ρ be a ground stratum-i rule with head H, t and let bρ,t be its Boolean body response when positive stratum-i atoms are interpreted by Mi,F . We first prove the exact pair for the body by induction on its length. For an empty body, the response is the constant-one function. Its unique prime 1-implicant is ϵ, and its prime 0-family is empty, thus the assigned pair is 1. Assume that the first k body atoms have response gk and exact pair (Prime1 (gk ), Prime0 (gk )). Let L be the (k + 1)-st body atom, and let λL be its Boolean response. We verify the exact pair for L in every syntactically possible case. 1. If L = u is a mutable extensional atom, then λL (F ) = 1 exactly when u ∈ F . Its prime families are {({u}, ∅)} and {(∅, {u})}, which are the initialized pair. 2. If L is an exogenous extensional atom, its value is independent of F . When the atom belongs to Dx , its response is constant one and its pair is 1. Otherwise, its response is constant zero and its pair is 0. 3. If L is a positive atom in a lower intensional stratum, the outer induction hypothesis supplies its exact completed pair. 4. If L is a positive atom in stratum i, the inner induction hypothesis supplies the exact pair of its stage-t response. 5. If L = ¬u for an extensional atom u, Cases 1 and 2 give the exact pair for u. Proposition 6 exchanges its two prime families under negation, exactly as the operation ¬X in (26).

6. If L = ¬K for an intensional atom K, stratification places K in a stratum below i. The outer induction hypothesis gives the completed exact pair for K, and Proposition 6 gives the exact swapped pair for ¬K. The six cases are exhaustive because a safe stratified rule body contains positive or negated extensional atoms, positive currentor lower-stratum intensional atoms, and negated lower-stratum intensional atoms; stratification excludes negated current- and higher-stratum intensional atoms. The response of the first k + 1 body atoms is gk ∧ λL . By Proposition 6, applying ⊓ to their exact pairs yields
Prime1 (gk ∧ λL ), Prime0 (gk ∧ λL ) . Induction on the body length gives
Pairρ,t = Prime1 (bρ,t ), Prime0 (bρ,t ) .

(39)

Let Ri (H) = {ρ1 , . . . , ρm } be the ground stratum-i rules with head H. Let q0 = hH,t

and

qj = qj−1 ∨ bρj ,t

(1 ≤ j ≤ m).

The exact pair for q0 follows from the inner induction hypothesis. If the iteration has the exact pair for qj−1 , then Equation (39) and the disjunction identity in Proposition 6 show that ∨PI produces the exact pair for qj . Induction on j yields the exact pair for _ qm = hH,t ∨ bρ,t = hH,t+1 . (40) ρ∈Ri (H)

The case Ri (H) = ∅ has m = 0 and gives hH,t+1 = hH,t , so it is included. Consequently,
Vit+1 (H) = Prime1 (hH,t+1 ), Prime0 (hH,t+1 ) , which proves the inner induction step. 1 0 ⊆ · · · is ⊆ Mi,F Let mi be the number of ground intensional atoms in stratum i. For each state F , the sequence Mi,F inflationary. Every strict inclusion adds at least one of the mi available atoms. Hence, no sequence has more than mi strict increases, and mi mi +1 Mi,F = Mi,F for every F . The stabilized interpretation is the least fixpoint of the positive immediate-consequence operator for stratum i. Applying (38) at stage mi gives
Vimi (H) = Prime1I (H), Prime0I (H) . Thus, the final values in stratum i satisfy the outer induction claim. Induction over i = 1, . . . , s proves the proposition. Proof of Theorem 3 Let b = ans(E) and τ ∈ U . We prove each item in both directions. The responsibility proof constructs a contingency from a compatible prime pair and constructs a compatible prime pair from a minimum contingency. / E, then ℓE (τ ) = ¬τ and The candidate polarity cases are exhaustive. If τ ∈ E, then ℓE (τ ) = τ and ℓcE (τ ) = ¬τ . If τ ∈ ℓcE (τ ) = τ . Each alternative occurs with b = 1 and with b = 0. The derivations below use only these complementary literals and therefore discharge all four cases. Item 1, forward direction. Assume that τ is an actual cause, and let Γ satisfy (2). Let F = E △ Γ and G = F △ {τ }. Since τ ∈ / Γ, the states E and F assign the same value to τ . Equation (2) gives ans(F ) = b and ans(G) = 1 − b. By (8), choose C ∈ PrimebI with F |= C. If C contained no literal on τ , then G |= C, and the implicant property would give ans(G) = b. Thus, C contains a literal on τ . Since F agrees with E on τ , that literal is ℓE (τ ). Item 1, reverse direction. Assume that C ∈ PrimebI contains ℓE (τ ). Let C−τ remove that literal. Primeness implies that C−τ is not a b-implicant. Thus, a state G satisfies G |= C−τ and ans(G) = 1 − b.

(41)

The state G assigns τ the value opposite to its current value. If it assigned the current value, then G |= C, contradicting (41). Let F = G △ {τ }. Then, F |= C, ans(F ) = b, and F agrees with E on τ . Let Γ = E △ F . We have τ∈ / Γ,

E △ Γ = F and E △ (Γ ∪ {τ }) = G.

These equalities and (41) establish (2). Item 2, upper bound. Let (C, D) ∈ QbE,τ , and let M = C ⊔ Dτ = (PM , NM ). Compatibility makes M a term. Both components contain ℓE (τ ). Let F = (E ∪ PM ) \ NM and Γ = E △ F.

For every positive literal of M , F contains its atom; for every negative literal, F omits its atom. Thus, F |= M . Since ℓE (τ ) is satisfied by E, τ ∈ / Γ. The remaining literals of M not satisfied by E correspond exactly to the noncandidate members of Γ, thus |Γ| = dE,−τ (M ). (42) Since F |= C, ans(F ) = b. Since F |= Dτ , toggling τ yields F △ {τ } |= D, and therefore ans(F △ {τ }) = 1 − b. Therefore, Γ is a contingency, and κE (τ ) ≤ dE,−τ (C ⊔ Dτ ). Minimization over QbE,τ gives κE (τ ) ≤ KE (τ ). Item 2, lower bound. Assume κE (τ ) < ∞, and let Γ be a contingency of minimum size. Let F = E △ Γ and G = F △ {τ }. Choose C ∈ PrimebI with F |= C, and choose D ∈ Prime1−b with G |= D. The forward direction of Item 1 shows that C I contains ℓE (τ ). If D contained no literal on τ , then F |= D, contradicting ans(F ) = b. The literal on τ in D agrees with G, thus it is ℓcE (τ ). Hence, F |= Dτ . The common satisfying state F proves that C and Dτ are compatible, and therefore (C, D) ∈ QbE,τ . Let M = C ⊔ Dτ = (PM , NM ). Since F = E △ Γ satisfies M , every atom in (PM \ E) \ {τ } belongs to F \ E ⊆ Γ, and every atom in (NM ∩ E) \ {τ } belongs to E \ F ⊆ Γ. The two atom families are disjoint. Thus, dE,−τ (M ) ≤ |Γ| = κE (τ ). Taking the minimum over compatible pairs yields KE (τ ) ≤ κE (τ ). The two bounds give KE (τ ) = κE (τ ). Equation (3) gives the responsibility formula. If QbE,τ = ∅, the lower-bound construction proves that no contingency exists; both minima are ∞. Item 3, upper bound. Let D = (P, N ) ∈ Prime1−b , and let I F = (E ∪ P ) \ N. Then, F |= D and ans(F ) = 1 − b. The toggled atoms are exactly P \ E and N ∩ E, thus |E △ F | = dE (D). Therefore, Rob(E) ≤ dE (D). Minimization over D gives the upper bound in (13). Item 3, lower bound. Assume Rob(E) < ∞, and choose J ⊆ U with |J| = Rob(E) and ans(E △ J) = 1 − b. By (8), choose D = (P, N ) ∈ Prime1−b satisfied by E △ J. Every atom in P \ E must be inserted by J, and every atom in N ∩ E I must be deleted by J. These families are disjoint. Thus, dE (D) = |P \ E| + |N ∩ E| ≤ |J| = Rob(E). The upper and lower bounds prove (13). If Prime1−b = ∅, Equation (8) states that no opposite-outcome state exists, so both I sides are ∞. Proof of Proposition 3 Let p = P (c), q = Q(c), r = R(c), U = {p, q, r}, and E = {p, r}. Let Π3 be the program in Equation (15) and let I3 = (Π3 , ∅, U , E, Goal). The program is ground, safe, nonrecursive, and stratified. For every F ⊆ U, ans(F ) = 1 ⇐⇒ r ∈ / F ∧ (p ∈ /F ∨ q∈ / F ).

(43)

Since r ∈ E, the observed outcome is 0. We compute the prime 0-family. The term Cr = ({r}, ∅) forces outcome 0. Its only proper subterm is ϵ, which is satisfied by ∅ of outcome 1; hence, Cr is prime. The term Cpq = ({p, q}, ∅) also forces outcome 0: when r ∈ F , the first conjunct in (43) fails, and when r ∈ / F , the two disjuncts fail because p, q ∈ F . Removing p yields ({q}, ∅), which is satisfied by {q} of outcome 1. Removing q yields ({p}, ∅), which is satisfied by {p} of outcome 1. Thus, Cpq is prime. Every false state either contains r or contains both p and q. If a 0-implicant contained neither r nor both p, q as positive requirements, it would admit a true state obtained by omitting r and one of p, q. Therefore, every prime 0-implicant equals Cr or Cpq , and Prime0I = {({r}, ∅), ({p, q}, ∅)}. (44) For outcome 1, let Dp = (∅, {p, r}) and Dq = (∅, {q, r}). Every state satisfying either term omits r and omits one of p, q, thus it has outcome 1. In Dp , removing ¬r admits {r} of outcome 0, and removing ¬p admits {p, q} of outcome 0. Thus, Dp is prime. The symmetric witnesses {r} and {p, q} show that both literals of Dq are necessary. Every true state omits r and at least one of p, q, thus every prime 1-implicant equals Dp or Dq . Therefore, Prime1I = {(∅, {p, r}), (∅, {q, r})}.

(45)

For candidate p, ℓE (p) = p. The only prime opposite-outcome term containing ¬p is Dp . Outside the candidate coordinate, its sole literal is ¬r, which is not satisfied by E. Hence, opp δE (p) = dE,−p (Dp ) = 1.

(46)

Let Γ = {q, r}. Then, E △ Γ = {p, q} and E △ (Γ ∪ {p}) = {q}, and (43) gives outcomes 0 and 1, respectively. Therefore, p is a cause and κE (p) ≤ 2. The contingencies excluding p of size at most one are exactly ∅, {q}, and {r}. Their adjacent outcome pairs are Γ ans(E △ Γ) ∅ ans({p, r}) = 0 {q} ans({p, q, r}) = 0 {r} ans({p}) = 1

ans(E △ (Γ ∪ {p})) ans({r}) = 0 ans({q, r}) = 0 ans(∅) = 1

No row satisfies Definition 2. Thus, κE (p) ≥ 2, and κE (p) = 2. Finally, the current prime term Cpq contains p. Replacing ¬p in Dp by p gives Dpp = ({p}, {r}), which is compatible with Cpq . Their merge is ({p, q}, {r}). Outside p, the literals not satisfied by E are q and ¬r, thus Equation (12) returns 2. The compatible current-outcome term accounts for the contingency change that the opposite-only distance omits. Proof of Corollary 1 Let I and I ′ share Dx , U, and A. Assume that the replacement is intervention-preserving. Then, ansI (F ) = ansI ′ (F ) for every F ⊆ U. For every term C and polarity b, C is a b-implicant for I ⇐⇒ ∀F |= C, ansI (F ) = b ⇐⇒ ∀F |= C, ansI ′ (F ) = b ⇐⇒ C is a b-implicant for I ′ . The subterm order is common to the two instances. Hence, C has a proper b-implicant subterm for I exactly when it has one for I ′ . Thus, PrimebI = PrimebI ′ (b = 0, 1). Conversely, assume Prime1I = Prime1I ′ . For every mutable state F , the prime cover gives ansI (F ) = 1 ⇐⇒ ∃C ∈ Prime1I (F |= C) ⇐⇒ ∃C ∈ Prime1I ′ (F |= C) ⇐⇒ ansI ′ (F ) = 1. The Boolean responses therefore agree on every state, so the replacement is intervention-preserving. If Prime0I = Prime0I ′ , then for every F ⊆ U , ansI (F ) = 0 ⇐⇒ ∃C ∈ Prime0I (F |= C) ⇐⇒ ∃C ∈ Prime0I ′ (F |= C) ⇐⇒ ansI ′ (F ) = 0. The Boolean responses agree on every mutable state. Equation (9) also shows that equality of the prime 1-families is equivalent to equality of the prime 0-families. Both directions are proved. Proof of Corollary 2

Assume that Π is positive. Perfect-model entailment is monotone in the mutable state: F ⊆ F ′ =⇒ ans(F ) ≤ ans(F ′ ).

(50)

Prime truth implicants are minimal supports. Let S ∈ SuppI . Every state F satisfying (S, ∅) contains S. Since ans(S) = 1, monotonicity gives ans(F ) = 1. Thus, (S, ∅) is a 1-implicant. For every s ∈ S, minimality of S gives ans(S \ {s}) = 0, and the state S \ {s} satisfies the term obtained by deleting the literal s. Hence, every literal is necessary and (S, ∅) is prime. Conversely, let C = (P, N ) ∈ Prime1I . The state P satisfies C because P ∩ N = ∅, thus ans(P ) = 1. Every state containing P has outcome 1 by monotonicity; therefore, (P, ∅) is a 1-implicant and a subterm of C. Primeness gives N = ∅. If a proper subset P ′ ⊊ P had outcome 1, monotonicity would make (P ′ , ∅) a proper 1-implicant subterm of C, a contradiction. Thus, P is a minimal support. We obtain Prime1I = {(S, ∅) | S ∈ SuppI }. Prime falsity implicants are minimal transversals. Let T ∈ Tr(SuppI ), and let F |= (∅, T ). Then, F ∩ T = ∅. Suppose ans(F ) = 1. Among the finitely many substates of F with outcome 1, choose an inclusion-minimal one S. Then, S ∈ SuppI and S ⊆ F , thus S ∩ T = ∅, contradicting that T intersects every support. Therefore, (∅, T ) is a 0-implicant.

Let t ∈ T . Since T is an inclusion-minimal transversal, T \ {t} is not a transversal. Hence, some St ∈ SuppI satisfies St ∩ (T \ {t}) = ∅. Since T is a transversal, St ∩ T ̸= ∅; the preceding equality forces St ∩ T = {t}. Thus, St satisfies the term obtained from (∅, T ) by deleting ¬t, and ans(St ) = 1. Every negative literal is necessary, thus (∅, T ) is prime. Conversely, let C = (P, N ) ∈ Prime0I . We first show that (∅, N ) is a 0-implicant. Suppose F ∩ N = ∅ and ans(F ) = 1. Since P ∩ N = ∅, the state F ∪ P also avoids N . Monotonicity gives ans(F ∪ P ) = 1, while F ∪ P |= (P, N ) = C, contradicting the 0-implicant property. Thus, (∅, N ) is a 0-implicant. Because it is a subterm of the prime term C, we obtain P = ∅. The family N intersects every support. Otherwise, a support S ∈ SuppI with S ∩ N = ∅ would satisfy (∅, N ) and have outcome 1. If a proper subset N ′ ⊊ N intersected every support, the argument in the preceding paragraph would show that (∅, N ′ ) is a proper 0-implicant subterm, contradicting primeness. Hence, N is an inclusion-minimal transversal, and Prime0I = {(∅, T ) | T ∈ Tr(SuppI )}. The boundary conventions also agree. If SuppI = ∅, no state has outcome 1, thus Prime1I = ∅, the response is constant zero, and Prime0I = {ϵ}; our convention gives Tr(∅) = {∅}. If ∅ ∈ SuppI , monotonicity makes the response constant one, thus Prime1I = {ϵ} and Prime0I = ∅; our convention gives Tr(SuppI ) = ∅. Thus, both equalities in (16) hold in all cases. Proof of Theorem 4 We prove the path and cut representations in both directions, derive the two robustness formulas by matching upper and lower bounds, and then prove the cause and succinctness clauses. Let H = (V, L), and use the notation from Section 5. Item 1, forward direction. Let π be a simple s-t path. Every state satisfying Cπ contains Ee and omits Be for every e ∈ π. Thus, every edge of π is active, and Πbr derives Path(s, t). To prove primeness, remove one literal from Cπ . If the removed literal is the positive literal Ee , choose a state containing exactly the edge facts for π \ {e}, omitting all blockers on π, and omitting all other edge facts. If the removed literal is the negative literal ¬Be , choose a state containing all edge facts on π, containing Be , omitting the other blockers on π, and omitting all other edge facts. In either case, the reduced term is satisfied and the active graph has no s-t path. Thus, every literal is necessary, and Cπ is prime. Item 1, reverse direction. Let C = (P, N ) ∈ Prime1I . Suppose Be ∈ P . Remove the positive blocker literal Be , and let F satisfy the reduced term. If Be ∈ F , then F |= C and has an active s-t path. If Be ∈ / F , let F ′ = F ∪ {Be }. The state F ′ satisfies C, so it has an active s-t path. Passing from F ′ to F removes a blocker and can only activate edge e; hence, every path active in F ′ remains active in F . Thus, the reduced term is a 1-implicant, contradicting primeness. Thus, P contains no blocker atom. Suppose Ee ∈ N , thus C contains the negative edge literal ¬Ee . Remove that literal, and let F satisfy the reduced term. If Ee ∈ / F , then F |= C and has an active path. If Ee ∈ F , let F ′ = F \ {Ee }. The state F ′ satisfies C, so it has an active path. Passing from F ′ to F inserts an edge fact and can only activate edge e; the path remains active. Again, the reduced term is a 1-implicant, contradicting primeness. Hence, N contains no edge atom. Primeness therefore gives P ⊆ {Ee |e ∈ L} and N ⊆ {Be |e ∈ L}.

(51)

Let FC contain exactly the edge facts in P , omit exactly the blockers in N , omit every other edge fact, and contain every other blocker. The state FC satisfies C. Since C is a 1-implicant, the active graph HFC contains a simple s-t path π. Every edge e ∈ π satisfies Ee ∈ P and Be ∈ N . Hence, Cπ ⪯ C. The forward direction proved that Cπ is a 1-implicant. Primeness of C gives C = Cπ . Item 2, forward direction. Let K be an inclusion-minimal directed s-t edge cut, and let α : K → {edge, block}. Every state satisfying D(K,α) disables each edge of K: an edge fact is absent when α(e) = edge, and a blocker is present when α(e) = block. Its active graph is a subgraph of H − K, thus it has no s-t path. Thus, D(K,α) is a 0-implicant. Let e ∈ K. Inclusion-minimality of K gives a directed s-t path πe in H − (K \ {e}). Since K is a cut, πe uses e; thus, πe ∩ K = {e}. Remove the literal selected for e from D(K,α) , and construct state Fe as follows. For every f ∈ πe , let Ef ∈ Fe and Bf ∈ / Fe . For every f ∈ K \ {e}, let Ef ∈ / Fe when α(f ) = edge, and let Bf ∈ Fe when α(f ) = block. These assignments do not conflict because πe ∩ (K \ {e}) = ∅. For every edge not yet assigned, let its edge atom be absent and its blocker atom be present. The resulting state satisfies every retained literal of the reduced term. It also contains every edge atom and omits every blocker on πe , thus it activates πe . Thus, removing any selected literal admits a true state. Every selected literal is necessary, and D(K,α) is prime. Item 2, reverse direction. Let D = (P, N ) ∈ Prime0I . Suppose Ee ∈ P . Remove the positive edge literal Ee , and let F satisfy the reduced term. If Ee ∈ F , then F |= D and has no active s-t path. If Ee ∈ / F , let F ′ = F ∪ {Ee }. The state F ′ satisfies D and has no active path. Passing from F ′ to F deletes an edge fact and can only remove active edges, thus F also has no active path. The reduced term is a 0-implicant, contradicting primeness. Hence, P contains no edge atom.

Suppose Be ∈ N , so D contains the negative blocker literal ¬Be . Remove that literal, and let F satisfy the reduced term. If Be ∈ / F , then F |= D and has no active path. If Be ∈ F , let F ′ = F \ {Be }. The state F ′ satisfies D and has no active path. Passing from F ′ to F inserts a blocker and can only remove active edge e, so F also has no active path. The reduced term is a 0-implicant, contradicting primeness. Hence, N contains no blocker atom. Thus, P ⊆ {Be |e ∈ L} and N ⊆ {Ee |e ∈ L}.

(52)

No edge contributes both Be ∈ P and Ee ∈ N . If both occurred, remove either one. The remaining literal still disables e, and all other edge constraints are unchanged. Every state satisfying the reduced term still disables every edge disabled by the original term, thus it remains unreachable. The reduced term would be a proper 0-implicant, contradicting primeness. Let K = {e|Be ∈ P or Ee ∈ N }. If K were not a directed s-t cut, choose a directed path π with π ∩ K = ∅. Construct a state F by putting Ef ∈ F and Bf ∈ /F for every f ∈ π; putting Bf ∈ F when Bf ∈ P ; putting Ef ∈ / F when Ef ∈ N ; and assigning all remaining edge facts absent and all remaining blockers present. The path avoids K, so these assignments are consistent. The state F satisfies D and activates π, contradicting the 0-implicant property. Thus, K is a cut. If a proper subset K ′ ⊊ K were a cut, retain in D only the selected literal for each edge of K ′ . Every state satisfying that proper subterm disables all edges in K ′ , and therefore has no directed s-t path. The subterm would be a proper 0-implicant, contradicting primeness. Thus, K is inclusion-minimal, and D = D(K,α) for the unique mode map determined by its literals. Item 3. Assume HE contains an s-t path. Let J change the outcome to false. Let XJ contain the edges active in HE that are inactive in HE△J . Every s-t path in HE intersects XJ ; otherwise, that path would remain active after applying J. Thus, XJ is an s-t edge cut of HE . Making an active edge inactive requires toggling its present edge fact or its absent blocker, and distinct edges require distinct facts. Therefore, |J| ≥ |XJ | ≥ λHE (s, t). (53) Conversely, let K be a minimum edge cut of HE . For every e ∈ K, toggle either the present edge fact Ee or the absent blocker Be . The resulting intervention has size |K|, only disables active edges, and removes every active s-t path. Thus, Rob(E) ≤ |K| = λHE (s, t). Together with (53), the two bounds prove (18). Item 4. Assume HE has no s-t path. If H has no potential s-t path, no intervention can create the goal, and both sides of (19) equal ∞. Assume that H has a potential path. For a potential path π, let Jπ = {Ee |e ∈ π, Ee ∈ / E} ∪ {Be |e ∈ π, Be ∈ E}. Applying the intervention Jπ makes every edge of π active. Its cardinality is the sum in (19), thus the minimum path cost is an upper bound on Rob(E). Conversely, let J create the goal, and choose an active s-t path π in HE△J . For every e ∈ π, if Ee ∈ / E, then Ee ∈ J; if Be ∈ E, then Be ∈ J. These literals concern distinct mutable atoms. Therefore, X
|J| ≥ 1[Ee ∈ / E] + 1[Be ∈ E] . e∈π

Minimization over J and π gives the lower bound and establishes (19). Item 5. Assume first that ans(E) = 1. A prime 1-implicant is a path term Cπ by Item 1. Such a term contains only the enabling literals Ef and ¬Bf for edges f ∈ π. Let τ = Ee . If Ee ∈ E, then ℓE (τ ) = Ee , and Cπ contains that literal exactly when e ∈ π. If Ee ∈ / E, then ℓE (τ ) = ¬Ee , and no path term contains that disabling literal. Let τ = Be . If Be ∈ / E, then ℓE (τ ) = ¬Be , and Cπ contains it exactly when e ∈ π. If Be ∈ E, then ℓE (τ ) = Be , and no path term contains it. By Item 1 of Theorem 3, a candidate is therefore a cause in a true state exactly when its current literal enables e and e lies on a simple potential s-t path. Assume next that ans(E) = 0. A prime 0-implicant is a cut term D(K,α) by Item 2. Such a term contains only disabling literals: ¬Ef in edge mode and Bf in blocker mode. For τ = Ee , the current literal occurs in a cut term exactly when Ee ∈ / E, e ∈ K, and α(e) = edge. For τ = Be , it occurs exactly when Be ∈ E, e ∈ K, and α(e) = block. Hence, the causal characterization reduces the false-outcome cause condition to membership of e in an inclusion-minimal directed s-t edge cut. We prove that an edge belongs to an inclusion-minimal directed s-t cut exactly when it belongs to a directed s-t path. Let e ∈ K for an inclusion-minimal cut K. Since K \ {e} is not a cut, the graph H − (K \ {e}) contains an s-t path π. The path must use e, because K is a cut. Thus, e ∈ π. Conversely, let π be an s-t path containing e. The family K0 = {e} ∪ (L \ π) is a cut: every s-t path either is π, in which case it uses e, or contains an edge outside π. Among the cuts K ′ ⊆ K0 that contain e, choose an inclusion-minimal one K. For every f ∈ K \ {e}, the family K \ {f } still contains e; its being a cut would contradict the choice of K. The family K \ {e} is not a cut because the path π avoids K0 \ {e}, and hence avoids K \ {e}. Thus, deleting any member of K destroys the cut property, thus K is inclusion-minimal and contains e. The false-outcome cause characterization follows.

Counterfactual cases. Suppose ans(E) = 1 and ℓE (τ ) is an enabling literal for e. We distinguish the two possible edge states. If e is inactive in HE , then toggling τ cannot remove any active edge and therefore cannot destroy an active s-t path. Thus, τ is not counterfactual. Since ans(E) = 1, an active s-t path exists, and no active path uses the inactive edge e; therefore, the condition that every active s-t path uses e is also false. If e is active in HE , toggling τ disables exactly e and changes no other edge status. The resulting state is false exactly when every active s-t path in HE uses e. Hence, in both cases, τ is counterfactual exactly when every active s-t path uses e. Suppose ans(E) = 0 and the current literal of τ disables e. Toggling τ can activate only e. If the toggle creates an active s-t path π, then e ∈ π, the candidate activation literal is the only activation literal of π not satisfied by E, and every other edge of π is already active. Conversely, if a potential path π has the complementary candidate activation literal as its only unsatisfied activation literal, toggling τ satisfies that literal and activates every edge of π. The outcome changes from 0 to 1. These two implications prove the auxiliary criterion. Item 6. Let Hn = (Vn , Ln ), where Vn = {a0 , . . . , an , u1 , . . . , un , v1 , . . . , vn } and, for every 1 ≤ i ≤ n, Ln contains exactly (ai−1 , ui ), (ui , ai ), (ai−1 , vi ), (vi , ai ). Let s = a0 and t = an . In layer i, every ai−1 -ai path uses exactly one of ai−1 → ui → ai and ai−1 → vi → ai . Since consecutive layers meet only at ai , every simple a0 -an path chooses one branch in each layer, and every vector in {0, 1}n determines one such path. This is a bijection, thus Hn has exactly 2^n simple s-t paths. Distinct paths have distinct edge families and therefore distinct terms Cπ . Item 1 gives |Prime1IHn ,En | = 2^n for En = ∅. Proof of Theorem 5 Let τ ∈ {Ee , Be }, and let m(τ ) be its cut mode. True observed outcome. Assume ans(E) = 1 and ℓE (τ ) enables e. If τ = Ee , then Ee ∈ E, the path term contains Ee , and a cut term with α(e) = edge contains ¬Ee . If τ = Be , then Be ∈ / E, the path term contains ¬Be , and a cut term with α(e) = block contains Be . Therefore, every pair in Q1E,τ has the form (Cπ , D(K,α) ), where e ∈ π ∩ K and α(e) = m(τ ). τ Let f ∈ (π ∩ K) \ {e}. If α(f ) = edge, then Cπ contains Ef and D(K,α) contains ¬Ef . If α(f ) = block, then Cπ contains τ ¬Bf and D(K,α) contains Bf . In both cases, the terms conflict. At e, replacing the candidate literal in the cut term by its complement makes it equal to the path literal. Edges outside π ∩ K occur in at most one term. Therefore, τ Cπ is compatible with D(K,α) ⇐⇒ π ∩ K = {e}.

(54)

Thus, Q1E,τ is in bijection with Weτ . / E] + 1[Bf ∈ E] to the distance. Each f ∈ K \ {e} contributes Let (π, K, α) ∈ Weτ . Each f ∈ π \ {e} contributes 1[Ef ∈ 1[Ef ∈ E] in edge mode and 1[Bf ∈ / E] in blocker mode. These contributions concern distinct atoms because π ∩ K = {e}. At e, we distinguish the two candidate atoms. If τ = Ee , then Ee ∈ E; the candidate cut literal ¬Ee contributes 1 to cE (K, α) and is removed by switching and by dE,−τ , while the noncandidate path literal ¬Be contributes 1[Be ∈ E] to both sides. If τ = Be , then Be ∈ / E; the candidate cut literal Be contributes 1 to cE (K, α); switching it changes the literal to ¬Be , and dE,−τ excludes the candidate coordinate. The noncandidate path literal Ee contributes 1[Ee ∈ / E] to both sides. Thus, the subtraction of one cancels exactly the candidate cut cost and retains the other activation cost at e. Hence, τ dE,−τ (Cπ ⊔ D(K,α) ) = aE (π) + cE (K, α) − 1.

(55)

Item 2 of Theorem 3, together with (54) and (55), proves the formula for a true observed outcome. False observed outcome. Assume ans(E) = 0 and ℓE (τ ) disables e. If τ = Ee , then Ee ∈ / E, the cut term in edge mode contains ¬Ee , and the path term contains Ee . If τ = Be , then Be ∈ E, the cut term in blocker mode contains Be , and the path term contains ¬Be . Every pair in Q0E,τ has the form (D(K,α) , Cπ ), where e ∈ π ∩ K and α(e) = m(τ ). For every f ∈ (π ∩ K) \ {e}, the cut and path literals are complementary under both cut modes, thus they conflict. At e, replacing the candidate literal in Cπ by its complement makes it equal to the cut literal ℓE (τ ). Therefore, D(K,α) is compatible with Cπτ ⇐⇒ π ∩ K = {e}.

(55a)

For a compatible triple, the path and cut literals outside e contribute the activation and disabling costs stated above. At e, we again distinguish the two candidates. If τ = Ee , then Ee ∈ / E; the candidate path literal Ee contributes 1 to aE (π) and is removed by switching and by dE,−τ , while the noncandidate path literal ¬Be contributes 1[Be ∈ E] to both sides. If τ = Be ,

then Be ∈ E; the candidate path literal ¬Be contributes 1 to aE (π); switching it changes the literal to Be , and dE,−τ excludes the candidate coordinate. The noncandidate path literal Ee contributes 1[Ee ∈ / E] to both sides. Thus, the subtraction of one cancels exactly the candidate path cost and retains the other activation cost at e. Hence, dE,−τ (D(K,α) ⊔ Cπτ ) = aE (π) + cE (K, α) − 1.

(55b)

Item 2 of Theorem 3 proves the formula for a false observed outcome. Failed polarity. Assume ans(E) = 1 and ℓE (τ ) disables e. Every prime 1-implicant is a path term, and path terms contain only enabling literals. Thus, no prime implicant of the observed outcome contains ℓE (τ ). Assume ans(E) = 0 and ℓE (τ ) enables e. Every prime 0-implicant is a cut term, and cut terms contain only disabling literals. Again, no prime implicant of the observed outcome contains ℓE (τ ). Item 1 of Theorem 3 gives that τ is not a cause in either case, and κE (τ ) = ∞. Proof of Corollary 3 Let Hn be the graph from Item 6 and let In = IHn ,En , where En = ∅. Every potential edge atom and blocker atom is mutable. The graph has 3n + 1 vertices, 4n potential edges, and 8n mutable atoms, thus |In | = O(n). The program Πbr is independent of n. Given an explicitly represented In and a mutable state F ⊆ Un , perfect-model evaluation is polynomial in |In | because Πbr is fixed; more concretely, it computes directed reachability in the active subgraph induced by F . We next give a polynomial cause-recognition procedure. At En = ∅, the outcome is false. For an edge atom Ee , the current literal is ¬Ee , which disables e. By Item 5 of Theorem 4, Ee is a cause exactly when e belongs to a potential s-t path. The potential graph is acyclic. For e = (u, v), such a path exists exactly when u is reachable from s and t is reachable from v. Two graph searches compute these conditions for every edge in polynomial time. For a blocker atom Be , the current literal is ¬Be , which enables rather than disables e. The failed polarity clause of Theorem 5 gives that no blocker atom is a cause at the false state En . Thus, actual-cause recognition is polynomial for all candidate atoms. The robustness radius is polynomially computable. At En , every edge fact is absent and every blocker is absent, so the false-outcome formula (19) assigns cost 1 to each edge of a potential path. Each potential edge has weight wEn (e) = 1[Ee ∈ / En ] + 1[Be ∈ En ] = 1, thus a shortest-path computation returns the value in Equation (19). More generally, the false-outcome weight is wE (e) = 1[Ee ∈ / E] + 1[Be ∈ E] ∈ {0, 1, 2}, while the true-outcome case uses Equation (18); both are computable in polynomial time. Finally, each diamond contributes one independent binary branch choice. Mapping a binary vector in {0, 1}n to its selected branches is a bijection with the simple s-t paths. Hence, there are exactly 2^n paths. Item 1 of Theorem 4 maps each path to a distinct prime truth term and maps every prime truth term back to a path. Therefore, |Prime1In | = 2^n . Thus, given In , F ⊆ Un , and τ ∈ Un , the value ansIn (F ), the cause status of τ at En , and Rob(En ) are computable in time polynomial in |In |, while the prime truth family has 2^n members. Proof of Theorem 6 We use exactly the programs and predicate arities stated in Equations (22) and (23). Each item has a fixed safe nonrecursive stratified program and a fixed goal predicate. Membership in NP. For Cause, guess Γ ⊆ U \{τ }, evaluate the fixed program on E △Γ and E △(Γ∪{τ }), and verify (2). For Robust, guess J ⊆ U with |J| ≤ k, evaluate the program on E and E △ J, and verify opposite outcomes. For Responsibility, guess Γ ⊆ U \ {τ } with |Γ| ≤ k and verify (2). Each witness has polynomial size, and evaluation of a fixed stratified program is polynomial in the database-level input. Thus, all three problems belong to NP. Item 1: hardness of Cause. Let φ be a CNF formula with variable family V and clause family K. Let Dx contain Var(v),

Clause(c),

Pos(c, v)

and

Neg(c, v)

for the variables, clauses, positive occurrences, and negative occurrences of φ. Let U = {True(v) | v ∈ V } ∪ {Switch},

E = ∅,

A = Goal

and

τ = Switch.

Use the fixed program in Equation (22). It is safe and nonrecursive. A stratification places the extensional predicates in stratum 0, Sat in stratum 1, Bad in stratum 2, and Goal in stratum 3. For a contingency Γ ⊆ {True(v) | v ∈ V }, let νΓ (v) = 1 exactly when True(v) ∈ Γ. For every clause c, the first two rules of (22) give Sat(c) ∈ P(Π ∪ Dx ∪ Γ) ⇐⇒ νΓ satisfies c. Therefore, the third rule gives Bad ∈ P(Π ∪ Dx ∪ Γ) ⇐⇒ νΓ ̸|= φ. Since Switch ∈ / E △ Γ, the goal is false before the candidate toggle. After toggling τ , the final rule gives ans(E △ (Γ ∪ {τ })) = 1 ⇐⇒ νΓ |= φ.

(61)

If φ is satisfiable, the true-variable atoms of a satisfying assignment form a witnessing contingency. Conversely, any witnessing contingency excludes τ and determines, by Equation (61), a satisfying assignment. Thus, τ is a cause exactly when φ is satisfiable.

The construction has one mutable assignment atom per variable, one switch atom, and one exogenous fact per variable, clause, and literal occurrence, and therefore has polynomial size. Item 2: hardness of Robust. We reduce from Vertex Cover restricted to nonempty graphs. The restriction remains NPcomplete under the map (G, k) 7→ (G ∪˙ K2 , k + 1): a cover of G extends by one endpoint of the new edge, and every cover of the disjoint union contains an endpoint of that edge whose removal leaves a cover of G. Let G = (V, EG ) be a nonempty graph. Choose one orientation of each undirected edge and include the corresponding facts Edge(u, v) in Dx . Let U = E = {Keep(v) | v ∈ V } and A = Goal, and use exactly the fixed program in Equation (23). It is safe, nonrecursive, and stratified with Bad below Goal. Since G is nonempty and every keep-atom is initially present, the observed goal is false. For an intervention J ⊆ U, let SJ = {v | Keep(v) ∈ J}. Every atom in J is initially present, thus applying J deletes exactly the keep-atoms of SJ . The two rules of (23) yield ans(E △ J) = 1 ⇐⇒ ¬∃{u, v} ∈ EG (u ∈ / SJ ∧ v ∈ / SJ ) ⇐⇒ ∀{u, v} ∈ EG (u ∈ SJ ∨ v ∈ SJ ) ⇐⇒ SJ is a vertex cover of G.

(62)

A cover of size at most k therefore gives an outcome-changing intervention of size at most k, and every such intervention yields a cover of the same size. Hence, Rob(E) ≤ k exactly when (G, k) is a yes-instance of Vertex Cover. The construction contains |V | mutable atoms and |EG | exogenous edge facts, and is linear. Item 3: hardness of Responsibility. Use the same oriented-edge database and the first rule of Equation (23), and replace its goal rule by the main-text rule Goal ← Switch, ¬Bad. (63) Let U = {Keep(v) | v ∈ V } ∪ {Switch}, E = {Keep(v) | v ∈ V }, A = Goal and τ = Switch. The switch is absent, so the observed goal is false. A contingency Γ ⊆ U \ {τ } deletes precisely the keep-atoms of SΓ = {v | Keep(v) ∈ Γ}, and the goal remains false before the candidate toggle. After toggling τ , ans(E △ (Γ ∪ {τ })) = 1 ⇐⇒ Bad ∈ / P(Π ∪ Dx ∪ (E △ Γ)) ⇐⇒ SΓ is a vertex cover of G,

(64)

where the second equivalence is Equation (62). A cover of size at most k yields a contingency of size at most k, and every witnessing contingency yields a cover of the same size. Thus, κE (τ ) equals the minimum vertex-cover size. The construction is linear in |V | + |EG |, and the program and goal predicate are fixed. The NP upper bounds and the three polynomial reductions prove the theorem. Proof of Theorem 7 Both target programs are fixed, safe, nonrecursive, and stratified. For membership, the complement guesses F ⊆ U. Fixed-program perfect-model evaluation computes ansI1 (F ) and ansI2 (F ) in polynomial time. The verifier accepts exactly when the values differ. Hence, nonequivalence is in NP, and Response-Equivalence is in coNP. For hardness, let φ be a CNF formula with variables x1 , . . . , xn and clauses c1 , . . . , cm . Let Dx contain the facts Var(xi ), Clause(cj ), Pos(cj , xi ) for positive occurrences, and Neg(cj , xi ) for negative occurrences. Let U = {True(xi )|1 ≤ i ≤ n}. For every reduction instance, let A = Goal. The first fixed program is Sat(c) ← Pos(c, x), True(x), Sat(c) ← Neg(c, x), Var(x), ¬True(x), Bad ← Clause(c), ¬Sat(c), Goal ← ¬Bad.

(58)

The final rule is ground and therefore safe. A stratification places extensional predicates in stratum 0, Sat in stratum 1, Bad in stratum 2, and Goal in stratum 3. The program is nonrecursive. For F ⊆ U, let assignment νF make xi true exactly when True(xi ) ∈ F . For each clause cj , the first rule derives Sat(cj ) exactly when cj has a true positive literal, and the second rule derives it exactly when cj has a true negative literal. Therefore, Sat(cj ) ∈ P(Π1 ∪ Dx ∪ F ) ⇐⇒ νF satisfies cj . The third rule derives Bad exactly when some clause is not satisfied. The final rule gives ansI1 (F ) = 1 ⇐⇒ νF |= φ.

(59)

Let Π2 = ∅ over the same common extensional signature and with the same designated goal atom A = Goal. Since Π2 has no rule with head Goal, ansI2 (F ) = 0 for every F ⊆ U. If φ is unsatisfiable, Equation (59) gives ansI1 (F ) = ansI2 (F ) = 0 for every F . If the responses are equal, then ansI1 (F ) = 0 for every assignment state F , and Equation (59) implies that φ is unsatisfiable. The two implications prove both correctness directions. The construction adds one mutable atom per variable and one exogenous fact per variable, clause, and literal occurrence. Its size is linear in the input CNF encoding. Therefore, the reduction is polynomial, and Response-Equivalence is coNP-hard.

C

Proofs of Supplementary Results

Proof of Proposition 4 Let U = {p, q, r}, where p = P (c), q = Q(c), and r = R(c). The two rules of (6) are ground, nonrecursive, and safe. We place the extensional predicates in stratum 0 and Goal in stratum 1. For every F ⊆ U, the first rule derives Goal exactly when p ∈ F , q ∈ / F , and r ∈ / F . The second rule derives Goal exactly when p, q, r ∈ F . Hence, ans(F ) = 1 ⇐⇒ F = {p} or F = {p, q, r}. (30) We first refute (25). The state {p} has outcome 1, whereas its only proper substate ∅ has outcome 0. Thus, {p} is a minimal positive support. The state {p, q} contains that support but has outcome 0 by (30). Consequently, support containment does not imply outcome 1, and (25) fails. Let the observed state be E = ∅. Since E △ J = J, Equation (30) gives ans(E △ J) = 1 ⇐⇒ J = {p} or J = {p, q, r}. The intervention {p} is inclusion-minimal, while {p, q, r} is not inclusion-minimal because {p} ⊊ {p, q, r} already changes the outcome. Therefore, FlipI (E) = {{p}}. In particular, r belongs to no inclusion-minimal outcome-changing intervention. Let Γ = {p, q}. We have r ∈ / Γ and ans(E △ Γ) = ans({p, q}) = 0

and

ans(E △ (Γ ∪ {r})) = ans({p, q, r}) = 1.

Thus, Γ satisfies (2), and r is an actual cause. The same instance establishes both claims of the proposition. Proof of Proposition 5 Let p = P (c), q = Q(c), and Π = {Goal ← P (c), ¬Q(c)}. The program is ground, safe, nonrecursive, and stratified. Direct perfect-model evaluation gives F ans(F ) ∅ 0 {p} 1 {q} 0 {p, q} 0

(31a)

Let C = ({p}, {q}). Every state satisfying C equals {p}, thus C is a 1-implicant. Removing the positive literal p yields (∅, {q}), which is satisfied by ∅ of outcome 0. Removing the negative literal ¬q yields ({p}, ∅), which is satisfied by {p, q} of outcome 0. Thus, both literals are necessary and C is prime. Every 1-implicant must contain the positive literal p: otherwise, it has a satisfying state omitting p, and both such states in Table 31a have outcome 0. Every 1-implicant must also contain the negative literal ¬q: otherwise, it has a satisfying state containing both p and q, whose outcome is 0. Thus, Prime1I = {({p}, {q})}. For outcome 0, let Dp = (∅, {p})

and

Dq = ({q}, ∅).

Every state satisfying Dp omits p and has outcome 0. Removing ¬p yields the empty term, which admits {p} of outcome 1. Thus, Dp is prime. Every state satisfying Dq contains q and has outcome 0. Removing q again yields the empty term and admits {p}. Thus, Dq is prime. Let D be any 0-implicant. If D contains neither ¬p nor q, then {p} satisfies D, contradicting its outcome 1. Thus, Dp ⪯ D or Dq ⪯ D. Primeness permits no proper implicant subterm, thus every prime 0-implicant equals Dp or Dq . Therefore, Prime0I = {Dp , Dq }. The unique prime truth implicant contains the negative literal ¬q, and the prime falsity implicant Dq contains the positive literal q.

Proof of Proposition 6 We prove the two product identities by both inclusions and verify primeness in each direction. The remaining identities follow from duality and Boolean negation. Conjunction truth implicants. Let M11 = {Cf ⊔ Cg | Cf ∈ Prime1 (f ), Cg ∈ Prime1 (g), Cf , Cg compatible}. Every M ∈ M11 is a 1-implicant of f ∧ g: a state satisfying M satisfies both constituent terms, thus it has f = g = 1. Let C ∈ Prime1 (f ∧ g). Since C forces f ∧ g = 1, it separately forces f = 1 and g = 1. Finite minimization among the subterms of C yields Cf ∈ Prime1 (f ) and Cg ∈ Prime1 (g) with Cf ⪯ C and Cg ⪯ C. Both are subterms of the common term C, thus they are compatible and M0 = Cf ⊔ Cg ⪯ C. Choose a ⪯-minimal member M of M11 satisfying M ⪯ M0 ; such a member exists because M0 belongs to the finite family. No member of M11 is properly below M , since any such member would also be below M0 . Thus, M ∈ Min⪯ (M11 ). The first paragraph shows that M is a 1-implicant of f ∧ g. Since M ⪯ C and C is prime, M = C. Hence, Prime1 (f ∧ g) ⊆ Prime1 (f ) ⊗ Prime1 (g). For the reverse inclusion, let M ∈ Prime1 (f ) ⊗ Prime1 (g). The first paragraph shows that M is a 1-implicant of f ∧ g. Suppose a proper subterm M ′ ≺ M were also a 1-implicant. The term M ′ separately forces f = 1 and g = 1. Among its finitely many subterms that force f = 1, choose a prime one Cf′ ∈ Prime1 (f ); among its subterms that force g = 1, choose a prime one Cg′ ∈ Prime1 (g). Then, Cf′ , Cg′ ⪯ M ′ . Their merge M0′ belongs to M11 and satisfies M0′ ⪯ M ′ ≺ M . A minimal member of M11 below M0′ belongs to the product and is properly below M , contradicting the defining minimality of M . Therefore, M is prime, and Prime1 (f ∧ g) = Prime1 (f ) ⊗ Prime1 (g). Disjunction falsity implicants. Let M00 = {Df ⊔ Dg | Df ∈ Prime0 (f ), Dg ∈ Prime0 (g), Df , Dg compatible}. Every member of M00 forces f = 0 and g = 0, and therefore forces f ∨ g = 0. Let D ∈ Prime0 (f ∨ g). The term D separately forces f = 0 and g = 0. Choose prime subterms Df ∈ Prime0 (f ) and Dg ∈ Prime0 (g) below D. They are compatible, their merge is below D, and a minimal member of M00 below that merge is a 0-implicant of f ∨ g. Primeness of D forces equality, yielding Prime0 (f ∨ g) ⊆ Prime0 (f ) ⊗ Prime0 (g). Conversely, let M ∈ Prime0 (f ) ⊗ Prime0 (g). It is a 0-implicant of f ∨ g. If a proper subterm M ′ ≺ M were a 0-implicant, then M ′ would separately force f = 0 and g = 0. Prime minimization below M ′ would produce a member of M00 , and then a product member, properly below M , a contradiction. Hence, M is prime, and Prime0 (f ∨ g) = Prime0 (f ) ⊗ Prime0 (g). Remaining identities. Proposition 1 gives Prime0 (h) = Dual(Prime1 (h)) and Prime1 (h) = Dual(Prime0 (h)) for every Boolean response h. Applying these equalities to the two identities already proved yields

Prime0 (f ∧ g) = Dual Prime1 (f ∧ g) = Dual Prime1 (f ) ⊗ Prime1 (g) ,

Prime1 (f ∨ g) = Dual Prime0 (f ∨ g) = Dual Prime0 (f ) ⊗ Prime0 (g) . Finally, for every term C,

C is a b-implicant of ¬f ⇐⇒ ∀F |= C, 1 − f (F ) = b ⇐⇒ ∀F |= C, f (F ) = 1 − b ⇐⇒ C is a (1 − b)-implicant of f.

The equivalence is unchanged for every proper subterm of C, so it also preserves primeness. Therefore, Primeb (¬f ) = Prime1−b (f ). Proof of Proposition 7 Let Conditions 1–4 be those in Proposition 7. Condition 1 and Condition 4 are identical after taking the empty contingency in Definition 2. We prove 1 ⇒ 2, 1 ⇒ 3, 2 ⇒ 1, and 3 ⇒ 1. Assume Condition 1. Choose F ⊆ U with ans(F ) ̸= ans(F △ {τ }), and let b = ans(F ). By the prime cover, choose C ∈ PrimebI with F |= C. If C contained no literal on τ , toggling τ would preserve satisfaction of every literal of C, thus F △ {τ } |= C. The implicant property would then give ans(F △ {τ }) = b, a contradiction. Thus, C contains a literal on τ . If b = 1, then C ∈ Prime1I establishes Condition 2. If b = 0, then C ∈ Prime0I establishes Condition 3. Let G = F △ {τ }. Its outcome is 1 − b. By the prime cover, choose D ∈ Prime1−b with G |= D. If D contained no literal I on τ , then F |= D, because F and G differ only on τ . The implicant property would give ans(F ) = 1 − b, contradicting

ans(F ) = b. Thus, D contains a literal on τ . If b = 1, then D ∈ Prime0I establishes Condition 3; if b = 0, then D ∈ Prime1I establishes Condition 2. Therefore, Condition 1 implies both Conditions 2 and 3 for both values of b. Assume Condition 2. Let C ∈ Prime1I contain a literal Lτ on τ , and let C−τ be the proper subterm obtained by deleting that literal. Since C is prime, C−τ is not a 1-implicant. Thus, some state G satisfies C−τ and has outcome 0. If G satisfied Lτ , then G |= C, contradicting the implicant property of C. Hence, G satisfies the complementary literal on τ , and G △ {τ } |= C. We obtain ans(G) = 0 and ans(G △ {τ }) = 1, which is Condition 1. Assume Condition 3. Let D ∈ Prime0I contain a literal Lτ , and let D−τ delete it. Primeness gives a state G |= D−τ with outcome 1. The state G cannot satisfy Lτ , because then G |= D would force outcome 0. Therefore, G △ {τ } |= D, and ans(G) = 1

and

ans(G △ {τ }) = 0.

Condition 1 follows. All four conditions are equivalent. We finally prove the quantified consequence. Let F, J ⊆ U, and enumerate J \ RelI = {u1 , . . . , um }. Let J0 = J,

and

Jj = Jj−1 \ {uj }

(1 ≤ j ≤ m).

For 0 ≤ j ≤ m, let Gj = F △ Jj . The states Gj−1 and Gj differ only on uj . Since uj ∈ / RelI , Condition 1 fails at every state, and therefore ans(Gj−1 ) = ans(Gj ). Induction on j yields ans(F △ J) = ans(F △ Jm ). Since Jm = J ∩ RelI , we obtain ans(F △ J) = ans(F △ (J ∩ RelI )). Proof of Corollary 4 Let I1 and I2 share Dx , U, E, and A. Assume Prime1I1 = Prime1I2 . For every state F ⊆ U , the prime cover gives ansI1 (F ) = 1 ⇐⇒ ∃C ∈ Prime1I1 (F |= C) ⇐⇒ ∃C ∈ Prime1I2 (F |= C) ⇐⇒ ansI2 (F ) = 1. The responses are Boolean, so they agree on F . Since F was arbitrary, they agree on every mutable state. If Prime0I1 = Prime0I2 , then for every F ⊆ U , ansI1 (F ) = 0 ⇐⇒ ∃C ∈ Prime0I1 (F |= C) ⇐⇒ ∃C ∈ Prime0I2 (F |= C) ⇐⇒ ansI2 (F ) = 0. Booleanity again gives response equality. Conversely, assume ansI1 (F ) = ansI2 (F ) for every F ⊆ U . For every term C and b ∈ {0, 1}, C is a b-implicant of I1 ⇐⇒ ∀F |= C, ansI1 (F ) = b ⇐⇒ ∀F |= C, ansI2 (F ) = b ⇐⇒ C is a b-implicant of I2 . The two instances use the same subterm order. Thus, a b-implicant has a proper b-implicant subterm in one instance exactly when it has one in the other. Thus, PrimebI1 = PrimebI2 for b = 0, 1. Equation (9) also proves directly that equality of either polarity is equivalent to equality of the other. Assume the equivalent response-equality conditions. Let τ ∈ U and Γ ⊆ U \ {τ }. Both instances assign the same outcome to E △ Γ and to E △ (Γ ∪ {τ }). Therefore, Γ satisfies the two causality equations for I1 exactly when it satisfies them for I2 . The feasible contingency families are identical for every candidate. Their minimum cardinalities are consequently equal, including the common value ∞ when the family is empty. Equation (3) then gives equal responsibilities and equal actual-cause families. Likewise, for every intervention J ⊆ U, ansI1 (E △ J) ̸= ansI1 (E) ⇐⇒ ansI2 (E △ J) ̸= ansI2 (E). Thus, the outcome-changing intervention families coincide, and their minimum cardinalities, including ∞, are equal. The robustness radii agree.

Proof of Corollary 5 Let b = ans(E). Assume first that b = 1. Let τ ∈ / E, and let Γ ⊆ U \ {τ } be arbitrary. Since τ ∈ / E and τ ∈ / Γ, the state F = E △ Γ omits τ , and F △ {τ } = F ∪ {τ }. If Γ preserved the observed outcome, then ans(F ) = 1. Monotonicity gives 1 = ans(F ) ≤ ans(F ∪ {τ }) ≤ 1, so the candidate toggle cannot produce outcome 0. Thus, no atom outside E is a cause, and every actual cause belongs to E. Let τ ∈ E. Then, ℓE (τ ) = τ . By Theorem 3, τ is a cause exactly when a prime 1-implicant contains the positive literal τ . By Corollary 2, the prime 1-implicants are exactly (S, ∅) for S ∈ SuppI . Therefore, τ is a cause ⇐⇒ ∃S ∈ SuppI (τ ∈ S). Assume now that b = 0. Let τ ∈ E, and let Γ ⊆ U \ {τ }. The state F = E △ Γ contains τ , and F △ {τ } = F \ {τ }. If Γ preserved the observed outcome, then ans(F ) = 0. Monotonicity gives 0 ≤ ans(F \ {τ }) ≤ ans(F ) = 0, thus deleting τ cannot produce outcome 1. Thus, every actual cause lies in U \ E. Let τ ∈ / E. Then, ℓE (τ ) = ¬τ . By Theorem 3, τ is a cause exactly when a prime 0-implicant contains ¬τ . Corollary 2 identifies every prime 0-implicant with (∅, T ) for T ∈ Tr(SuppI ). Such a term contains ¬τ exactly when τ ∈ T . Consequently, τ is a cause ⇐⇒ ∃T ∈ Tr(SuppI ) (τ ∈ T ). The two outcome cases and both candidate polarities are exhausted. Proof of Proposition 8 Let ∆ be the active domain of (Π, Dx , U, A), and let N = |∆|. Since Π is fixed, predicate arities, rule lengths, and the numbers of variables per rule are constants. If a rule has at most d variables, it has at most N d ground instances. Thus, the complete grounding contains polynomially many ground atoms and ground rules. For every ground extensional atom L, construct its gate as follows. If L ∈ U, use the input gate XL . If L ∈ Dx , use constant 1. Every other extensional atom uses constant 0. Under input χF , these gates compute membership in Dx ∪ F . Renumber the stratification so that all intensional predicates have positive strata and the used intensional strata are 1, . . . , s. We prove gate correctness by outer induction on the stratum. The outer induction hypothesis states that, for every ground atom in a stratum below i, its final gate computes its completed perfect-model truth value for every input state. The hypothesis is vacuous for the least intensional stratum. Let Bi be the family of ground intensional atoms in stratum i, and let mi = |Bi |. For H ∈ Bi , let GH,0 = 0. For 1 ≤ t ≤ mi , let _ GH,t = GH,t−1 ∨ Bodyρ,t−1 , (56) ρ∈Gri (H)

where Gri (H) is the family of ground stratum-i rules with head H. The empty disjunction is 0, and an empty body has gate 1. For a nonempty ground body, use a conjunction of one gate per body atom. The following cases exhaust safe stratified rule syntax. 1. A positive extensional atom uses its input or constant membership gate. 2. A positive lower-stratum atom uses its completed final gate. 3. A positive stratum-i atom uses its round-(t − 1) gate. 4. A negated extensional atom uses the Boolean negation of its extensional membership gate. 5. A negated intensional atom belongs to a lower stratum by stratification and uses the Boolean negation of its completed final gate. No negated current- or higher-stratum atom is permitted by stratification. For a state F ⊆ U, let Ti,F be the inflationary immediate-consequence operator for stratum i, with extensional facts and completed lower strata held constant. We prove simultaneously for every H ∈ Bi and every t ∈ {0, . . . , mi } that t GH,t (χF ) = 1 ⇐⇒ H ∈ Ti,F (∅).

(57)

0 For t = 0, the left side is false because GH,0 = 0, and the right side is false because Ti,F (∅) = ∅. Assume (57) for every stratum-i atom at round t − 1. Let ρ be a ground rule. We verify its body gate atom by atom. Case 1 is true exactly when the extensional atom belongs to Dx ∪ F , by the extensional gate definition. Case 2 is true exactly when the lower-stratum atom belongs to its completed relation, by the outer induction hypothesis. Case 3 is true exactly when the t−1 atom belongs to Ti,F (∅), by the inner induction hypothesis. Cases 4 and 5 negate the exact truth values from Cases 1 and 2. A conjunction gate is therefore true exactly when every positive body atom is present and every negated body atom is absent in the round-(t − 1) interpretation. This is exactly the satisfaction condition for the body of ρ. Equation (56) is true exactly when either H was present at round t − 1, or some rule with head H has a body true at that t round. This condition is equivalent to H ∈ Ti,F (∅), proving the inner induction step.

The operator Ti,F is inflationary on the finite family Bi . Every strict increase adds at least one new atom, so it has at most mi strict increases. Hence, mi mi +1 Ti,F (∅) = Ti,F (∅). The stabilized relation is the least fixpoint for stratum i. Let GH = GH,mi . Equation (57) shows that GH computes the completed truth value of H. Thus, the outer induction hypothesis holds for stratum i. Induction over all strata proves that the final gate for A, denoted CΠ,Dx ,U ,A , satisfies (21) for every state F . For the size bound, let Ri be the number of ground rules in stratum i, and let b0 be the maximum rule-body length, a constant. At each of the mi rounds, the construction uses at most O(Ri b0 ) body and combination gates. Thus, stratum i uses O(mi Ri b0 ) gates. The number of strata is constant, and every mi and Ri is polynomial in the grounding size. The total circuit size and construction time are therefore polynomial in |Dx | + |U | + |A|. Proof of Proposition 9 Let an assignment to the circuit inputs represent FX = {u ∈ U | Xu = 1}. For eu = χE (u), the Boolean value Xu ⊕ eu equals 1 exactly when u belongs to the symmetric difference FX △ E. Therefore, X (Xu ⊕ eu ) = |FX △ E|. (60) u∈U

Proposition 8 gives C(X) = ans(FX ). Item 1, forward direction. Assume (28) is satisfiable, and let X be a satisfying assignment. Let F = FX and J = E △ F . Symmetric-difference identities give E △ J = F . Equation (60) and the cardinality constraint give |J| ≤ k. The output constraint gives ans(E △ J) = ans(F ) = C(X) = 1 − b. Thus, J is an outcome-changing intervention of size at most k, and Rob(E) ≤ k. Item 1, reverse direction. Assume Rob(E) ≤ k. Choose J ⊆ U with |J| ≤ k and ans(E △ J) = 1 − b. Let F = E △ J and X = χF . Circuit correctness gives C(X) = 1 − b. Since F △ E = J, Equation (60) gives X (Xu ⊕ eu ) = |J| ≤ k. u∈U

Thus, X satisfies (28). Item 2, forward direction. Assume (29) is satisfiable, and let X be a satisfying assignment. Let F = FX and Γ = E △ F . The equality Xτ = eτ means that F and E agree on τ , thus τ ∈ / Γ. The first output constraint gives ans(E △ Γ) = ans(F ) = b. Complementing input coordinate τ represents F △ {τ } = E △ (Γ ∪ {τ }), because τ ∈ / Γ. The second output constraint therefore gives ans(E △ (Γ ∪ {τ })) = 1 − b. For every u ̸= τ , the summand Xu ⊕ eu indicates membership of u in Γ, while the candidate summand is zero. Hence, the cardinality sum equals |Γ| ≤ k. Thus, Γ is a witnessing contingency and κE (τ ) ≤ k. Item 2, reverse direction. Assume κE (τ ) ≤ k. Choose a contingency Γ ⊆ U \ {τ } with |Γ| ≤ k satisfying (2). Let F = E △ Γ and X = χF . Since τ ∈ / Γ, Xτ = eτ . Circuit correctness and (2) give C(X) = b

and

C(X ⊕τ ) = 1 − b.

Equation (60), restricted to U \ {τ }, gives the cardinality value |Γ| ≤ k. Hence, X satisfies (29). If the cardinality constraint is removed from (29), satisfiability is equivalent to the existence of some contingency, with no bound on its size. This is exactly the decision problem Cause. For a CNF translation, introduce one Tseitin variable for every circuit gate and clauses enforcing the corresponding gate equivalence. Introduce deviation variables Yu ↔ (Xu ⊕eu ), and encode the relevant cardinality constraint with any polynomialsize Boolean cardinality encoding. These clauses preserve satisfiability in both directions because every assignment of the input variables extends uniquely to the gate values, and every satisfying Tseitin assignment restricts to the encoded circuit computation. For unweighted MaxSAT, keep all circuit, output, candidate, and coordinate constraints hard, and add the unit soft clause ¬Yu for every permitted deviation. A feasible assignment violates exactly one soft clause per changed atom. Under the convention that an infeasible hard part represents value ∞, the optimum represents Rob(E) for the robustness encoding and κE (τ ) for the contingency encoding. The circuit and all auxiliary encodings have polynomial size.

Proof of Proposition 10 Let U = {p, q, r}, E = {p}, and Dx = ∅. Let Π1 = {A ← p}, and let Π2 = Π1 ∪ {A ← q, r}. For every F ⊆ U , ansI1 (F ) = 1 ⇐⇒ p ∈ F and ansI2 (F ) = 1 ⇐⇒ p ∈ F ∨ {q, r} ⊆ F. (47) Both observed outcomes equal 1. For candidate p, the empty contingency satisfies ansIj (E) = 1

and

ansIj (E △ {p}) = ansIj (∅) = 0

(j = 1, 2).

Thus, p is counterfactual in both instances, κIE1 (p) = κIE2 (p) = 0

and

RespIE1 (p) = RespIE2 (p) = 1.

(48)

We prove that q is not a cause in either instance. Let Γ ⊆ U \ {q}, and let F = E △ Γ. A witnessing contingency would require ansIj (F ) = ansIj (E) = 1. Since q ∈ / F , toggling q produces F ∪ {q}. Both responses in (47) are monotone, thus ansIj (F ) ≤ ansIj (F ∪ {q})

(j = 1, 2).

The left side equals 1, and thus the right side also equals 1. Toggling q cannot reverse the observed outcome after any contingency. Therefore, q is not a cause in either instance. For r, let Γ ⊆ U \ {r} and F = E △ Γ. A witnessing contingency requires ansIj (F ) = 1. Since r ∈ / F , monotonicity gives ansIj (F ) ≤ ansIj (F ∪ {r}). Thus, inserting r also preserves outcome 1, and r is not a cause in either instance. Thus, both instances have exactly the cause p, and both assign responsibility 0 to q and r. Toggling p changes the observed outcome in both instances, so each robustness radius is at most 1. An intervention of size 0 leaves the observed true outcome unchanged, so each radius is at least 1. Hence, RobI1 (E) = RobI2 (E) = 1.

(49)

At the state F = {q, r}, Equation (47) gives ansI1 (F ) = 0 and ansI2 (F ) = 1. Therefore, the two full responses differ although their actual causes, responsibility values, and robustness radii agree at E. Proof of Theorem 8 The input is (Dx , U, A, C, b), while the safe nonrecursive stratified program and the goal predicate are fixed. We prove coNP membership by a counterexample state and coNP-hardness by a reduction from CNF unsatisfiability. For membership, the complement guesses F ⊆ U , verifies F |= C, evaluates the fixed program on Dx ∪ F , and accepts when ans(F ) = 1 − b. The witness has |U | bits, term satisfaction is polynomial, and fixed-program evaluation has polynomial data complexity. Thus, non-implicanthood is in NP, and Implicant is in coNP. For hardness, let φ be a CNF formula with variable family V and clause family K. Let Dx contain the facts Var(v), Clause(k), Pos(k, v), and Neg(k, v) determined by the formula. Let U = {True(v)|v ∈ V }, let C = ϵ, let b = 0, and let A = Goal. Use the fixed program Sat(k) ← Pos(k, v), True(v), Sat(k) ← Neg(k, v), Var(v), ¬True(v), Bad ← Clause(k), ¬Sat(k), Goal ← ¬Bad. The program is safe and nonrecursive. A stratification places the extensional predicates in stratum 0, Sat in stratum 1, Bad in stratum 2, and Goal in stratum 3. For every state F ⊆ U , the derivation used in Equation (59) gives ans(F ) = 1 ⇐⇒ F encodes a satisfying assignment of φ. Since every state satisfies the empty term, ϵ is a 0-implicant ⇐⇒ ans(F ) = 0 for every F ⊆ U ⇐⇒ φ is unsatisfiable. The empty term has no proper subterm, so it is prime whenever it is an implicant. The construction contains one mutable atom per variable and one exogenous fact per variable, clause, and literal occurrence. It is polynomial. CNF unsatisfiability is coNP-complete, thus Implicant is coNP-hard.

Related documents

• Causal Explanations for Stratified Datalog#662307
• Causal Explanations for Stratified Datalog#661257
• Omissions and Causal Explanations#775060
• Causal Overdetermination and Kim’s Exclusion Argument#763507
• Counterfactual Explanation in Literature and the Social Sciences#720668