# On Tractable Representations of Binary Neural Networks

arXiv: https://arxiv.org/abs/2004.02082 · HTML: https://mlsanity.com/paper/2004.02082/

## Key facts

- Cited by 34 papers in the map (data through 14 Oct 2026).
- First posted on arXiv 5 Apr 2020.

## Built on by (most cited first, 30 of 34)

- [On Guaranteed Optimal Robust Explanations for NLP Models](https://mlsanity.com/paper/2105.03640/) (2021)
- [Logic-Based Explainability in Machine Learning](https://mlsanity.com/paper/2211.00541/) (2022)
- [Deep Learning with Logical Constraints](https://mlsanity.com/paper/2205.00523/) (2022)
- [On Tackling Explanation Redundancy in Decision Trees](https://mlsanity.com/paper/2205.09971/) (2022)
- [Towards Formal XAI: Formally Approximate Minimal Explanations of Neural Networks](https://mlsanity.com/paper/2210.13915/) (2022)
- [Explanations for Monotonic Classifiers](https://mlsanity.com/paper/2106.00154/) (2021)
- [On the Complexity of SHAP-Score-Based Explanations: Tractability via Knowledge Compilation and Non-Approximability Results](https://mlsanity.com/paper/2104.08015/) (2021)
- [ASTERYX : A model-Agnostic SaT-basEd appRoach for sYmbolic and score-based eXplanations](https://mlsanity.com/paper/2206.11900/) (2022)
- [Probabilistic Sufficient Explanations](https://mlsanity.com/paper/2105.10118/) (2021)
- [Formally Explaining Neural Networks within Reactive Systems](https://mlsanity.com/paper/2308.00143/) (2023)
- [On the Computation of Necessary and Sufficient Explanations](https://mlsanity.com/paper/2203.10451/) (2022)
- [Logic for Explainable AI](https://mlsanity.com/paper/2305.05172/) (2023)
- [On Quantifying Literals in Boolean Logic and Its Applications to Explainable AI](https://mlsanity.com/paper/2108.09876/) (2021)
- [FlowPG: Action-constrained Policy Gradient with Normalizing Flows](https://mlsanity.com/paper/2402.05149/) (2024)
- [A unified logical framework for explanations in classifier systems](https://mlsanity.com/paper/2105.14452/) (2021)
- [Tractable Boolean and Arithmetic Circuits](https://mlsanity.com/paper/2202.02942/) (2022)
- [Cardinality-Minimal Explanations for Monotonic Neural Networks](https://mlsanity.com/paper/2205.09901/) (2022)
- [A New Class of Explanations for Classifiers with Non-Binary Features](https://mlsanity.com/paper/2304.14760/) (2023)
- [Provable Guarantees on the Robustness of Decision Rules to Causal Interventions](https://mlsanity.com/paper/2105.09108/) (2021)
- [A Symbolic Approach for Counterfactual Explanations](https://mlsanity.com/paper/2206.09638/) (2022)
- [Formal Abductive Latent Explanations for Prototype-Based Networks](https://mlsanity.com/paper/2511.16588/) (2025)
- [A Scalable, Interpretable, Verifiable & Differentiable Logic Gate Convolutional Neural Network Architecture From Truth Tables](https://mlsanity.com/paper/2208.08609/) (2022)
- [Semantic Probabilistic Control of Language Models](https://mlsanity.com/paper/2505.01954/) (2025)
- [Efficient Computation of Shap Explanation Scores for Neural Network Classifiers via Knowledge Compilation](https://mlsanity.com/paper/2303.06516/) (2023)
- [Injecting Undetectable Backdoors in Obfuscated Neural Networks and Language Models](https://mlsanity.com/paper/2406.05660/) (2024)
- [Attribution-Scores and Causal Counterfactuals as Explanations in Artificial Intelligence](https://mlsanity.com/paper/2303.02829/) (2023)
- [Attribution-Scores in Data Management and Explainable Machine Learning](https://mlsanity.com/paper/2308.00184/) (2023)
- [Principled Diverse Counterfactuals in Multilinear Models](https://mlsanity.com/paper/2201.06467/) (2022)
- [Verifying Properties of Binary Neural Networks Using Sparse Polynomial Optimization](https://mlsanity.com/paper/2405.17049/) (2024)
- [Binary Spiking Neural Networks as Causal Models](https://mlsanity.com/paper/2604.27007/) (2026)

## Abstract (arXiv)

We consider the compilation of a binary neural network's decision function into tractable representations such as Ordered Binary Decision Diagrams (OBDDs) and Sentential Decision Diagrams (SDDs). Obtaining this function as an OBDD/SDD facilitates the explanation and formal verification of a neural network's behavior. First, we consider the task of verifying the robustness of a neural network, and show how we can compute the expected robustness of a neural network, given an OBDD/SDD representation of it. Next, we consider a more efficient approach for compiling neural networks, based on a pseudo-polynomial time algorithm for compiling a neuron. We then provide a case study in a handwritten digits dataset, highlighting how two neural networks trained from the same dataset can have very high accuracies, yet have very different levels of robustness. Finally, in experiments, we show that it is feasible to obtain compact representations of neural networks as SDDs.