Incomplete MaxSAT approaches for combinatorial testing
Tóm tắt
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.
Tài liệu tham khảo
Alviano, M., Dodaro, C., Ricca, F.: A maxsat algorithm using cardinality constraints of bounded size. In: Twenty-Fourth International Joint Conference on Artificial Intelligence, (2015)
Ansótegui, C., Izquierdo, I., Manyà, F., Torres-Jiménez, J.: A max-sat-based approach to constructing optimal covering arrays. In: Proceedings of the 16th International Conference of the Catalan Association for Artificial Intelligence Artificial Intelligence Research and Development, Vic, Catalonia, Spain, October 23-25, 2013, pp. 51–59 (2013)
Ansótegui, C., Manyà, F.: Mapping problems with finite-domain variables into problems with boolean variables. In: SAT 2004 - The Seventh International Conference on Theory and Applications of Satisfiability Testing, 10-13 May 2004, Vancouver, BC, Canada, Online Proceedings, pp. 1–15 (2004)
Ansótegui, C., Ojeda, J., Pacheco, A., Pon, J., Salvia, J. M., Torres, E.: Optilog: A framework for sat-based systems. In: SAT 2021, Cham, pp. 1–10 (2021)
Ansótegui, C., Gabàs, J.: WPM3: an (in)complete algorithm for weighted partial MaxSAT. Artif. Intell. 250, 37–57 (2017)
Ansótegui, C., Bonet, M.L., Levy, J.: Solving (Weighted) Partial MaxSAT through Satisfiability Testing. In: Kullmann, O. (ed.) Theory and Applications of Satisfiability Testing - SAT 2009. Lecture Notes in Computer Science, pp. 427–440. Springer, Berlin (2009)
Ansótegui, C., Bonet, M.L., Gabàs, J., Levy, J.: Improving SAT-Based Weighted MaxSAT Solvers. In: Milano, M. (ed.) Principles and Practice of Constraint Programming. Lecture Notes in Computer Science, pp. 86–101. Springer, Berlin (2012)
Ansótegui, C., Izquierdo, I., Manyà, F., Jiménez, J.T.: A max-sat-based approach to constructing optimal covering arrays. Front. Artif. Intell. Appl. 256, 51–59 (2013)
Ansótegui, C., Bonet, M.L., Levy, J.: Sat-based maxsat algorithms. Artif. Intell. 196, 77–105 (2013)
Ansótegui, C., Gabàs, J., Levy, J.: Exploiting subproblem optimization in SAT-based MaxSAT algorithms. J. Heuristics 22(1), 1–53 (2016)
Audemard, G., Lagniez, J.-M., Simon, L.: Improving glucose for incremental sat solving with assumptions: application to mus extraction. In: International conference on theory and applications of satisfiability testing, Springer, pp. 309–317 (2013)
Avellaneda, F.: A short description of the solver evalmaxsat, MaxSAT Evaluation 2020 8
Bacchus, F., Berg, J., Järvisalo, M., Martins, R.: Maxsat evaluation 2020: solver and benchmark descriptions (2020)
Bacchus, F.: Maxhs in the maxsat evaluation. MaxSAT Evaluat. 2020, 19 (2020)
Banbara, M., Matsunaka, H., Tamura, N., Inoue, K.: 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, pp. 112–126. Springer, Berlin (2010)
Berg, J., Demirovic, E., Stuckey, P.: Loandra in the MaxSAT evaluation. MaxSAT Evaluat 2020, 10 (2020)
Biere, A., Heule, M., van Maaren, H., Walsh, T.: (Eds.), Handbook of Satisfiability, Vol. 185 of Frontiers in Artificial Intelligence and Applications, IOS Press, (2009)
Borazjany, M.N., Yu, L., Lei, Y., Kacker, R., Kuhn, R.: Combinatorial testing of ACTS: A case study. In: Proceedings of the Fifth IEEE International Conference on Software Testing, Verification and Validation, ICST 2012, Montreal, QC, Canada, April 17-21, 2012, pp. 591–600 (2012)
Bryce, R. C., Colbourn, C. J., Cohen, M.B.: A framework of greedy methods for constructing interaction test suites. In: Proceedings of the 27th International Conference on Software Engineering (ICSE 2005), 15-21 May 2005, St. Louis, Missouri, USA, pp. 146–155 (2005)
Carrizales-Turrubiates, O., Rangel-Valdez, N., Torres-Jiménez, J.: Optimal shortening of covering arrays. In: Batyrshin, I.Z., Sidorov, G. (Eds.), Advances in Artificial Intelligence - 10th Mexican International Conference on Artificial Intelligence, MICAI 2011, Puebla, Mexico, November 26 - December 4, 2011, Proceedings, Part I, Vol. 7094 of Lecture Notes in Computer Science, Springer, pp. 198–209 (2011)
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. Softw. Eng. 34(5), 633–650 (2008)
Colbourn, C.J.: Combinatorial aspects of covering arrays. Le Matematiche 59(1,2), 125–172 (2004)
Czerwonka, J.: Pairwise testing in real world. In: Proceedings of the 24th Annual Pacific Northwest Software Quality Conference, 10-11 October 2006, Portland, Oregon, pp. 419–430 (2006)
Duan, F., Lei, Y., Yu, L., Kacker, R.N., Kuhn, D.R.: Optimizing ipog’s vertical growth with constraints based on hypergraph coloring. In: 2017 IEEE International Conference on Software Testing, Verification and Validation Workshops, ICST Workshops 2017, Tokyo, Japan, March 13-17, 2017, pp. 181–188 (2017)
Eén, N., Sörensson, N.: Translating Pseudo-Boolean Constraints into SAT, Journal on Satisfiability, Boolean Modeling and Computation 2 (1-4) 1–26, publisher: IOS Press (2006)
Flener, P., Frisch, A. M., Hnich, B., Kiziltan, Z., Miguel, I., Pearson, J., Walsh, T.: Breaking row and column symmetries in matrix models. In: 8th International Conference on Principles and Practice of Constraint Programming - CP 2002, CP 2002, Ithaca, NY, USA, September 9-13, 2002, Proceedings, pp. 462–476 (2002)
Fu, Z., Malik, S.: On solving the partial max-sat problem. In: Biere, A., Gomes, C.P. (eds.) Theory and Applications of Satisfiability Testing - SAT 2006, pp. 252–265. Springer, Berlin (2006)
Gent, I. P., Nightingale, P.: A new encoding of alldifferent into sat. In: International Workshop on Modelling and Reformulating Constraint Satisfaction, pp. 95–110 (2004)
Gomes, C., Sellmann, M.: Streamlined constraint reasoning. In: Wallace, M. (ed.) Principles and Practice of Constraint Programming - CP 2004, pp. 274–289. Springer, Berlin (2004)
Hnich, B., Prestwich, S., Selensky, E.: Constraint-based approaches to the covering test problem. In: Faltings, B.V., Petcu, A., Fages, F., Rossi, F. (eds.) Recent Advances in Constraints, pp. 172–186. Springer, Berlin (2005)
Hnich, B., Prestwich, S.D., Selensky, E., Smith, B.M.: Constraint models for the covering test problem. Constraints 11(2), 199–219 (2006)
Ignatiev, A.: Rc2-2018@ maxsat evaluation 2020, MaxSAT Evaluation 2020 13
Kuhn, D.R., Wallace, D.R., Gallo, A.M.: Software fault interactions and implications for software testing. IEEE Trans. Softw. Eng. 30(6), 418–421 (2004)
Le Berre, D., Parrain, A.: The Sat4j library, release 2.2, Journal on Satisfiability, Boolean Modeling and Computation 7 (2-3), 59–64, (2010) publisher: IOS Press
Lei, Z., Cai, S.: Solving (weighted) partial maxsat by dynamic local search for sat. In: Proceedings of the Twenty-Seventh International Joint Conference on Artificial Intelligence, IJCAI-18, International Joint Conferences on Artificial Intelligence Organization, pp. 1346–1352 (2018)
Logic and Optimization Group, Pypblib, https://pypi.org/project/pypblib/, University of Lleida (2019)
Maltais, E., Moura, L.: Finding the best CAFE is np-hard. In: Proceedings of the 9th Latin American Symposium on LATIN 2010: Theoretical Informatics, Oaxaca, Mexico, April 19-23, 2010. , pp. 356–371 (2010)
Manquinho, V., Marques-Silva, J., Planes, J.: Algorithms for Weighted Boolean Optimization. In: Kullmann, O. (ed.) Theory and Applications of Satisfiability Testing - SAT 2009. Lecture Notes in Computer Science, pp. 495–508. Springer, Berlin (2009)
Morgado, A., Heras, F., Liffiton, M.H., Planes, J., Marques-Silva, J.: Iterative and core-guided maxsat solving: a survey and assessment. Constraints An Int. J. 18(4), 478–534 (2013)
Nadel, A.: Tt-open-wbo-inc-20: an anytime maxsat solver entering mse’20, MaxSAT Evaluation 2020 32
Nanba, T., Tsuchiya, T., Kikuno, T.: Using satisfiability solving for pairwise testing in the presence of constraints. IEICE Trans. Fundament. Electron. Commun. Comput. Sci. 95(9), 1501–1505 (2012)
Nanba, T., Tsuchiya, T., Kikuno, T.: Using satisfiability solving for pairwise testing in the presence of constraints. IEICE Trans. 95(9), 1501–1505 (2012)
Nie, C., Leung, H.: A survey of combinatorial testing. ACM Comput. Surv. (CSUR) 43(2), 1–29 (2011)
Rossi, F., van Beek, P., Walsh, T.: (Eds.), Handbook of Constraint Programming, Elsevier (2006)
Segall, I., Tzoref-Brill, R., Farchi, E.: Using binary decision diagrams for combinatorial test design. In: Proceedings of the 2011 International Symposium on Software Testing and Analysis, Association for Computing Machinery, New York, NY, USA, pp. 254–264 (2011)
Tseitin, G.S.: On the Complexity of Derivation in Propositional Calculus, pp. 466–483. Springer, Berlin (1983)
Yamada, A., Biere, A., Artho, C., Kitamura, T., Choi, E.-H.: Greedy combinatorial test case generation using unsatisfiable cores. In: Proceedings of the 31st IEEE/ACM International Conference on Automated Software Engineering, ASE 2016, Association for Computing Machinery, New York, NY, USA, pp. 614–624 (2016)
Yamada, A., Kitamura, T., Artho, C., Choi, E., Oiwa, Y., Biere, A.: Optimization of combinatorial testing by incremental SAT solving. In: 8th IEEE International Conference on Software Testing, Verification and Validation, ICST 2015, Graz, Austria, April 13-17, 2015, pp. 1–10 (2015)
Yu, L., Duan, F., Lei, Y., Kacker, R. N., Kuhn, D. R.: Constraint handling in combinatorial test generation using forbidden tuples. In: 2015 IEEE Eighth International Conference on Software Testing, Verification and Validation Workshops (ICSTW), pp. 1–9 (2015)