Decision trees are one of the most interpretable machine learning models and due to this property have gained increased attention in the past years. In this context, decision trees of small size and depth are of particular interest and new methods have been developed that can induce decision trees that are both small and accurate.

In this talk, I will give an overview of SAT-based methods that have been proposed, starting with general encodings for inducing decision trees and then discussing options for scaling them to larger instances in a heuristic manner. I will give particular focus to our algorithm DT-SLIM, which reduces the size and depth of a given decision tree by using a SAT solver to repeatedly improve localized parts of the tree.

Joint work with Stefan Szeider.