Learning Optimal Oblique Decision Trees with (Max)SAT

1 Introduction

Decision trees are one of the most widely used models in machine learning, valued for their interpretability, simplicity, and competitive performance on various classification tasks [Breiman et al., 1984; Quinlan, 1986]. A decision tree partitions the input space into regions by iteratively applying simple rules. Each leaf corresponds to a class, and the path from the root to a leaf represents a conjunction of conditions that leads to that classification.

Traditional decision tree learning methods, such as ID3 [Quinlan, 1986], C4.5 [Quinlan, 1993], and CART [Breiman et al., 1984], employ an axis-parallel splitting approach, where each decision node tests a single feature against a threshold, resulting in splits that are perpendicular to one of the feature axes. In these methods, each internal node splits the data based on a single feature and a threshold. While effective and computationally efficient, axis-parallel trees have inherent limitations. Specifically, when the decision boundary between classes is not aligned with the feature axes, these trees may require numerous splits to approximate the boundary, resulting in larger, less interpretable, and potentially less accurate models.

Oblique decision trees overcome this limitation by allowing internal nodes to split the data using a linear combination of features rather than relying on single-feature splits [Heath et al., 1993]. This flexibility enables the trees to naturally capture non-axis-parallel decision boundaries, often leading to smaller, more accurate models. Early work on oblique decision trees, such as the OC1 algorithm [Murthy et al., 1994], employed randomized searches to identify hyperplanes. While these approaches offered improvements over axis-parallel trees, they relied on greedy heuristics, lacking guarantees of global optimality.

Recent advances in optimal decision tree learning have highlighted the potential of combinatorial optimization techniques. Mixed-integer linear programming [Bertsimas and Dunn, 2017; Verwer and Zhang, 2019], SAT solving [Avellaneda, 2020a; Verwer and Zhang, 2019; Shati et al., 2021; Narodytska et al., 2018], and dynamic programming [Demirovi´c et al., 2022; Aglin et al., 2020; Nijssen and Fromont, 2007] have been successfully applied to derive provably optimal axis-parallel trees. However, extending these methods to oblique decision trees presents unique challenges due to the continuous nature of hyperplane parameters and the combinatorial complexity of optimizing tree structures. Although some progress has been made using linear programming for this task [Zhu et al., 2020; Bertsimas and Dunn, 2017], to the best of our knowledge, the potential of (Max)SAT encoding remains unexplored.

In this paper, we introduce a novel approach for learning optimal oblique decision trees using (Max)SAT solvers. Our method encodes the learning problem as a (Max)SAT instance, enabling modern solvers to find globally optimal solutions. This approach combines guaranteed optimality with practical efficiency for reasonably sized datasets.

The paper is structured as follows. Section 2 introduces background on oblique decision trees. Section 3 describes our encoding and solving approach. Section 4 reports experimental results. Finally, Section 5 concludes the paper.

2 Preliminaries

Let E = {e0, . . . , en-1} be a set of n examples. Each example ei ∈ Rm is a vector representing the values of m features F = {f0, . . . , fm-1}. For an example e ∈ E and a feature f ∈ F, we use the notation e[f] to represent the value of feature f for the example e. The label class for each example e is given by the true label function γ : E → Y, where Y = {0, . . . , c - 1} is the set of possible class labels.

Definition 1 (Binary Tree Structure). A binary tree structure T is a tuple (NB,NL, δ, p, l, r) where:

• NB and NL are disjoint finite sets of branching nodes and leaf nodes, respectively.
• δ ∈ NB ∪NL is the root node.
• p : (NB ∪ NL) \ {δ} → NB is the parent function, mapping each non-root node to its parent.
• l : NB →NB ∪NL is the left child function.
• r : NB →NB ∪NL is the right child function.

Additionally, the following conditions must hold:

• (Parent-Child Consistency) For every branching node n ∈ NB, we have p(l(n)) = n and p(r(n)) = n.
• (Tree Structure) Every node n ∈ NB ∪NL is reachable from the root through a unique path. Formally, there exists a unique sequence of nodes n0, . . . , nk such that n0 = δ, nk = n, and for all i ∈ {0, . . . , k - 1}, ni+1 = l(ni) or ni+1 = r(ni).

We define the depth of a binary tree structure T as the length of the longest path from the root to a leaf node.

Definition 2 (Oblique Decision Tree). An oblique decision tree D is a tuple D = (T , θ, λ), where:

• T = (NB,NL, δ, p, l, r) is a binary tree structure.
• θ : NB → (Rm ×R) is a function that assigns to each branching node n ∈ NB a decision rule, represented by the tuple θ(n) = (wn, tn). Here, wn ∈ Rm is a weight vector and tn ∈ R is a threshold.
• λ : NL → Y is a function that assigns to each leaf node n ∈ NL a prediction λ(n) ∈ Y.

To classify an example e using an oblique decision tree D, we denote the resulting classification as D(e). This classification is determined by the function cl(D, δ, e), where δ represents the root node of the tree. The function cl is defined recursively as follows:

The accuracy of an oblique decision tree D on a set of examples E with true labels γ is formally defined as:

Definition 3 (Optimal Oblique Decision Tree). Given a maximum depth d ∈ N, a set of examples E, and a true label function γ, an oblique decision tree D∗ is optimal with respect to depth d if the depth of D∗ is equal or less than d and for any other oblique decision tree D′ such that depth(D′ ) ≤ p, Accuracy(D′ , E, γ) ≤ Accuracy(D∗ , E, γ)

In this paper, we focus on sparse oblique decision trees where each decision rule θ(n) = (wn, tn) is constrained such that the weight vector wn contains at most two non-zero components.

3 Constraint-Based Learning of Decision Trees

Given a set of examples E and a true label function γ : E → Y, our objective is to learn an optimal oblique decision tree D∗ that minimizes classification error while respecting a maximum depth constraint d. Building on the SAT encoding for non-binary features proposed in [Shati et al., 2021], we introduce a novel encoding for learning optimal oblique decision trees.

To formalize the problem, we define the following set of Boolean variables:

• Se,n: True if the example e is directed towards the left child, if it passes through branching node n.
• Ze,n: True if the example e terminates at leaf node n.
• Cn,c: True if the leaf node n is assigned to the class c.
• An,f1,f2 : True if the feature f1 and f2 are selected for the split at branching node n.

For each each n ∈ NB and every f1, f2, f ′1 , f ′2 ∈ F such that (f1, f2) ̸= (f ′1 , f ′2 ) , we add the clause:

These clauses ensure that each branching node selects at most one pair of features for splitting.

For each n ∈ NB, we add the clause:

These clauses ensure that each branching node selects at least one pair of features for splitting.

For each n ∈ NL, each e ∈ E and each n′ ∈ Al(n), we add the clause:

With Al(n) the set of ancestors of the leaf node n such that n is a descendant of their left branch.

For each n ∈ NL, each e ∈ E and each n′ ∈ Ar(n), we add the clause:

With Ar(n) the set of ancestors of the leaf node n such that n is a descendant of their right branch.

For each n ∈ NL and each e ∈ E, we add the clause:

The clauses (3) and (4) ensure that if an example e reaches a leaf node n, it must have followed the correct path from the root to n, as dictated by the variables S. Conversely, the clauses (5) ensure that if an example e does not terminate at a leaf node n, then at least one of its ancestor nodes must have redirected e to a different path.

For every c1, c2 ∈ Y and each n ∈ NL, we add the clause:

These clauses ensure that each leaf node is assigned to a single class.

For each example e ∈ E and each n ∈ NL, we add the clause:

These clauses ensure that if an example e reaches a leaf node n, the leaf node n must be assigned the correct class as specified by the true label function γ.

Note that if clauses (7) are treated as hard clauses, then we construct a SAT formula that seeks a decision tree fully consistent with the dataset, i.e., achieving 100% accuracy. If such a tree does not exist and we aim to find the tree that minimizes classification errors, we can switch to MaxSAT by treating clauses (7) as soft clauses. The same applies to the SMT setting: we can use MaxSMT to minimize classification errors when no perfectly consistent tree exists.

At this point, we need to add constraints to S and A to ensure that, given the features present at each branching node, the partition represented by S can be achieved via linear separation using only two features. We propose two solutions to implement these constraints. The first approach utilizes an (Max)SMT solver to encode them directly, while the second involves encoding them natively in (Max)SAT.

3.1 Linear separation with (Max)SMT

Satisfiability Modulo Theories (SMT) is an extension of SAT that allows for solving satisfiability problems with constraints from specific theories, such as linear arithmetic. By employing an SMT solver, we can encode the linear separation constraints directly within the theory of linear arithmetic, which simplifies the process and leverages the solver's built-in capabilities for handling such theories. Its extension, MaxSMT, further allows for the inclusion of soft clauses.

To encode the possible splits at each branching node, we introduce real variables xn,1, xn,2, and xn,3 for each branching node n ∈ NB. These variables represent the coefficients of the linear inequality that defines the split at node n.

Specifically, if the variable An,f1,f2 is true, indicating that features f1 and f2 are used at node n, then the split at node n is defined by the linear inequality:

Here, Ff1 and Ff2 represent the values of features f1 and f2, respectively. This linear equation determines how data points are partitioned at the branching node based on the selected features and the learned coefficients.

Thus, for each branching node n ∈ NB, each pair of features f1, f2 ∈ F, and each example e ∈ E, we add the following constraints:

These constraints ensure that if the pair of features f1 and f2 is selected for the split at branching node n, then example e is directed to the left child if the linear inequality is satisfied, and to the right child otherwise.

3.2 Linear Separation with (Max)SAT

At each branching node n, if An,f1,f2 is true, the split at this node, represented by Se,n, must correspond to a linear separation of the examples based on features f1 and f2. This reduces to finding a linear separator in a 2D plane, where each example is a point with coordinates given by its values of f1 and f2. A naive approach would consider all possible linear cuts and add constraints to ensure each example is directed to the correct child node based on the chosen cut. However, this method is inefficient due to the excessive number of variables and constraints required.

To address this, we propose an alternative approach that reduces the number of variables and constraints needed to encode the problem. We introduce two fictitious points at infinity in the projective plane, defined as PA = (1, 1, 0) and PB = (-1,-1, 0). In the projective plane, a point is represented by a triplet (x, y, z). When z ̸= 0, the point corresponds to the Euclidean coordinates (x/z, y/z). When z = 0, the point is considered to lie "at infinity" in a specific direction. Given three points p1, p2 and p3, we denote by triangle(p1, p2, p3) the convex hull of these three points.

Then, our method relies on the following theorem:

Theorem 1. Let A and B be two sets of points. These sets are linearly separable if and only if the following two conditions are satisfied:

• For every triplet of points (p1, p2, p3) with p1, p2 ∈ A and p3 ∈ B, p3 /∈ triangle(p1, p2, PA).
• For every triplet of points (p1, p2, p3) with p1, p2 ∈ B and p3 ∈ A, p3 /∈ triangle(p1, p2, PB).

Where PA and PB are two points at infinity in the projective plane, defined as PA = (1, 1, 0) and PB = (-1,-1, 0), or vice versa.

Proof. (⇒) Suppose that A and B are linearly separable. Then, there exist real coefficients a, b, and c such that:

Since PA and PB are points at infinity in opposite directions, only one of them lies in the half-plane ax + by + c ≥ 0. Without loss of generality, assume PA lies in this half-plane. Consider any triplet (p1, p2, p3) with p1, p2 ∈ A and p3 ∈ B. The triangle formed by p1, p2, and PA, is entirely contained within the half-plane ax + by + c ≥ 0. Since p3 lies in B and the half-plane ax + by + c < 0, it cannot lie within triangle(p1, p2, PA). Therefore, p3 /∈ triangle(p1, p2, PA). A similar argument applies for B and PB.

(⇐) Conversely, suppose the conditions hold but A and B are not linearly separable. This means their convex hulls intersect. Consequently, there exists a point p that belongs to both Conv(A) and Conv(B).

This implies that there exist points p1, p2 ∈ A and p3, p4 ∈ B such that p lies within both triangle(p1, p2, PA) and triangle(p3, p4, PB). Since the sides leading to PA and PB are parallel (as PA and PB are points at infinity in opposite directions), and the triangles have a non-empty intersection, this intersection must contain at least one of the points p1, p2, p3, or p4. This contradiction implies that A and B must be linearly separable.

This theorem allows us to encode the linear separation problem by stating that if two points p1 and p2 belong to the same class A, then any point p3 that lies within the triangle formed by p1, p2, and the point at infinity PA must also belong to class A. A similar reasoning applies for class B with the point at infinity PB.

Therefore, for each branching node n ∈ NB, each pair of features f1, f2 ∈ F , and every triplet of examples e1, e2, e3 ∈ E such that p3 lies inside the triangle formed by p1, p2, and PA, with p1 = (e1[f1], e1[f2]), p2 = (e2[f1], e2[f2]), and p3 = (e3[f1], e3[f2]), we add the clause:

Similarly, each branching node n ∈ NB, every pair of features f1, f2 ∈ F, and every triplet of examples e1, e2, e3 ∈ E such that p3 ∈ triangle(p1, p2, PB), with p1 = (e1[f1], e1[f2]), p2 = (e2[f1], e2[f2]), and p3 = (e3[f1], e3[f2]), we add the clause:

Equations (10) and (11) ensure that if the pair of features f1, f2 is chosen for separation at branching node n, S will split the examples such that a linear separation exists.

Minimizing the Number of Clauses

Equations (10) and (11) can introduce a substantial number of clauses into our model, potentially increasing computational complexity. To enhance efficiency, we aim to minimize the number of clauses by eliminating redundant constraints.

Let p1 = (e1[f1], e1[f2]), p2 = (e2[f1], e2[f2]), p3 = (e3[f1], e3[f2]), and p′3 = (e′3 [f1], e′3 [f2]), four points such that p3 ∈ triangle(p1, p2, PA), p′3 ∈ triangle(p1, p2, PA), and p′3 ∈ triangle(p1, p3, PA) (see Figure 1). In this configuration, if we have already added the constraints (10) for the triplets (e1, e2, e3) and (e1, e3, e′3 ), it becomes unnecessary to add the same constraints for the triplet (e1, e2, e′3 ). The reason is that the constraints for (e1, e2, e′3 ) are implied by those for (e1, e2, e3) and (e1, e3, e′3 ). A similar argument applies when p′3 ∈ triangle(p2, p3, PA), as well as for the corresponding case involving the point PB.

Similarly, examples sharing identical values for features f1 and f2 cannot be separated by a linear decision boundary based on these features. Thus, it suffices to retain a single representative example from each group of duplicates for our constraints.

To formalize this reduction, we define two functions based on a total order ≤ on the set of examples E. The function firsts(f1, f2) selects, for each unique combination of feature values (v1, v2), the minimal example according to the total order. Formally, firsts(f1, f2) = {e ∈ E | ∀e′ ∈ E, e′ [f1] = e[f1] ∧ e′ [f2] = e[f2] ⇒ e′ ≥ e} For each e ∈ firsts(f1, f2), the function doublons(e) returns the set of examples that share the same feature values as e but are greater than e in the total order. Formally: doublons(e) = {e′ ∈ E | e′ [f1] = e[f1], e′ [f2] = e[f2], e′ > e}.

Using these functions, we can now replace (10) and (11) by the following constraints.

For each branching node n ∈ NB, each pair of features f1, f2 ∈ F, and each example e ∈ firsts(f1, f2), we add the clauses:

These constraints ensure that examples with identical values for features f1 and f2 are directed toward the same child. We define the projection πf1,f2 (e) = (e[f1], e[f2]). For each branching node n ∈ NB, each pair of features f1, f2 ∈ F , and each pair of examples e1, e2 ∈ firsts(f1, f2), we select only one example e3 ∈ firsts(f1, f2) such that πf1,f2 (e3) ∈ triangle(πf1,f2 (e1), πf1,f2 (e2), PA), and for all e′3 ∈ firsts(f1, f2), if πf1,f2 (e′3 ) ∈ triangle(πf1,f2 (e1), πf1,f2 (e2), PA), then πf1,f2 (e′3 ) ∈ triangle(πf1,f2 (e1), πf1,f2 (e3), PA) ∪ triangle(πf1,f2 (e2), πf1,f2 (e3), PA). We then add the clause:

For each branching node n ∈ NB, each pair of features f1, f2 ∈ F , and each pair of examples e1, e2 ∈ firsts(f1, f2), we select only one example e3 ∈ firsts(f1, f2) such that πf1,f2 (e3) ∈ triangle(πf1,f2 (e1), πf1,f2 (e2), PB), and for all e′3 ∈ firsts(f1, f2), if πf1,f2 (e′3 ) ∈ triangle(πf1,f2 (e1), πf1,f2 (e2), PB), then πf1,f2 (e′3 ) ∈ triangle(πf1,f2 (e1), πf1,f2 (e3), PB) ∪ triangle(πf1,f2 (e2), πf1,f2 (e3), PB). We then add the clause:

The clauses (14) and (15) ensure that if the pair of features f1, f2 is chosen for splitting at node n, then the assignment of examples to the left or right child by S corresponds to a linear separation based on these features.

3.3 Decoding Decision Trees from Solutions

The solutions obtained from the (Max)SMT or (Max)SAT encodings allow us to construct an oblique decision tree that minimizes classification errors. However, translating these solutions into an explicit tree is nontrivial. While it is relatively easy to determine which examples reach each node, identifying a linear separation equations at the branching nodes presents a challenge.

In the SAT-based approach, the linear separation equations at the branching nodes are not explicitly provided. The SMTbased approach produces valid equations but does not necessarily optimize the separation between classes.

To address this, we employ a hard-margin Support Vector Machine (SVM) to compute optimal separating hyperplanes at each branching node [Vapnik, 2013]. Hard-margin SVMs find the hyperplane that maximizes the margin between classes, reducing the risk of misclassification on unseen data.

Reconstructing the oblique decision tree involves two steps.

Step 1. Identifying Examples at Each Node

The variables Se,n from the solution indicate the path each example e takes through the tree. For a node n, we determine the examples that reach it by examining the values of Se,n. An example reaches node n if it satisfies the branching decisions along the path from the root to n. This step is straightforward and involves tracing the decisions encoded by Se,n for each example.

Step 2. Computing Optimal Separating Hyperplanes

For each branching node n, we compute the optimal separating hyperplane using a hard-margin SVM. Examples reaching node n are labeled +1 if directed to the left child, and -1 if directed to the right. Then, using these labeled examples and the selected features Ff1 and Ff2 at node n, we compute the optimal separating hyperplane defined by:

where xn,1, xn,2, and xn,3 are SVM-derived coefficients. This hyperplane represents the decision boundary at node n.

4 Experimentation

Our experimental evaluation assesses the computational feasibility and effectiveness of our proposed (Max)SAT and (Max)SMT encodings for learning optimal oblique decision trees. While oblique decision trees are known for their superior accuracy and more compact model sizes compared to axis-parallel trees, particularly on datasets with non-linear decision boundaries [Bertsimas and Dunn, 2017], our research specifically addresses the challenge of finding provably optimal solutions. We focused on two key aspects: the computational complexity of achieving optimality and the structural characteristics of the resulting optimal trees. We implemented our methods in C++ 1 and utilized the EvalMaxSAT solver [Avellaneda, 2020b] for MaxSAT, the Z3 solver [De Moura and Bjørner, 2008] for SMT and LibSVM [Chang and Lin, 2011] to compute the hard-margin SVM.

4.1 Experimental Setup

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. 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 "-".

4.2 Scope and Limitations

Our evaluation deliberately focuses on the fundamental challenge of learning optimal oblique decision trees rather than on techniques for enhancing generalization performance. Consequently, we did not perform exhaustive comparisons of test set accuracy against heuristic methods. Advanced techniques such as pruning, regularization of oblique splits, and ensemble methods were beyond the scope of our research.

4.3 Real-World Datasets

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. These datasets represent diverse classification tasks, exhibiting variations in the number of instances, features, and classes.

To evaluate our optimal oblique tree learning methods, we compared them with three distinct approaches:

• Optimal ADT [Shati et al., 2021]: The current state-ofthe-art method for learning optimal axis-parallel decision trees using (Max)SAT solvers. This comparison allows us to isolate the computational overhead introduced by learning oblique splits while maintaining optimality.
• HHCART [Wickramarachchi et al., 2016]: A heuristic algorithm for learning oblique decision trees, implemented in the scikit-obliquetree Python package [ECNU, 2021]. This serves as a reference against a practical and fast heuristic approach.
• IAI [Interpretable AI, 2024]: A commercial implementation based on the optimal decision tree framework [Bertsimas and Dunn, 2017]. While IAI's theoretical

1 https://github.com/FlorentAvellaneda/InferOptimalObliqueDT

framework addresses optimal trees, their implementation employs heuristic approximations for practical runtime considerations. We acknowledge IAI's provision of an academic license for our experimental work.

Although we originally planned to include comparisons with the mixed-integer programming approach for optimal oblique decision tree learning [Zhu et al., 2020], we were unable to obtain access to their implementation.

Our experimental results, presented in Table 2, demonstrate that both our SMT-based and MaxSAT-based encodings consistently achieve superior training accuracy, validating our theoretical guarantee of discovering globally optimal oblique decision trees. Notably, the MaxSAT encodings solved with EvalMaxSAT demonstrated markedly better runtime performance compared to the SMT encodings solved with Z3.

To address scalability limitations with larger datasets, we conducted additional experiments using the incomplete MaxSAT solver NuWLS [Chu et al., 2023], configuring it with timeouts of 5 minutes and 1 hour. Although these configurations do not guarantee optimality, NuWLS provided high-quality solutions within the specified time limits. The results closely approximated those of the complete methods and, crucially, NuWLS successfully processed larger datasets where exact methods exceeded the 3-hour timeout threshold. In these cases, NuWLS solutions frequently outperformed heuristic approaches in terms of training accuracy.

Our comparative analysis revealed that our prototype consistently produced decision trees with superior training accuracy compared to both heuristic methods and the optimal axis-parallel method. However, HHCART and IAI, while significantly faster (typically completing in under one second) traded off solution quality for speed, as evidenced by their lower training accuracies.

Notably, IAI's implementation includes non-optional heuristic optimizations for runtime performance, which prevents direct measurement of the time required to find provably optimal decision trees. Moreover, in their original research [Bertsimas and Dunn, 2017], which focused primarily on demonstrating superior out-of-sample accuracy rather than computational efficiency, they reported that finding an optimal oblique decision tree of depth 2 for the Wine dataset required approximately 5 minutes. By contrast, our method achieves the same result in 40 seconds.

4.4 Synthetic Datasets

To complement our real-world dataset analysis with controlled evaluations, we conducted systematic experiments using synthetic datasets generated through a structured protocol. This approach allowed us to precisely measure the performance of our encodings under specific, controlled conditions.

In our first experimental series, illustrated in Figure 2, we examined the relationship between dataset size and computational efficiency. We generated synthetic datasets using random oblique decision trees with consistent parameters: four features, each with 100 possible values, two classes, and a tree depth of three. The dataset sizes varied to observe how computational time scales with the number of examples. The results demonstrated a polynomial growth in execution time as the dataset size increased. Notably, the SAT encoding consistently outperformed the SMT encoding by several orders of magnitude in terms of runtime efficiency.

In the second experimental series, presented in Figure 2, we investigated the impact of tree depth on computational complexity. We maintained a constant training dataset size of 64 examples and systematically increased the tree depth from low to higher values. Correspondingly, we adjusted the number of features to be equal to the tree depth plus one (i.e., number of features = depth + 1) for each iteration. The experiments revealed an exponential growth in execution time for both encodings as tree depth increased. However, the SAT encoding exhibited a significantly slower growth rate compared to the SMT encoding, indicating better scalability with respect to tree depth.

5 Conclusion

In this paper, we presented a novel approach for learning optimal oblique decision trees by formulating the problem as instances of (Max)SAT and SMT. Our novel contributions are a theoretical framework encoding the oblique decision tree learning problem as (Max)SAT or SMT, an efficient SAT encoding that uses geometric properties of linear separability, and empirical validation showing our method finds provably optimal oblique decision trees on small to medium-sized datasets. Notably, our SAT encoding significantly outperforms the SMT encoding in computational efficiency, often by several orders of magnitude.

Despite these advancements, computational complexity remains a significant challenge, especially for larger datasets and deeper trees. While our SAT-based approach scales better than SMT, both exhibit exponential growth in execution time with increasing tree depth due to the combinatorial nature of finding globally optimal decision trees. To mitigate scalability issues, we used incomplete MaxSAT solvers, which, although not guaranteeing optimality, provided high-quality solutions within practical time bounds for larger datasets. Our experiments show that incomplete MaxSAT solvers often outperform heuristic methods in training accuracy while operating within reasonable computational times.

Acknowledgements

We gratefully acknowledge the support of the Natural Sciences and Engineering Research Council of Canada (NSERC) [funding reference number RGPIN-2023-04468] and Fonds de recherche du Qu´ebec - Nature et technologies (FRQNT) [funding reference number 345904 : https://doi.org/10.69777/345904]. The benchmarks were carried out with support from Calcul Qu´ebec (calculquebec.ca) and the Digital Research Alliance of Canada (alliancecan.ca).