Learning Optimal Oblique Decision Trees with (Max)SAT
Authors: Florent Avellaneda
IJCAI 2025 | Venue PDF | Archive PDF | Plain Text | LLM Run Details
| Reproducibility Variable | Result | LLM Response |
|---|---|---|
| Research Type | Experimental | Experiments on benchmark datasets demonstrate that our approach generates optimal oblique decision trees within reasonable computational time for small to medium-sized datasets. |
| Researcher Affiliation | Academia | Florent Avellaneda Universit e du Qu ebec a Montr eal (UQAM), Montr eal, Canada EMAIL |
| Pseudocode | No | The paper describes the problem formulation using (Max)SAT and SMT constraints and then details a two-step process for decoding decision trees from solutions, but it does not present these as structured pseudocode or algorithm blocks. |
| Open Source Code | Yes | 1https://github.com/Florent Avellaneda/Infer Optimal Oblique DT |
| Open Datasets | Yes | We evaluated our approach using 13 small to medium-sized real-world datasets from the UCI Machine Learning Repository [Kelly et al., 2023], as detailed in Table 1. |
| Dataset Splits | No | The paper mentions evaluating training accuracy on datasets but does not explicitly provide details about training/test/validation splits (e.g., percentages, sample counts, or specific splitting methodologies). |
| Hardware Specification | Yes | All experiments were conducted under controlled conditions using a single thread of a AMD EPYC 7532 (Zen 2) processor (2.4 GHz) with 32 GB of RAM. |
| Software Dependencies | No | We implemented our methods in C++1 and utilized the Eval Max SAT solver [Avellaneda, 2020b] for Max SAT, the Z3 solver [De Moura and Bjørner, 2008] for SMT and Lib SVM [Chang and Lin, 2011] to compute the hard-margin SVM. |
| Experiment Setup | Yes | To ensure practical feasibility, we imposed a maximum runtime limit of three hours per experiment. In our results tables, experiments exceeding this time limit are denoted by . (...) To address scalability limitations with larger datasets, we conducted additional experiments using the incomplete Max SAT solver Nu WLS [Chu et al., 2023], configuring it with timeouts of 5 minutes and 1 hour. |