Backtracking Search - Automatic Generation of Combinatorial Test Data - page 61

excluding some isomorphic solutions while leaving at least one solution in each
symmetric equivalence class. The other is to break symmetry dynamically during
search, adapting the search procedure appropriately. The static approach is easy to
understand and implement. In particular, it is very cost-effective for matrix models.
The symmetry breaking techniques discussed in this chapter are basically classified
as the static approach.
6.1.4 Constraint Solving Tools
Many tools have been developed for solving constraints. They are called constraint
solvers or constraint programming systems. For instance,
• GeCode ( http://www.gecode.org/ ) is a toolkit for developing constraint-based
systems and applications. It can also be used as a library.
• Minion ( http://minion.sourceforge.net/ ) is a fast scalable constraint solver.
• Choco ( http://www.emn.fr/z-info/choco-solver/ ) is a library for constraint solv-
ing and constraint programming, implemented in Java.
All of them are open source.
There are many efficient SAT solvers available today, e.g., MiniSat
( http://www.minisat.se/ ) . For more information about SAT solving and related tools,
see for example, http://www.satlive.org/ and http://www.satisfiability.org/ .
6.2 Constraint Solving and the Generation of Covering Arrays
In the previous chapters, we have seen that, to deal with constraints in combinatorial
testing, we need to perform some kind of constraint solving or SAT solving. Such
techniques have been integrated into the algorithms IPOG-C and AETG-SAT. When
implementing AETG-SAT, Cohen et al. [ 1 ] used the tool MiniSat . The ACTS tool,
which implements IPOG-C [ 11 ], uses the Choco library.
In addition, we may transform the whole problem of generating covering arrays
into a constraint satisfaction problem (CSP) or SAT. Hnich et al. [ 3 ] developed sev-
eral constraint programming models of the problem. They exploit such techniques as
global constraints and symmetry-breaking constraints. In particular, they use com-
pound variables to represent tuples of variables, which allows better propagation.
Improved bounds were obtained using this approach, with the help of ILOG Solver
6.0.
Hnich et al. [ 3 ] also experimented with the SAT-encoding of the CA generation
problem. They used a SAT solver that is based on local search. They noted that this
approach is able to find improved bounds for larger problem instances, and the best
model for local search is not necessarily the best model for backtrack search.