An incremental MaxSAT-based model to learn interpretable and balanced classification rules

The success of Machine Learning (ML) in recent years has led to a growing advancement in studies in this area [2, 8, 12]. Several applications have emerged with the aim of circumventing various problems and situations [4, 14, 20]. One such problem is the lack of explainability of prediction models. This directly affects the reliability of using these applications in critical situations involving, for example, finance, autonomous systems, damage to equipment, the environment, and even lives [1, 7, 23]. That said, some works seek to develop approaches that bring explainability to their predictions [13, 21, 22].

Precise predictions with high levels of interpretability are often not a simple task. There are some works that try to solve this problem by balancing the accuracy of the prediction with the interpretability [5, 9, 17, 24, 6, 16, 15]. It can be seen that some of these works use approaches based on the Boolean Satisfiability Problem (SAT) and the Maximum Boolean Satisfiability Problem (MaxSAT). The choice of these approaches to solve this problem has been increasingly recurrent in recent years. The reasons can be seen in the results obtained by these models.

SAT-based approaches have been proposed recently [18, 19] to learn quantifier-free first-order sentences from a set of classified strings. More specifically, given a set of classified strings, the goal is to find a first-order sentence over strings of minimum size that correctly classifies all the strings. One of the approaches demonstrated is SQFSAT (Synthesis of quantifier-free first-order sentences over strings with SAT). Upon receiving a set of classified strings, this approach generates a quantifier-free first-order sentence over strings in disjunctive normal form (DNF) with a given number of terms. What makes this method stand out is the fact that we can limit both the number of terms and the number of formulas per term in the generated formula. In addition, as the approach generates formulas in DNF, each term of the formula can be seen as a rule. Then, for each rule, its explanation is the conjunction of formulas in the rule, which can be interesting for their interpretability [11, 18]. On the other hand, as the model is based on the SAT problem, in certain situations it may bring results that are not so interesting in terms of interpretability and efficiency, such as in cases where the set of strings is large.

Ghosh, B. et al. created a classification model based on MaxSAT called IMLI [6]. The approach takes a set of classified samples, represented by vectors of numerical and categorical data, and generates a set of rules expressed in DNF or in conjunctive normal form (CNF) that correctly classifies as many samples as possible. In this work, we focus on using IMLI for learning rules in DNF. The number of rules in the set of rules can be defined similarly to SQFSAT, but IMLI does not consider the number of elements per rule. Although IMLI focuses on learning a sparse set of rules, it may obtain a combination of both large and small rules. IMLI also takes into account the option of defining a weighting for correct classifications. As the weighting increases, the accuracy of the model improves, but at the cost of an increase in the size of the generated set of rules. The smaller the weighting, the lower the accuracy of the model, but correspondingly, the generated set of rules tends to be smaller. Furthermore, IMLI uses an incremental approach to achieve better runtime performance. The incremental form consists of dividing the set of samples into partitions in order to generate a set of rules for each partition from the set of rules obtained in the previous partitions.

In this work, we aim to create a new approach for learning interpretable rules based on MaxSAT that unites SQFSAT with the incrementability of IMLI. The motivation for choosing SQFSAT is the possibility of defining the number of literals per clause, allowing us to generate smaller and more balanced rules. The choice of IMLI is motivated by its incrementability technique, which allows the method to train on large sets of samples efficiently. In addition, we propose a technique that reduces the size of the generated rules, removing possible redundancies.

This work is divided into 6 sections. In Section 2, we define the general notions and notations. Since all methods presented in this paper use Boolean logic, we also define in Section 2 how these methods binarize datasets with numerical and categorical data. In Section 3, SQFSAT and IMLI are presented, respectively. We present SQFSAT in the context of our work where samples consist of binary vectors instead of strings, and elements of rules are not first-order sentences over strings. In Section 4, our contribution is presented: IMLIB. In Section 5, we describe the experiments conducted and the results for the comparison of our approach against IMLI. Finally, in the last section, we present the conclusions and indicate future work.

We consider the binary classification problem where we are given a set of samples and their classifications. The set of samples is represented by a binary matrix of size $n\times m$ and their classifications by a vector of size $n$. We call the matrix X and the vector y. Each row of X is a sample of the set and we will call it $\textbf{X}_{i}$ with $i\in\{1,...,n\}$. To represent a specific value of $\textbf{X}_{i}$, we will use $x_{i,j}$ with $j\in\{1,...,m\}$. Each column of X has a label representing a feature and the label is symbolized by $x^{j}$. To represent a specific value of y, we will use $y_{i}$.

To represent the opposite value of $y_{i}$, that is, if it is $1$ the opposite value is $0$ and vice versa, we use $\lnot y_{i}$. Therefore, we will use the symbol $\lnot\textbf{y}$ to represent y with all opposite values. To represent the opposite value of $x_{i,j}$, we use $\lnot x_{i,j}$. Therefore, we will use the symbol $\lnot\textbf{X}_{i}$ to represent $\textbf{X}_{i}$ with all opposite values. Each label also has its opposite label which is symbolized by $\lnot x^{j}$.

A partition of X is represented by $\textbf{X}^{t}$ with $t\in\{1,...,p\}$, where $p$ is the number of partitions. Therefore, the partitions of vector y are represented by $\textbf{y}^{t}$. Each element of y is symbolized by $y_{i}$ and represents the class value of sample $\textbf{X}_{i}$. We use $\mathcal{E}^{-}=\{X_{i}\mid y_{i}=0,1\leq i\leq n\}$ and $\mathcal{E}^{+}=\{X_{i}\mid y_{i}=1,1\leq i\leq n\}$. To represent the size of these sets, that is, the number of samples contained in them, we use the notations: $|\mathcal{E}^{-}|$ and $|\mathcal{E}^{+}|$.

As we assume a set of binary samples, we need to perform some preprocessing. Preprocessing consists of binarizing a set of samples with numerical or categorical values. The algorithm divides the features into four types: constant, where all samples have the same value; binary, where there are only two distinct variations among all the samples for the same value; categorical, when the feature does not fit in constant and binary and its values are three or more categories; ordinal, when the feature does not fit into constant and binary and has numerical values.

When the feature type is constant, the algorithm discards that feature. This happens due to the fact that a feature common to all samples makes no difference in the generated rules. When the type is binary, one of the feature variations will receive $0$ and the other $1$ as new values. If the type is categorical, we employ the widely recognized technique of one-hot encoding. Finally, for the ordinal type feature, a quantization is performed, that is, the variations of this feature are divided into quantiles. With this, Boolean values are assigned to each quantile according to the original value.

We use SAT and MaxSAT solvers to implement the methods presented in this work. A solver receives a formula in CNF, for example: $(p\lor q)\land(q\lor\lnot p)$. Furthermore, a MaxSAT solver receives weights that will be assigned to each clause in the formula. A clause is the disjunction of one or more literals. The weights are represented by $W(Cl)=w$ where $Cl$ is one or more clauses and $w$ represents the weight assigned to each one of them. A SAT solver tries to assign values to the literals in such a way that all clauses are satisfied. A MaxSAT solver tries to assign values to the literals in a way that the sum of the weights of satisfied clauses is maximum. Clauses with numerical weights are considered soft. The greater the weight, the greater the priority of the clause to be satisfied. Clauses assigned a weight of $\infty$ are considered hard and must be satisfied.

In this section, we will present our method IMLIB which is an incremental version of SQFSAT based on MaxSAT. IMLIB also has a technique for reducing the size of the generated set of rules. Therefore, our approach partitions the set of samples X. Moreover, our method has one more constraint and weight on all clauses. With that, our approach receives five input parameters X, y, $k$, $l$, $\lambda$ and tries to obtain the smallest R that correctly classifies as many samples as possible, penalizing classification errors with $\lambda$, that is, $\min_{\textbf{R}}\{|\textbf{R}|+\lambda|\mathcal{E}_{R}|\mid\mathcal{E}_{R}=\{\textbf{X}_{i}\mid\textbf{R}(\textbf{X}_{i})\neq y_{i}\}\}$. That said, below, we will show the constraints of our approach for constructing MaxSAT clauses.

Constraints that guarantee that exactly only one $u_{o,d}^{j}$ is true for the $d$th feature of the rule $R_{o}$:

Constraints representing that the model will try to insert as few features as possible in R:

Conjunction of clauses that guarantees that each rule has at least one feature:

The following conjunction of formulas ensures that $e_{o,d,i}$ is true if the $j$th feature label in the $o$th rule contributes to correctly classify sample $\textbf{X}_{i}$:

Conjunction of formulas guaranteeing that the classification of a specific rule will not be interfered by skipped features in the rule:

Conjunction of formulas indicating that the model assigns true to $z_{o,i}$ if all the features of rule $R_{o}$ support the correct classification of sample $\textbf{X}_{i}$:

Conjunction of clauses designed to generate a set of rules R that correctly classify as many samples as possible:

Finally, after converting formula $Q$ below to CNF, we have the MaxSAT query that is sent to the solver.

In this section, we present the experiments we conducted to compare our method IMLIB against IMLI. The two models were implemented¹¹1Source code of IMLIB and the implementation of the tests performed can be found at the link: https://github.com/cacajr/decision_set_models with Python and MaxSAT solver RC2 [10]. The experiments were carried out on a machine with the following configurations: Intel(R) Core(TM) i5-4460 3.20GHz processor, and 12GB of RAM memory. Ten databases from the UCI repository [3] were used to compare IMLI with IMLIB. Information on the datasets can be seen in Table 1. Databases that have more than two classes were adapted, considering that both models are designed for binary classification. For purposes of comparison, we measure the following metrics: number of rules, size of the set of rules, size of the largest rule, accuracy on test data and training time. The number of rules, size of the set of rules, and size of the largest rule can be used as interpretability metrics. For example, a set of rules with few rules and small rules is more interpretable than one with many large rules.

Each dataset was split into $80\%$ for training and $20\%$ for testing. Both models were trained and evaluated using the same training and test sets, as well as the same random distribution. Then, the way the experiments were conducted ensured that both models had exactly the same set of samples to learn the set of rules.

For both IMLI and IMLIB, we consider parameter configurations obtained by combining values of: $k\in\{1,2,3\}$, $\lambda\in\{5,10\}$ and $lp\in\{8,16\}$, where $lp$ is the number of samples per partition. Since IMLIB has the maximum number of features per rule $l$ as an extra parameter, for each parameter configuration of IMLI and its corresponding $\mathbf{R}$, we considered $l$ ranging from $1$ to one less than the size of the largest rule in $\mathbf{R}$. Thus, the value of $l$ that resulted in the best test accuracy was chosen to be compared with IMLI. Our objective is to evaluate whether IMLIB can achieve higher test accuracy compared to IMLI by employing smaller and more balanced rules. Furthermore, it should be noted that this does not exclude the possibility of our method generating sets of rules with larger sizes than IMLI.

For each dataset and each parameter configuration of $k$, $\lambda$ and $lp$, we conducted ten independent realizations of this experiment. For each dataset, the parameter configuration with the best average of test accuracy for IMLI was chosen to be inserted in Table 2. For each dataset, the parameter configuration with the best average of test accuracy for IMLIB was chosen to be inserted in Table 3. The results presented in both tables are the average over the ten realizations.

In Table 2, when considering parameter configurations that favor IMLI, we can see that IMLIB stands out in the size of the generated set of rules and in the size of the largest rule in datasets. Furthermore, our method achieved equal or higher accuracy compared to IMLI in four out of ten datasets. In datasets where IMLI outperformed IMLIB in terms of accuracy, our method exhibited a modest average performance gap of only three percentage points. Besides, IMLI outperformed our method in terms of training time in all datasets.

In Table 3, when we consider parameter configurations that favor our method, we can see that IMLIB continues to stand out in terms of the size of the generated set of rules and the size of the largest rule in all datasets. Moreover, our method achieved equal or higher accuracy than IMLI in all datasets. Again, IMLI consistently demonstrated better training time performance compared to IMLIB across all datasets.

As an illustrative example of interpretability, we present a comparison of the sizes of rules learned by both methods in the Mushroom dataset. Table 4 shows the sizes of rules obtained in all ten realizations of the experiment. We can observe that IMLIB consistently maintains a smaller and more balanced set of rules across the different realizations. This is interesting because unbalanced rules can affect interpretability. See realization $6$, for instance. The largest rule learned by IMLI has a size of $10$, nearly double the size of the remaining rules. In contrast, IMLIB learned a set of rules where the size of the largest rule is $6$ and the others have similar sizes. Thus, interpreting three rules of size at most $6$ is easier than interpreting a rule of size $10$. Also as illustrative examples of interpretability, we can see some sets of rules learned by IMLIB in Table 5.

In this work, we present a new incremental model for learning interpretable and balanced rules: IMLIB. Our method leverages the strengths of SQFSAT, which effectively constrains the size of rules, while incorporating techniques from IMLI, such as incrementability, cost for classification errors, and minimization of the set of rules. Our experiments demonstrate that the proposed approach generates smaller and more balanced rules than IMLI, while maintaining comparable or even superior accuracy in many cases. We argue that sets of small rules with approximately the same size seem more interpretable when compared to sets with a few large rules. As future work, we plan to develop a version of IMLIB that can classify sets of samples with more than two classes, enabling us to compare this approach with multiclass interpretable rules from the literature [11, 24].