Abstract
In the context of automatic test generation, the use of propositional satisfiability (SAT) and Satisfiability Modulo Theories
(SMT) solvers is becoming an attractive alternative to traditional algorithmic test generation methods, especially when testing
Boolean expressions. The main advantages are the capability to deal with constraints over the inputs, the generation of compact
test suites and the support for fault-detecting test generation methods. However, these solvers normally require more time
and a greater amount of memory than classical test generation algorithms, making their applicability not always feasible in
practice. In this paper, we propose several ways to optimize the SAT/SMT-based process of test generation for Boolean expressions
and we compare several solving tools and propositional transformation rules. These optimizations promise to make SAT/SMT-based
techniques as efficient as standard methods for testing purposes, especially when dealing with Boolean expressions, as proved
by our experiments.
[download the pdf file] [DOI] [url]