On the Complexity of Global Necessary Reasons to Explain Classification

Cristian Molinaro; Enrico Malizia; Marco Calautti

REVIEW 2 major objections 4 minor 1 cited by

On the Complexity of Global Necessary Reasons to Explain Classification

T0 review · 2 major / 4 minor · reviewed 2026-08-10 · deepseek-v4-flash

Challenge this review Re-run · record.json Download PDF Read on arXiv ↗ Review JSON

Pith's one-line read Checking and minimizing global necessary reasons ranges from logarithmic space for perceptrons to co-NP- and DP-completeness for multilayer perceptrons.

desk verdict Nice complexity map for global necessary reasons, but Theorem 4.2's proof as written is wrong — the implication graph is directed, not undirected, so the logspace upper bounds are currently unsupported. read the letter →

arxiv 2501.06766 v1 pith:KK2BDWJR submitted 2025-01-12 cs.AI

Marco Calautti , Enrico Malizia , Cristian Molinaro This is my paper · ORCID

classification cs.AI MSC 68Q1768Q2568T05

keywords globalnecessaryreasonsexplainableAIcomputationalcomplexitybinarydecisiondiagramsperceptronmultilayerlogspaceminimalexplanations

verification ladder T0 review T1 audit T2 compute T3 formal

The pith

A machine-rendered reading of the paper's core claim, the machinery that carries it, and where it could break.

The reading

The paper asks how hard it is to decide that a logical condition is a global necessary reason for a classifier to output a class—meaning every instance given that class must satisfy the condition—and how hard it is to find the most informative such reason. It establishes a complete complexity map: the decision problems are in logarithmic space for perceptrons, NL-complete for binary decision diagrams, and co-NP-complete for multilayer perceptrons, with minimality pushing only the MLP case up to DP-complete. The two natural minimality criteria, fewer satisfying instances and a subset of satisfying instances, turn out to select exactly the same reasons and to have the same complexity. This matters because global necessary reasons can expose biases in a classifier, and the map says when such reasons can be computed quickly, in parallel, or only by SAT-style search.

What carries the argument

The central object is the condition language $\mathcal{L}[n]$: conjunctions of literals of the form $t \Diamond t'$ with $\Diamond \in \{=,\ne\}$ and terms drawn from feature variables and constants $0,1$. The paper's pivotal lemma says that a global necessary reason $\varphi$ is minimal under either preorder exactly when no single literal $\ell$ that $\varphi$ does not entail is itself a global necessary reason; this turns every minimality question into $O(n^2)$ checks of single literals. The entailment check $\varphi \models \ell$ is shown to be in L by translating it into a two-literal conjunctive normal form whose implication graph has symmetric edges, making it an undirected graph whose reachability is decided in logarithmic space. For BDDs, the non-necessity of $\varphi$ is characterized by an accepting path whose conjunction of feature assignments fails to entail some literal entailed by $\varphi$, and an NL algorithm guesses that path. For MLPs, the hardness proofs run through the polynomial-time encoding of arbitrary Boolean formulas as ReLU/Heaviside networks, transferring satisfiability hardness to the explanation problem.

What would settle it

An exact check would enumerate all small perceptrons, BDDs, and MLPs together with all conditions in $\mathcal{L}[n]$, compute global necessity and both kinds of minimality by brute force, and compare against the paper's algorithms. One mismatch—for instance a condition that is minimal despite some non-entailed literal being necessary, or a BDD whose path characterization fails—would refute the key lemma and the complexity classification built on it.

Watch

Extended reading notes

Core claim

The central claim is a complete complexity classification for global necessary reasons expressed as conjunctions of equalities and inequalities over feature variables and constants (the condition language $\mathcal{L}[n]$). For perceptrons, deciding whether a given condition is a global necessary reason is in L (deterministic logarithmic space), and deciding minimality stays in L. For free binary decision diagrams both problems are NL-complete. For multilayer perceptrons with rectified-linear hidden activations and a step output, necessity is co-NP-complete and minimality is DP-complete, where DP is the class of problems formed by combining one NP and one co-NP problem. The paper also proves that the two minimality preorders—comparing numbers of models and comparing model sets—are equivalent for this language, and that computing a minimal reason is polynomial-time with an oracle for the arbitrary-necessity problem, hence polynomial for perceptrons and BDDs and SAT-solver-accessible for MLPs.

Load-bearing premise

The load-bearing premise is that an explanation is a conjunction of equalities and inequalities; every equivalence, logspace algorithm, and completeness proof in the paper depends on that restriction, and the MLP hardness also assumes that arbitrary Boolean formulas can be encoded as polynomial-size ReLU/Heaviside networks.

Editorial extensions

If this is right

Minimal global necessary reasons for perceptrons and BDDs are computable in polynomial time, so auditing these classifiers for necessary conditions is practical.
For MLPs, minimal global necessary reasons are computable in polynomial time with a co-NP oracle; in practice this means SAT solvers, since the decision problem for arbitrary reasons is co-NP-complete.
The two minimality criteria—fewest satisfying instances and subset of satisfying instances—lead to identical minimal explanations, so model counting is not needed to pick the most informative condition.
Minimality adds no complexity for perceptrons or BDDs, but it moves MLPs from co-NP-complete to DP-complete, so the extra demand is real only for the expressive family.
Computing a minimal reason is at least as hard as deciding whether a given reason is minimal, and is no harder than a polynomial number of calls to the arbitrary-necessity oracle; the decision and search problems therefore have matching practical strategies.

Reading between the lines

Editorial extensions of the paper, not claims the author makes directly.

Editorial inference: the restriction to conjunctions is what keeps the picture tractable; allowing disjunctions would let conditions encode arbitrary classifier behavior, and the logspace/undirected-graph argument would not survive.
Editorial inference: because the two preorders coincide, a greedy extraction loop that repeatedly conjoins any literal that keeps the condition necessary should find a minimal reason; this is a direct implementation recipe the paper does not benchmark.
Editorial inference: for MLPs, the DP-complete characterization suggests encoding non-minimality as a SAT instance and using an off-the-shelf solver, which would be a natural experimental follow-up.
Editorial inference: the results give a formal way to audit bias—finding minimal necessary reasons for a sensitive class on linear classifiers and BDDs is cheap, so fairness checks could run at scale; the paper does not discuss this application.

Share X Bluesky LinkedIn Reddit HN

Editorial analysis

A structured set of objections, weighed in public.

Desk editor's note, referee report, and a circularity audit.

Desk Editor's Note

read the letter

Two things to know. First, the paper delivers the first full complexity map for global necessary reasons: L for perceptrons, NL-complete for BDDs, co-NP-complete and DP-complete for MLPs. The minimality characterization (Lemma 4.1) is genuinely useful — it reduces minimality to checking whether any non-entailed literal is itself a necessary reason, and it correctly shows cardinality and subset minimality coincide for this language. Second, the proof of Theorem 4.2, the logspace entailment lemma that carries every upper bound, has a real gap. The stress-test example lands. For φ=(v1=1)∧(v1=v2), ℓ=(v2=1), the constructed ψ is x1∧(x1→x2)∧(x2→x1)∧¬x2, which is unsatisfiable. But the claimed undirected implication graph has directed edges ¬x1→x1 and x2→¬x2 from the unit clauses, plus the symmetric pair x1↔x2. There is no path from ¬x2 to x2, so the undirected reachability test misses the contradiction. The paper's claim that every implication has a symmetric counterpart is simply false once unit clauses appear. This is not cosmetic: Theorem 4.2 feeds the perceptron upper bound, Algorithm 2 for BDDs, and the generic minimality procedure. Without a valid L-membership proof, the PRC results and the BDD upper bounds lack support. The lower-bound reductions look careful, and the theorem is likely repairable — the condition language is a system of equalities/inequalities over Boolean variables, i.e. parity constraints, and undirected parity reachability is plausibly in L. But as written the proof fails.

What the paper does well: the related-work separation from INM19 and BAK24 is clear and honest; the BDD characterization (Lemma 4.5) is elegant; the hardness reductions are standard and give genuine completeness; the reliance on free BDDs and the external MLP encoding lemma are explicit and defensible. The appendix is detailed and readable.

Who is this for: people in formal explainability who need to know when global necessary reasons are tractable. For them the complexity map matters, and most of it will survive a proof repair. The paper deserves a serious referee, but only with the explicit instruction that Theorem 4.2 be rewritten and checked. I would not cite it until that fix lands.

Referee Report

2 major / 4 minor

Summary. This paper studies global necessary reasons for binary classifiers, expressed as conjunctions of equalities and inequalities over feature variables. It introduces two decision problems, Necessity[C] and MinNecessity[C,≤/⊆], for C ∈ {PRC, BDD, MLP}, and claims a complete complexity classification: the problems are in L for perceptrons, NL-complete for BDDs, and co-NP-complete / DP-complete for MLPs. The technical core is a characterization (Lemma 4.1) that reduces minimality to checking whether any single literal is a global necessary reason, a claimed logspace entailment test for the condition language (Theorem 4.2), and reductions for each classifier family. The paper also draws conclusions about computing minimal global necessary reasons with oracles.

Significance. If the classification were fully established, this would be a valuable systematic contribution: it gives a complete complexity picture for a global explainability notion, shows that the two minimality criteria collapse, and yields efficient parallel/SAT-based algorithmic insights for perceptrons, BDDs, and MLPs. The Lemma 4.1 literal-characterization is an elegant and reusable tool, and the high-level framing is clear. However, the specific proof gaps identified below mean that several central claims are not yet supported by the manuscript; the results are plausible and likely repairable, but the paper as written overstates the rigor of its upper and lower bounds.

major comments (2)

[Appendix A, proof of Theorem 4.2] The proof asserts that the implication graph of the constructed 2CNF formula ψ is undirected, because every implication has a symmetric counterpart. This is not the case. Unit clauses occur whenever a literal fixes a feature (e.g., φ contains v1=1) or when the negated conclusion is a unit, and a unit clause x adds only the directed edge ¬x→x. Moreover, the encoding of vi=vj lists xi→xj and xj→xi but omits the contrapositive edges ¬xj→¬xi and ¬xi→¬xj that belong to the standard implication graph. Concretely, take φ=(v1=1)∧(v1=v2) and ℓ=(v2=1); then φ|=ℓ, but the graph containing x1→x2, x2→x1, ¬x1→x1, and x2→¬x2 has no path from ¬x2 to x2, so the claimed undirected reachability test does not detect the unsatisfiability of ψ. Since Theorem 4.2 is used in Theorems 4.3, 4.4, Algorithm 2, Theorem 4.7, and Theorem 4.9, the L and NL upper bounds are not established by the given argument. The conclusion may be repairable by viewing the constraints as parity (XOR) constraints and using logspace solvability of undirected parity reachability, but the current proof is invalid as written.
[Appendix A, proof of Theorem 4.6 (hardness)] The reduction from UniformRootedAcyclicReach to NotNecessity[BDD] connects every sink of the uniform RDAG to uyes, not only the designated sink t. Therefore a path from the root s through the distinguished edge e to any other sink u (followed by the edge to uyes) witnesses that φ=(s=0) is not a global necessary reason, even if no path from s to t traverses e. In the “only if” direction, after removing uyes the path may end at u rather than at t, and the proof incorrectly identifies an arbitrary sink with the given sink t. This breaks the claimed NL-hardness. The construction can likely be repaired by connecting only the designated sink t to uyes and all other sinks to uno, or by proving that a unique-sink version of UniformRootedAcyclicReach is NL-hard, but as written the lower bound of Theorem 4.6 is unsupported. The adaptation used in the hardness proof of Theorem 4.7 should be re-examined in light of the same issue.

minor comments (4)

[Section 4 and Theorem 4.9 proof] Several cross-references call Lemma 4.1 and Lemma 4.5 “Theorem 4.1” and “Theorem 4.5”; please make the numbering consistent throughout the text.
[Algorithm 1] Line 2 says “foreach literal ℓ∈L[n]”, but L[n] is the set of conditions (conjunctions), not the set of literals; the quantification should be over the O(n²) literals of the language.
[Section 4.2, A Note on Decision Trees] The claim that one can iterate over all leaves of a decision tree in logarithmic space deserves a short justification, since the naive traversal of a tree with exponentially many leaves is not obviously logspace.
[Lemma A.3] The notation used for replacing high-outdegree nodes, with u∗₀=u and u∗ₙ₋₁=vₙ, is terse; a small example or a restated indexing scheme would greatly improve readability.

Circularity Check

0 steps flagged · score 0.0 of 10

No significant circularity: the complexity results are proved from first principles with external, independently authored black-box lemmas; no fitted parameter is renamed as a prediction.

full rationale

The paper's derivation chain is self-contained and non-circular. The central definitions (global necessary reasons, minimality) are fixed independently of the complexity outcomes. Lemma 4.1 is proved by set-inclusion and cardinality arguments, not by assuming the decision problems have any particular complexity. Theorem 4.2 reduces literal entailment to 2CNF unsatisfiability and then to reachability; the reduction is constructive and does not presuppose the logspace upper bound it establishes. The PRC upper bounds are obtained by solving explicitly constructed linear inequalities, the BDD bounds by a path/literal characterization plus independent reductions from UniformRootedAcyclicReach, and the MLP bounds by a black-box use of Barceló, Monet, Pérez, and Subercaseaux's Lemma 13, an external result by different authors. There are no fitted parameters, no empirical predictions derived from fitted values, and no self-citation chain that carries a load-bearing premise. The only caveat worth flagging is not circularity: the proof of Theorem 4.2 asserts that every implication has a symmetric counterpart making the implication graph undirected; a skeptical reader could dispute that step (e.g., for unit clauses or omitted contrapositives). That is a potential correctness gap in the proof, not a reduction of the claim to its own input. Likewise, the paper's restriction of the condition language to conjunctions is a design choice motivated by interpretability, not an assumption that entails the complexity results.

Assumptions & free parameters 0 free parameters · 5 assumptions · 0 invented entities

The paper introduces no free parameters and no invented physical entities. Its results rest on standard complexity-theoretic theorems and two domain assumptions: the conjunctive explanation language and the cited MLP encoding lemma.

assumptions (5)

standard math Reingold's theorem: undirected graph reachability is decidable in logarithmic space.
Used in Theorem 4.2 to show that checking φ⊨ℓ is in L by converting to a 2CNF formula whose implication graph is undirected.
domain assumption Barceló et al. (2020) Lemma 13: every Boolean formula can be encoded as an MLP with ReLU hidden activations and a Heaviside output, constructible in polynomial time.
Load-bearing for the hardness reductions in Theorems 4.8 and 4.9, from UNSAT and Sat-UNSAT respectively; treated as a black box from cited prior work.
standard math Standard complexity class facts: L and NL are closed under complement; DP is the class of intersections of an NP and a co-NP language; composition of logspace procedures is logspace.
Used throughout Section 4 to obtain membership and completeness results for the various problems.
domain assumption The definition of free BDD with no repeated feature labels along any path, and exactly one path per instance.
The BDD algorithms and reductions (Theorems 4.6 and 4.7) rely on the free/uniqueness property to read off a path from a witness instance.
domain assumption Restriction of the condition language L[n] to conjunctions of literals, each literal being a comparison between two variables or constants.
The complexity results all depend on the conjunctive language; the paper explicitly chooses this balance between expressiveness and tractability in Section 3.

how reviews work

0 comments

Cite this review

Pith. "Pith review of On the Complexity of Global Necessary Reasons to Explain Classification." pith.science (2026). https://pith.science/paper/KK2BDWJR

@misc{pith2026250106766,
  author       = {Pith},
  title        = {Pith review of: On the Complexity of Global Necessary Reasons to Explain Classification},
  year         = {2026},
  howpublished = {\url{https://pith.science/paper/KK2BDWJR}},
  note         = {Machine review of arXiv:2501.06766}
}

read the original abstract

Explainable AI has garnered considerable attention in recent years, as understanding the reasons behind decisions or predictions made by AI systems is crucial for their successful adoption. Explaining classifiers' behavior is one prominent problem. Work in this area has proposed notions of both local and global explanations, where the former are concerned with explaining a classifier's behavior for a specific instance, while the latter are concerned with explaining the overall classifier's behavior regardless of any specific instance. In this paper, we focus on global explanations, and explain classification in terms of ``minimal'' necessary conditions for the classifier to assign a specific class to a generic instance. We carry out a thorough complexity analysis of the problem for natural minimality criteria and important families of classifiers considered in the literature.

Discussion (0). Continue with ORCID to comment.

Forward citations

Cited by 1 Pith paper

Reviewed papers in the Pith corpus that reference this work. Sorted by Pith novelty score. Full citation record

What makes an Ensemble (Un) Interpretable?
cs.LG 2025-06 conditional novelty 7.0 of 10

A complexity-theoretic analysis showing that the number, size, and type of base models determine whether ensemble explanations are tractable, with linear-model ensembles intractable even for two models.

Reference graph

Works this paper leans on

8 extracted references · 6 canonical work pages · cited by 1 Pith paper

[3]

Abductive Explanations of C lassiﬁers under Constraints: Complex- ity and Properties

[CA23] M. C. Cooper and L. Amgoud. “Abductive Explanations of C lassiﬁers under Constraints: Complex- ity and Properties”. In: Proc. ECAI. 2023, pp. 469–476. [CCM23] C. Carbonnel, M. C. Cooper, and J. Marques-Silva. “Tr actable Explaining of Multivariate Decision Trees”. In: Proc. KR. 2023, pp. 127–135. [CM22] A. de Colnet and P. Marquis. “On the Complexi...

work page 2023
[5]

Logic-Based Explainability in Ma chine Learning

[Mar22] J. Marques-Silva. “Logic-Based Explainability in Ma chine Learning”. In: Proc. RW. 2022, pp. 24–

work page 2022
[8]

Globally-Consistent Rul e-Based Summary-Explanations for Ma- chine Learning Models: Application to Credit-Risk Evaluati on

[RS23] C. Rudin and Y. Shaposhnik. “Globally-Consistent Rul e-Based Summary-Explanations for Ma- chine Learning Models: Application to Credit-Risk Evaluati on”. In: J. Mach. Learn. Res. 24 (2023), 16:1–16:44. [Set+19] M. Setzu, R. Guidotti, A. Monreale, and F. Turini. “G lobal Explanations with Local Scoring”. In: Proc. ECML PKDD Workshops. 2019, pp. 159–...

work page 2023
[104]

Marques-Silva

[Mar24] J. Marques-Silva. Logic-Based Explainability: Past, Present & Future . Tech. rep. arXiv:2406.11873. CoRR,

arXiv
[1995]

Computing Rule-B ased Explanations by Leveraging Counter- factuals

[GSS22] Z. Geng, M. Schleich, and D. Suciu. “Computing Rule-B ased Explanations by Leveraging Counter- factuals”. In: Proc. VLDB Endow. 16(3) (2022), pp. 420–432. [HAB02] W. Hesse, E. Allender, and D. A. M. Barrington. “Unifo rm Constant-Depth Threshold Circuits for Division and Iterated Multiplication”. In: J. Comput. Syst. Sci. 65(4) (2002), pp. 695–716...

work page 2022
[2009]

A Linear-Tim e Algorithm for Testing the Truth of Certain Quantiﬁed Boolean Formulas

[APT79] B. Aspvall, M. F. Plass, and R. E. Tarjan. “A Linear-Tim e Algorithm for Testing the Truth of Certain Quantiﬁed Boolean Formulas”. In: Inf. Process. Lett. 8(3) (1979), pp. 121–123. 24 [Are+21] M. Arenas, D. Baez, P. Barceló, J. Pérez, and B. Sube rcaseaux. “Foundations of Symbolic Languages for Model Interpretability”. In: Proc. NeurIPS. 2021, pp....

work page 1979
[2020]

Barceló, M

[Bar+20b] P. Barceló, M. Monet, J. Pérez, and B. Subercaseau x. Model Interpretability through the Lens of Com- putational Complexity. Tech. rep. arXiv:2010.12265. CoRR,

arXiv 2010
[2024]

Delivering Trustwo rthy AI through Formal XAI

25 [MI22] J. Marques-Silva and A. Ignatiev. “Delivering Trustwo rthy AI through Formal XAI”. In: Proc. AAAI. 2022, pp. 12342–12350. [OPS23] S. Ordyniak, G. Paesani, and S. Szeider. “The Paramet erized Complexity of Finding Concise Local Explanations”. In: Proc. IJCAI. 2023, pp. 3312–3320. [Rei08] O. Reingold. “Undirected Connectivity in Log-Space” . In: J...

work page 2008

Pith tools

Reviewed August 10, 2026 · model on record in the stance chip above.

[1] [3]

Abductive Explanations of C lassiﬁers under Constraints: Complex- ity and Properties

[CA23] M. C. Cooper and L. Amgoud. “Abductive Explanations of C lassiﬁers under Constraints: Complex- ity and Properties”. In: Proc. ECAI. 2023, pp. 469–476. [CCM23] C. Carbonnel, M. C. Cooper, and J. Marques-Silva. “Tr actable Explaining of Multivariate Decision Trees”. In: Proc. KR. 2023, pp. 127–135. [CM22] A. de Colnet and P. Marquis. “On the Complexi...

work page 2023

[2] [5]

Logic-Based Explainability in Ma chine Learning

[Mar22] J. Marques-Silva. “Logic-Based Explainability in Ma chine Learning”. In: Proc. RW. 2022, pp. 24–

work page 2022

[3] [8]

Globally-Consistent Rul e-Based Summary-Explanations for Ma- chine Learning Models: Application to Credit-Risk Evaluati on

[RS23] C. Rudin and Y. Shaposhnik. “Globally-Consistent Rul e-Based Summary-Explanations for Ma- chine Learning Models: Application to Credit-Risk Evaluati on”. In: J. Mach. Learn. Res. 24 (2023), 16:1–16:44. [Set+19] M. Setzu, R. Guidotti, A. Monreale, and F. Turini. “G lobal Explanations with Local Scoring”. In: Proc. ECML PKDD Workshops. 2019, pp. 159–...

work page 2023

[4] [104]

Marques-Silva

[Mar24] J. Marques-Silva. Logic-Based Explainability: Past, Present & Future . Tech. rep. arXiv:2406.11873. CoRR,

arXiv

[5] [1995]

Computing Rule-B ased Explanations by Leveraging Counter- factuals

[GSS22] Z. Geng, M. Schleich, and D. Suciu. “Computing Rule-B ased Explanations by Leveraging Counter- factuals”. In: Proc. VLDB Endow. 16(3) (2022), pp. 420–432. [HAB02] W. Hesse, E. Allender, and D. A. M. Barrington. “Unifo rm Constant-Depth Threshold Circuits for Division and Iterated Multiplication”. In: J. Comput. Syst. Sci. 65(4) (2002), pp. 695–716...

work page 2022

[6] [2009]

A Linear-Tim e Algorithm for Testing the Truth of Certain Quantiﬁed Boolean Formulas

[APT79] B. Aspvall, M. F. Plass, and R. E. Tarjan. “A Linear-Tim e Algorithm for Testing the Truth of Certain Quantiﬁed Boolean Formulas”. In: Inf. Process. Lett. 8(3) (1979), pp. 121–123. 24 [Are+21] M. Arenas, D. Baez, P. Barceló, J. Pérez, and B. Sube rcaseaux. “Foundations of Symbolic Languages for Model Interpretability”. In: Proc. NeurIPS. 2021, pp....

work page 1979

[7] [2020]

Barceló, M

[Bar+20b] P. Barceló, M. Monet, J. Pérez, and B. Subercaseau x. Model Interpretability through the Lens of Com- putational Complexity. Tech. rep. arXiv:2010.12265. CoRR,

arXiv 2010

[8] [2024]

Delivering Trustwo rthy AI through Formal XAI

25 [MI22] J. Marques-Silva and A. Ignatiev. “Delivering Trustwo rthy AI through Formal XAI”. In: Proc. AAAI. 2022, pp. 12342–12350. [OPS23] S. Ordyniak, G. Paesani, and S. Szeider. “The Paramet erized Complexity of Finding Concise Local Explanations”. In: Proc. IJCAI. 2023, pp. 3312–3320. [Rei08] O. Reingold. “Undirected Connectivity in Log-Space” . In: J...

work page 2008