Optimizing Binary Decision Diagrams with MaxSAT for Classification

Authors: Hao Hu, Marie-José Huguet, Mohamed Siala3767-3775

AAAI 2022 | Conference PDF | Archive PDF | Plain Text | LLM Run Details

Reproducibility Variable Result LLM Response
Research Type Experimental Our empirical study shows clear benefits of the proposed approach in terms of prediction quality and interpretability (i.e., lighter size) compared to the state-of-the-art approaches.
Researcher Affiliation Academia LAAS-CNRS, Universit e de Toulouse, CNRS, INSA, Toulouse, France
Pseudocode No The paper describes algorithmic steps in prose but does not include structured pseudocode or clearly labeled algorithm blocks.
Open Source Code Yes The source code and the datasets are available online at https://gitlab.laas.fr/hhu/bddencoding
Open Datasets Yes We consider datasets from CP4IM 3. These datasets are binarized with the one-hot encoding. Footnote 3: https://dtai.cs.kuleuven.be/CP4IM/datasets/
Dataset Splits Yes For each dataset, we use random 5-fold cross-validation with 5 different seeds.
Hardware Specification Yes All experiments were run on a cluster using Xeon E5-2695 v3@2.30GHz CPU and running x Ubuntu 16.04.6 LTS.
Software Dependencies No The Max SAT solver we used is Loandra (Berg, Demirovi c, and Stuckey 2019), an efficient incomplete Max SAT solver that return the best solution found within a limited computation time or report optimality. While the solver is named, a specific version number for it or other key software components is not provided.
Experiment Setup Yes We consider the P bdd(E, H) problem with 5 different depths H {2, 3, 4, 5, 6}. For each experiment, the time limit for generating formulas and the time limit for solver are set to 15 minutes.