Since 2006, the MaxSAT Evaluation (MSE) Bacchus et al. [2022] has been held annually with the primary objective of advancing MaxSAT technology and assessing its current state-of-the-art. The evaluation consists of multiple solvers being tested on various benchmarks across different evaluation tracks. This event has undeniably spurred the MaxSAT community to create more cutting-edge solvers and enhance their competitiveness. It is not surprising that solver performance depends on several factors, including the power of the algorithm implemented by the solver, proper configuration of solver parameters to unleash its full potential, and implementation issues. Therefore, we must interpret the MaxSAT Evaluation ranking results carefully and derive conclusions according to the goal of our analysis.

Combinatorial Testing (CT) tools are essential to test properly a wide range of systems (train systems, Graphical User Interfaces (GUIs), autonomous driving systems, etc). While there is an active research community working on developing CT tools, paradoxically little attention has been paid to making available enough resources to test the CT tools themselves. In particular, the set of available benchmarks to asses their correctness, effectiveness and efficiency is rather limited. In this paper, we introduce a new generator of CT benchmarks that essentially borrows the structure contained in the plethora of available Combinatorial Problems from other research communities in order to create meaningful benchmarks. We additionally perform an extensive evaluation of CT tools with these new benchmarks. Thanks to this study we provide some insights on under which circumstances a particular CT tool should be used.

Recently, there has been a growing interest in creating synergies between Combinatorial Optimization (CO) and Machine Learning (ML), and vice-versa. This is a natural connection since ML algorithms can be seen in essence as optimization algorithms that try to minimize prediction error. In this paper, we focus on how CO techniques can be applied to improve decision tree classifiers in ML. A decision tree classifier is a supervised ML technique that builds a tree-structured classifier, where internal nodes represent the features of a dataset, branches represent the decision rules and each leaf node represents the outcome. In essence, every path from the root to a leaf is a classification rule that determines to which class belongs the input query.

We present a Satisfiability (SAT)-based approach for building Mixed Covering Arrays with Constraints of minimum length, referred to as the Covering Array Number problem. This problem is central in Combinatorial Testing for the detection of system failures. In particular, we show how to apply Maximum Satisfiability (MaxSAT) technology by describing efficient encodings for different classes of complete and incomplete MaxSAT solvers to compute optimal and suboptimal solutions, respectively. Similarly, we show how to solve through MaxSAT technology a closely related problem, the Tuple Number problem, which we extend to incorporate constraints. For this problem, we additionally provide a new MaxSAT-based incomplete algorithm. The extensive experimental evaluation we carry out on the available Mixed Covering Arrays with Constraints benchmarks and the comparison with state-of-the-art tools confirm the good performance of our approaches.