Abstract
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.
Access provided by Autonomous University of Puebla. Download to read the full chapter text
Chapter PDF
Similar content being viewed by others
Keywords
- Original Matrix
- Generate Test Case
- Combinatorial Design
- Conjunctive Normal Form Formula
- Coverage Constraint
These keywords were added by machine and not by the authors. This process is experimental and the keywords may be updated as the learning algorithm improves.
References
de Kleer, J.: A comparison of ATMS and CSP techniques. In: Proceedings of the 11th International Joint Conference on Artificial Intelligence (IJCAI 1989), pp. 290–296 (1989)
Walsh, T.: SAT v CSP. In: Dechter, R. (ed.) CP 2000. LNCS, vol. 1894, pp. 441–456. Springer, Heidelberg (2000)
Kasif, S.: On the parallel complexity of discrete relaxation in constraint satisfaction networks. Artificial Intelligence 45(3), 275–286 (1990)
Gent, I.P.: Arc consistency in SAT. In: Proceedings of the 15th European Conference on Artificial Intelligence (ECAI 2002), pp. 121–125 (2002)
Selman, B., Levesque, H.J., Mitchell, D.G.: A new method for solving hard satisfiability problems. In: Proceedings of the 10th National Conference on Artificial Intelligence (AAAI 1992), pp. 440–446 (1992)
Iwama, K., Miyazaki, S.: SAT-variable complexity of hard combinatorial problems. In: Proceedings of the IFIP 13th World Computer Congress, pp. 253–258 (1994)
Gelder, A.V.: Another look at graph coloring via propositional satisfiability. Discrete Applied Mathematics 156(2), 230–243 (2008)
Tamura, N., Taga, A., Kitagawa, S., Banbara, M.: Compiling finite linear CSP into SAT. In: Benhamou, F. (ed.) CP 2006. LNCS, vol. 4204, pp. 590–603. Springer, Heidelberg (2006)
Tamura, N., Taga, A., Kitagawa, S., Banbara, M.: Compiling finite linear CSP into SAT. Constraints 14(2), 254–272 (2009)
Gavanelli, M.: The log-support encoding of CSP into SAT. In: Bessière, C. (ed.) CP 2007. LNCS, vol. 4741, pp. 815–822. Springer, Heidelberg (2007)
Williams, A.W.: Determination of test configurations for pair-wise interaction coverage. In: Proceedings of 13th International Conference on Testing Communicating Systems (TestCom 2000), pp. 59–74 (2000)
Chateauneuf, M.A., Kreher, D.L.: On the state of strength-three covering arrays. Journal of Combinatorial Designs 10(4), 217–238 (2002)
Hartman, A., Raskin, L.: Problems and algorithms for covering arrays. Discrete Mathematics 284(1-3), 149–156 (2004)
Cohen, D.M., Dalal, S.R., Fredman, M.L., Patton, G.C.: The AETG system: An approach to testing based on combinatiorial design. IEEE Transactions on Software Engineering 23(7), 437–444 (1997)
Lei, Y., Tai, K.C.: In-parameter-order: A test generation strategy for pairwise testing. In: Proceedings of 3rd IEEE International Symposium on High-Assurance Systems Engineering (HASE 1998), pp. 254–261 (1998)
Nurmela, K.J.: Upper bounds for covering arrays by tabu search. Discrete Applied Mathematics 138(1-2), 143–152 (2004)
Cohen, M.B., Gibbons, P.B., Mugridge, W.B., Colbourn, C.J.: Constructing test suites for interaction testing. In: Proceedings of the 25th International Conference on Software Engineering (ICSE 2003), pp. 38–48 (2003)
Shiba, T., Tsuchiya, T., Kikuno, T.: Using artificial life techniques to generate test cases for combinatorial testing. In: Proceedings of 28th International Computer Software and Applications Conference (COMPSAC 2004), pp. 72–77 (2004)
Bulutoglu, D., Margot, F.: Classification of orthogonal arrays by integer programming. Journal of Statistical Planning and Inference 138, 654–666 (2008)
Hnich, B., Prestwich, S.D., Selensky, E.: Constraint-based approaches to the covering test problem. In: Faltings, B.V., Petcu, A., Fages, F., Rossi, F. (eds.) CSCLP 2004. LNCS (LNAI), vol. 3419, pp. 172–186. Springer, Heidelberg (2005)
Hnich, B., Prestwich, S.D., Selensky, E., Smith, B.M.: Constraint models for the covering test problem. Constraints 11(2-3), 199–219 (2006)
Lopez-Escogido, D., Torres-Jimenez, J., Rodriguez-Tello, E., Rangel-Valdez, N.: Strength two covering arrays construction using a sat representation. In: Gelbukh, A., Morales, E.F. (eds.) MICAI 2008. LNCS (LNAI), vol. 5317, pp. 44–53. Springer, Heidelberg (2008)
Cohen, M.B., Dwyer, M.B., Shi, J.: Constructing interaction test suites for highly-configurable systems in the presence of constraints: A greedy approach. IEEE Trans. Software Eng. 34(5), 633–650 (2008)
Drescher, C., Walsh, T.: A translational approach to constraint answer set solving. TPLP 10(4-6), 465–480 (2010)
Zhang, H.: Combinatorial designs by sat solvers. In: Handbook of Satisfiability, pp. 533–568. IOS Press, Amsterdam (2009)
Colbourn, C.J.: Strength two covering arrays: Existence tables and projection. Discrete Mathematics 308(5-6), 772–786 (2008)
Sloane, N.J.A.: Covering arrays and intersecting codes. Journal of Combinatorial Designs 1, 51–63 (1993)
Seroussi, G., Bshouty, N.H.: Vector sets for exhaustive testing of logic circuits. IEEE Transactions on Information Theory 34(3), 513–522 (1988)
Colbourn, C.J.: Covering array tables (2010), http://www.public.asu.edu/~ccolbou/src/tabby/catable.html (Last Accessed on April 26, 2010)
Régin, J.C.: Generalized arc consistency for global cardinality constraint. In: Proceedings of the 13th National Conference on Artificial Intelligence (AAAI 1996), vol. 1, pp. 209–215 (1996)
Flener, P., Frisch, A.M., Hnich, B., Kiziltan, Z., Miguel, I., Pearson, J., Walsh, T.: Breaking row and column symmetries in matrix models. In: Van Hentenryck, P. (ed.) CP 2002. LNCS, vol. 2470, pp. 462–476. Springer, Heidelberg (2002)
Grayland, A., Miguel, I., Roney-Dougal, C.M.: Snake lex: An alternative to double lex. In: Gent, I.P. (ed.) CP 2009. LNCS, vol. 5732, pp. 391–399. Springer, Heidelberg (2009)
Yan, J., Zhang, J.: A backtracking search tool for constructing combinatorial test suites. Journal of Systems and Software 81(10), 1681–1693 (2008)
Eén, N., Sörensson, N.: An extensible SAT-solver. In: Giunchiglia, E., Tacchella, A. (eds.) SAT 2003. LNCS, vol. 2919, pp. 502–518. Springer, Heidelberg (2004)
Author information
Authors and Affiliations
Editor information
Editors and Affiliations
Rights and permissions
Copyright information
© 2010 Springer-Verlag Berlin Heidelberg
About this paper
Cite this paper
Banbara, M., Matsunaka, H., Tamura, N., Inoue, K. (2010). Generating Combinatorial Test Cases by Efficient SAT Encodings Suitable for CDCL SAT Solvers . In: Fermüller, C.G., Voronkov, A. (eds) Logic for Programming, Artificial Intelligence, and Reasoning. LPAR 2010. Lecture Notes in Computer Science, vol 6397. Springer, Berlin, Heidelberg. https://doi.org/10.1007/978-3-642-16242-8_9
Download citation
DOI: https://doi.org/10.1007/978-3-642-16242-8_9
Publisher Name: Springer, Berlin, Heidelberg
Print ISBN: 978-3-642-16241-1
Online ISBN: 978-3-642-16242-8
eBook Packages: Computer ScienceComputer Science (R0)