Research map / Learning theory and algorithms / Sample complexity
Learning Minimum-Size BDDs: Towards Efficient Exact Algorithms
Read the paperCheck your idea against 108,967 papers
AI-extracted summary. Written by AI from the paper's full text. Numbers and claims can be wrong or missing context, so check the paper before you cite or build on it.
Gives a witness-based branch-and-bound algorithm (WitBDD) for minimum-size BDD learning with improved running-time bounds, plus ETH lower bounds and a proof-of-concept implementation compared against a SAT encoding.
Problem
Learning minimum-size binary decision diagrams (BDDs) that perfectly or near-perfectly classify labeled data; the problem is NP-hard and prior exact algorithms were impractical enumerative methods.
Approach
Adapts the witness paradigm from decision-tree learning to BDDs: the BDD is built incrementally by refining arcs for dirty examples, and each new edge is annotated with a witness example that must traverse it, shrinking the search space; the result is a search-tree algorithm with running time O((6s^2 δ D)^s · s·n).
Key results
- WitBDD solved 443 of 700 instances versus 557 for the re-implemented SAT encoding; all WitBDD-solved instances were also solved by SAT.
- On the 353 instances with optimal size at most 4, WitBDD was on average about 828 times faster than the SAT encoding (median speedup 64).
- On instances with optimal size above 4, the SAT encoding was on average about 37 times faster than WitBDD (median speedup 7).
Measured effects reported in the paper
| What was changed | Where | Measured | Effect |
|---|---|---|---|
| Use WitBDD instead of the SAT encoding | BDD minimum-size solving · Penn Machine Learning Benchmarks, instances with optimal BDD size at most 4 | running time: roughly 828 times faster on average; median speedup of 64 | Helped |
| Use WitBDD instead of the SAT encoding | BDD minimum-size solving · Penn Machine Learning Benchmarks, instances with optimal BDD size bigger than 4 | running time: SAT encoding was on average roughly 37 times faster; median speedup of 7 | Hurt |
| Use WitBDD instead of the SAT encoding | BDD minimum-size solving · Penn Machine Learning Benchmarks, 700 instances | instances solved: 443 vs 557 | Hurt |
Surprising findings
- ERROR BSBDD remains NP-hard even with only d=4 dimensions, unlike decision trees where the analogous problem is polynomial for constant d.
Limitations
- Implementation is proof-of-concept and substantially slower than the SAT approach for BDD sizes above 4.
- Only sizes up to about 8 solved; larger BDDs out of reach.
- Search space grows quickly with the size bound s.
Experimental setup
Datasets: Penn Machine Learning Benchmarks (35 binary classification datasets, subsampled to 700 instances)
Benchmarks: Penn Machine Learning Benchmarks subsampled instances
Metrics: running time number of instances solved within 60-minute limit optimal BDD size
Baselines: SAT encoding of Cabodi et al. (2024) Ordyniak et al. (2024) FPT algorithm
Builds on: witness paradigm for decision trees (Komusiewicz et al., 2023) extendability framework (Ordyniak et al., 2024) SAT-based MSOBDD encoding (Cabodi et al., 2024)
Closest papers by meaning
- Witty: An Efficient Solver for Computing Minimum-Size Decision Trees (AAAI 2025 · similarity 0.89)
- Using Clustering to Strengthen Decision Diagram Bounds for Discrete Optimization (AAAI 2024 · similarity 0.86)
- Optimal Decision Tree Pruning Revisited: Algorithms and Complexity (ICML 2025 · similarity 0.86)
- SORTeD Rashomon Sets of Sparse Decision Trees: Anytime Enumeration (NeurIPS 2025 · similarity 0.85)
- Learning Small Decision Trees for Data of Low Rank-Width (AAAI 2024 · similarity 0.85)
- Improving Decision Trees through the Lens of Parameterized Local Search (NeurIPS 2025 · similarity 0.85)
Writing a paper in this area? scime draft is a free LaTeX editor with AI included, real-time co-authors and a check of your references and venue rules before you submit. It also imports OpenAI Prism projects.