Article

Generating combinatorial test cases by efficient SAT encodings suitable for CDCL SAT solvers

Authors:

Mutsunori Banbara,

Haruki Matsunaka,

Naoyuki Tamura,

Katsumi InoueAuthors Info & Claims

LPAR'10: Proceedings of the 17th international conference on Logic for programming, artificial intelligence, and reasoning

Pages 112 - 126

Published: 10 October 2010 Publication History

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.

References

[1]

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).

Digital Library

[2]

Walsh, T.: SAT v CSP. In: Dechter, R. (ed.) CP 2000. LNCS, vol. 1894, pp. 441- 456. Springer, Heidelberg (2000).

Digital Library

[3]

Kasif, S.: On the parallel complexity of discrete relaxation in constraint satisfaction networks. Artificial Intelligence 45(3), 275-286 (1990).

Digital Library

[4]

Gent, I.P.: Arc consistency in SAT. In: Proceedings of the 15th European Conference on Artificial Intelligence (ECAI 2002), pp. 121-125 (2002).

[5]

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).

Digital Library

[6]

Iwama, K., Miyazaki, S.: SAT-variable complexity of hard combinatorial problems. In: Proceedings of the IFIP 13th World Computer Congress, pp. 253-258 (1994).

[7]

Gelder, A.V.: Another look at graph coloring via propositional satisfiability. Discrete Applied Mathematics 156(2), 230-243 (2008).

Digital Library

[8]

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).

Digital Library

[9]

Tamura, N., Taga, A., Kitagawa, S., Banbara, M.: Compiling finite linear CSP into SAT. Constraints 14(2), 254-272 (2009).

Digital Library

[10]

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).

Digital Library

[11]

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).

Digital Library

[12]

Chateauneuf, M.A., Kreher, D.L.: On the state of strength-three covering arrays. Journal of Combinatorial Designs 10(4), 217-238 (2002).

[13]

Hartman, A., Raskin, L.: Problems and algorithms for covering arrays. Discrete Mathematics 284(1-3), 149-156 (2004).

Digital Library

[14]

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).

Digital Library

[15]

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).

Digital Library

[16]

Nurmela, K.J.: Upper bounds for covering arrays by tabu search. Discrete Applied Mathematics 138(1-2), 143-152 (2004).

Digital Library

[17]

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).

Digital Library

[18]

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).

Digital Library

[19]

Bulutoglu, D., Margot, F.: Classification of orthogonal arrays by integer programming. Journal of Statistical Planning and Inference 138, 654-666 (2008).

[20]

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).

Digital Library

[21]

Hnich, B., Prestwich, S.D., Selensky, E., Smith, B.M.: Constraint models for the covering test problem. Constraints 11(2-3), 199-219 (2006).

Digital Library

[22]

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).

Digital Library

[23]

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).

Digital Library

[24]

Drescher, C., Walsh, T.: A translational approach to constraint answer set solving. TPLP 10(4-6), 465-480 (2010).

Digital Library

[25]

Zhang, H.: Combinatorial designs by sat solvers. In: Handbook of Satisfiability, pp. 533-568. IOS Press, Amsterdam (2009).

[26]

Colbourn, C.J.: Strength two covering arrays: Existence tables and projection. Discrete Mathematics 308(5-6), 772-786 (2008).

Digital Library

[27]

Sloane, N.J.A.: Covering arrays and intersecting codes. Journal of Combinatorial Designs 1, 51-63 (1993).

[28]

Seroussi, G., Bshouty, N.H.: Vector sets for exhaustive testing of logic circuits. IEEE Transactions on Information Theory 34(3), 513-522 (1988).

Digital Library

[29]

Colbourn, C.J.: Covering array tables (2010), http://www.public.asu.edu/~ccolbou/src/tabby/catable.html (Last Accessed on April 26, 2010).

[30]

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).

Digital Library

[31]

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).

Digital Library

[32]

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).

Digital Library

[33]

Yan, J., Zhang, J.: A backtracking search tool for constructing combinatorial test suites. Journal of Systems and Software 81(10), 1681-1693 (2008).

Digital Library

[34]

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).

Cited By

Luo CLyu SZhao QWu WZhang HHu CChristakis MPradel M(2024)Beyond Pairwise Testing: Advancing 3-wise Combinatorial Interaction Testing for Highly Configurable SystemsProceedings of the 33rd ACM SIGSOFT International Symposium on Software Testing and Analysis10.1145/3650212.3680309(641-653)Online publication date: 11-Sep-2024
https://dl.acm.org/doi/10.1145/3650212.3680309
Zhao QLuo CCai SWu WLin JZhang HHu CChandra SBlincoe KTonella P(2023)CAmpactor: A Novel and Effective Local Search Algorithm for Optimizing Pairwise Covering ArraysProceedings of the 31st ACM Joint European Software Engineering Conference and Symposium on the Foundations of Software Engineering10.1145/3611643.3616284(81-93)Online publication date: 30-Nov-2023
https://dl.acm.org/doi/10.1145/3611643.3616284
Luo CSong JZhao QLi YCai SHu C(2023)Generating Pairwise Covering Arrays for Highly Configurable Software SystemsProceedings of the 27th ACM International Systems and Software Product Line Conference - Volume A10.1145/3579027.3608998(261-267)Online publication date: 28-Aug-2023
https://dl.acm.org/doi/10.1145/3579027.3608998
Show More Cited By

Recommendations

CDCL(Crypto) SAT solvers for cryptanalysis
CASCON '19: Proceedings of the 29th Annual International Conference on Computer Science and Software Engineering

Over the last two decades we have seen a dramatic improvement in the efficiency of conflict-driven clause-learning Boolean satisfiability (CDCL SAT) solvers on industrial problems from a variety of domains. The availability of such a powerful general-...
Clause vivification by unit propagation in CDCL SAT solvers
Abstract
Original and learnt clauses in Conflict-Driven Clause Learning (CDCL) SAT solvers often contain redundant literals. This may have a negative impact on solver performance, because redundant literals may deteriorate both the ...
An effective learnt clause minimization approach for CDCL SAT solvers
IJCAI'17: Proceedings of the 26th International Joint Conference on Artificial Intelligence

Learnt clauses in CDCL SAT solvers often contain redundant literals. This may have a negative impact on performance because redundant literals may deteriorate both the effectiveness of Boolean constraint propagation and the quality of subsequent learnt ...

Comments

Please enable JavaScript to view thecomments powered by Disqus.

Information & Contributors

Information

Published In

cover image Guide Proceedings

LPAR'10: Proceedings of the 17th international conference on Logic for programming, artificial intelligence, and reasoning

October 2010

656 pages

ISBN:364216241X

Editors:
Christian G. Fermüller
TU Wien, Institut für Computersprachen 185.2, Theory and Logic Group, Vienna, Austria
,
Andrei Voronkov
University of Manchester, School of Computer Science, Manchester, UK

Publisher

Springer-Verlag

Berlin, Heidelberg

Publication History

Published: 10 October 2010

Qualifiers

Article

Contributors

Other Metrics

View Article Metrics

Bibliometrics & Citations

Bibliometrics

Article Metrics

11
Total Citations
View Citations
0
Total Downloads

Downloads (Last 12 months)0
Downloads (Last 6 weeks)0

Reflects downloads up to 22 Nov 2024

Other Metrics

View Author Metrics

Citations

Cited By

Luo CLyu SZhao QWu WZhang HHu CChristakis MPradel M(2024)Beyond Pairwise Testing: Advancing 3-wise Combinatorial Interaction Testing for Highly Configurable SystemsProceedings of the 33rd ACM SIGSOFT International Symposium on Software Testing and Analysis10.1145/3650212.3680309(641-653)Online publication date: 11-Sep-2024
https://dl.acm.org/doi/10.1145/3650212.3680309
Zhao QLuo CCai SWu WLin JZhang HHu CChandra SBlincoe KTonella P(2023)CAmpactor: A Novel and Effective Local Search Algorithm for Optimizing Pairwise Covering ArraysProceedings of the 31st ACM Joint European Software Engineering Conference and Symposium on the Foundations of Software Engineering10.1145/3611643.3616284(81-93)Online publication date: 30-Nov-2023
https://dl.acm.org/doi/10.1145/3611643.3616284
Luo CSong JZhao QLi YCai SHu C(2023)Generating Pairwise Covering Arrays for Highly Configurable Software SystemsProceedings of the 27th ACM International Systems and Software Product Line Conference - Volume A10.1145/3579027.3608998(261-267)Online publication date: 28-Aug-2023
https://dl.acm.org/doi/10.1145/3579027.3608998
Luo CZhao QCai SZhang HHu CRoychoudhury ACadar CKim M(2022)SamplingCA: effective and efficient sampling-based pairwise testing for highly configurable software systemsProceedings of the 30th ACM Joint European Software Engineering Conference and Symposium on the Foundations of Software Engineering10.1145/3540250.3549155(1185-1197)Online publication date: 7-Nov-2022
https://dl.acm.org/doi/10.1145/3540250.3549155
Luo CSun BQiao BChen JZhang HLin JLin QZhang DSpinellis DGousios GChechik MDi Penta M(2021)LS-sampling: an effective local search based sampling approach for achieving high t-wise coverageProceedings of the 29th ACM Joint Meeting on European Software Engineering Conference and Symposium on the Foundations of Software Engineering10.1145/3468264.3468622(1081-1092)Online publication date: 20-Aug-2021
https://dl.acm.org/doi/10.1145/3468264.3468622
Luo CLin JCai SChen XHe BQiao BZhao PLin QZhang HWu WRajmohan SZhang D(2021)AutoCCAGProceedings of the 43rd International Conference on Software Engineering10.1109/ICSE43902.2021.00030(201-212)Online publication date: 22-May-2021
https://dl.acm.org/doi/10.1109/ICSE43902.2021.00030
Lin JCai SLuo CLin QZhang HDumas MPfahl DApel SRusso A(2019)Towards more efficient meta-heuristic algorithms for combinatorial test generationProceedings of the 2019 27th ACM Joint Meeting on European Software Engineering Conference and Symposium on the Foundations of Software Engineering10.1145/3338906.3338914(212-222)Online publication date: 12-Aug-2019
https://dl.acm.org/doi/10.1145/3338906.3338914
Petke JGay GAntoniol G(2015)ConstraintsProceedings of the Eighth International Workshop on Search-Based Software Testing10.5555/2821339.2821344(17-18)Online publication date: 16-May-2015
https://dl.acm.org/doi/10.5555/2821339.2821344
Bruce BPetke JHarman MEsparcia-Alcázar A(2015)Reducing Energy Consumption Using Genetic ImprovementProceedings of the 2015 Annual Conference on Genetic and Evolutionary Computation10.1145/2739480.2754752(1327-1334)Online publication date: 11-Jul-2015
https://dl.acm.org/doi/10.1145/2739480.2754752
Lin JLuo CCai SSu KHao DZhang LCohen MGrunske LWhalen M(2015)TCAProceedings of the 30th IEEE/ACM International Conference on Automated Software Engineering10.1109/ASE.2015.61(494-505)Online publication date: 9-Nov-2015
https://dl.acm.org/doi/10.1109/ASE.2015.61
Show More Cited By

View Options

View options

Media

Figures

Other

Tables

View Table of Contents