Incomplete MaxSAT Approaches for Combinatorial Testing

TL;DR

This paper introduces a SAT-based method using MaxSAT technology to efficiently generate optimal and suboptimal solutions for combinatorial testing problems involving constraints, demonstrating strong experimental performance.

Contribution

It presents novel MaxSAT encodings and algorithms for the Covering Array Number and Tuple Number problems, including an incomplete approach for constrained instances.

Findings

Effective MaxSAT encodings for the problems.

Competitive performance on benchmark datasets.

Successful extension to constrained problems.

Abstract

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.