Learning Minimum-Size BDDs: Towards Efficient Exact Algorithms
Authors: Christian Komusiewicz, Andre Schidler, Frank Sommer, Manuel Sorge, Luca Pascal Staus
ICML 2025 | Venue PDF | Archive PDF | Plain Text | LLM Run Details
| Reproducibility Variable | Result | LLM Response |
|---|---|---|
| Research Type | Experimental | To demonstrate the practical potential, we provide an implementation of our main algorithmic result. We compare it to a state-of-the-art SAT-based approach (Cabodi et al., 2024) on standard benchmark data. Despite its proof-of-concept status, our implementation computes optimal BDDs of size up to seven, is faster than the SAT-based approach for BDD sizes up to four, and in general solves 79% of the instances that also the SAT-approach solves within a 1h time limit. 5. Experiments We implemented Algorithm 1 to gauge how it performs in practice. |
| Researcher Affiliation | Academia | 1Institute of Computer Science, University of Jena, Germany 2Institute of Logic and Computation, TU Wien, Austria 3Computer Architecture, University of Freiburg, Germany. |
| Pseudocode | Yes | Algorithm 1: Wit BDD Input: A consistent WBDD W, a data set (E, λ), and a maximum size s N. Output: A perfect consistent WBDD of size at most s or if none could be found. |
| Open Source Code | Yes | Our source code is available in the supplementary material. |
| Open Datasets | Yes | For our experiments we used 35 datasets of the Penn Machine Learning Benchmarks (Romano et al., 2022) that were also used by Staus et al. (2025) in their experiments on computing optimal decision trees; see Table 1 in the appendix. |
| Dataset Splits | Yes | Specifically, for each data set we constructed 10 instances by randomly selecting 10% of the examples and 10 instances by randomly selecting 20% of the examples. This gives a total of 700 instances. |
| Hardware Specification | Yes | Our experiments were performed on Intel(R) Xeon(R) Platinum 8360Y(2) CPUs with 2.6 GHz and 24 cores and 256 GB RAM. Each individual experiment was performed on a private core with a RAM limit of 2 GB. For the SAT encoding we increased the limit to 20 GB. |
| Software Dependencies | Yes | We implemented Wit BDD in C++ and the SAT-formulation in Python with Ca Di Ca L 1.9.5 as the SAT-solver. Our source code is available in the supplementary material.3 For Wit BDD, we additionally use the SET COVER instance I from the Pair LB to compute a packing of the cuts such that each set in the packing has at least one example pair that can only be separated by cuts in that set. The number of sets in the packing is a lower bound for I and therefore also for the smallest size of a perfect BDD. To compute such a lower bound, we solve the LP relaxation of an ILP formulation for SET COVER, using Gurobi 10.0.3. (Gurobi Optimization, LLC, 2024). |
| Experiment Setup | Yes | Experimental setup. For our experiments we used 35 datasets of the Penn Machine Learning Benchmarks (Romano et al., 2022) that were also used by Staus et al. (2025) in their experiments on computing optimal decision trees; see Table 1 in the appendix. Each of these instances is a binary classification problem. Analogously to Cabodi et al. (2024), we randomly sampled multiple subsets of the examples from each data set: Specifically, for each data set we constructed 10 instances by randomly selecting 10% of the examples and 10 instances by randomly selecting 20% of the examples. This gives a total of 700 instances. For each instance we set a time limit of 60 minutes. Our experiments were performed on Intel(R) Xeon(R) Platinum 8360Y(2) CPUs with 2.6 GHz and 24 cores and 256 GB RAM. Each individual experiment was performed on a private core with a RAM limit of 2 GB. For the SAT encoding we increased the limit to 20 GB. We implemented Wit BDD in C++ and the SAT-formulation in Python with Ca Di Ca L 1.9.5 as the SAT-solver. Our source code is available in the supplementary material.3 |