Greedy combinatorial test case generation using unsatisfiable cores
Sprache des Titels:
Proc. 31st IEEE/ACM Intl. Conf. on Automated Software Engineering (ASE'16),
Combinatorial testing aims at covering the interactions of
parameters in a system under test, while some combinations
may be forbidden by given constraints (forbidden tuples).
In this paper, we illustrate that such forbidden tuples correspond
to unsatisfiable cores, a widely understood notion in
the SAT solving community. Based on this observation, we
propose a technique to detect forbidden tuples lazily during
a greedy test case generation, which significantly reduces
the number of required SAT solving calls. We further reduce
the amount of time spent in SAT solving by essentially
ignoring constraints while constructing each test case, but
then \amending" it to obtain a test case that satisfies the
constraints, again using unsatisfiable cores. Finally, to complement
a disturbance due to ignoring constraints, we implement
an efficient approximative SAT checking function
in the SAT solver Lingeling.
Through experiments we verify that our approach significantly improves the efficiency of constraint handling in our
greedy combinatorial testing algorithm.