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.
翻译:我们提出了一个基于满足性(SAT)的方法,用于构建具有最小长度限制的混合覆盖阵列,称为覆盖性阵列编号问题。这个问题在检测系统故障的组合测试中至关重要。特别是,我们通过描述不同类别完整和不完全的最大满足性(MAxSAT)解答器的有效编码,分别计算最佳和亚最佳解决方案,来显示如何通过MaxSAT技术解决一个密切相关的问题,即“图普列号问题”,我们将这一问题扩大到包括制约。对于这个问题,我们提供了一个新的基于MaxSAT的不完整算法。我们对现有混合覆盖阵列与制约基准进行的广泛实验评估,以及与最新工具的比较,证实了我们方法的良好表现。