Flattening or not of the combinatorial interaction testing models?

Combinatorial Interaction Testing (CIT) requires the use of models that represent the interactions between the features of the system under test. In most cases, CIT models involve Boolean or integer options and constraints among them. Thus, applying CIT requires solving the involved constraints, which can be directly performed using Satisfiability Modulo Theory (SMT) solvers. An alternative practice is to flatten the CIT model into a Boolean model and use Satisfiability (SAT) solvers. However, the flattening process artificially increases the size of the employed models, raising the question of whether it is profitable or not in the CIT context. This paper investigates this question and demonstrates that flattened models, despite being much larger, are processed faster with SAT solvers than the smaller original ones with SMT solvers. These results suggests that flattening is worthwhile in the CIT context.