Generating test cases for combinatorial testing is to find a covering array in Combinatorial Designs. In this paper, we consider the problem of finding optimal covering arrays by SAT encoding. We present two encodings suitable for modern CDCL SAT solvers. One is based on the order encoding that is efficient in the sense that unit propagation achieves the bounds consistency in CSPs. Another one is based on a combination of the order encoding and Hnich's encoding. CDCL SAT solvers have an important role in the latest SAT technology. The effective use of them is essential for enhancing efficiency. In our experiments, we found solutions that can be competitive with the previously known results for the arrays of strength two to six with small to moderate size of components and symbols. Moreover, we succeeded either in proving the optimality of known bounds or in improving known lower bounds for some arrays. © 2010 Springer-Verlag.
CITATION STYLE
Banbara, M., Matsunaka, H., Tamura, N., & Inoue, K. (2010). Generating combinatorial test cases by efficient SAT encodings suitable for CDCL SAT solvers. In Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics) (Vol. 6397 LNCS, pp. 112–126). Springer Verlag. https://doi.org/10.1007/978-3-642-16242-8_9
Mendeley helps you to discover research relevant for your work.