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

Chapter 6
Backtracking Search

Abstract This chapter describes how to use backtracking search to find covering
arrays and orthogonal arrays. The basic algorithms are presented, as well as various
heuristics which improve the efficiency of the search. Different from the approaches
described in the previous chapters, backtracking search is able to find the smallest
test suite.

6.1 Constraint Satisfaction Problems

Constraint satisfaction, in its basic form, involves finding a value for each one of a
set of variables so that all of the given constraints are satisfied. The formal definition
of a Constraint Satisfaction Problem (CSP) is as follows:

Definition 6.1 A constraint satisfaction problem P is a triple P = X , D , C ,

where X is an n -tuple of variables X = x 1 , x 2 ,..., x n , D is an n -tuple of domains

.
Each variable x i may take a value from the corresponding D i . Each constraint C j
involves some subset of the variables and specifies the allowable combinations of
values for that subset.

D = D 1 , D 2 ,..., D n , C is a collection of constraints C = C 1 , C 2 ,..., C m

To solve a CSP, we need to find a value v i ∈ D i for each variable x i , such that all

the constraints in C hold.
CSP is a general framework for many specific problems. For example, the graph
(vertex) coloring problem can be regarded as a CSP. Here the variables are the colors
of the vertices; and for each pair of adjacent vertices, we have a constraint of the
form x i x j .Here x i and x j correspond to the colors of the two vertices.

For more information about CSPs, the reader may refer to the handbook [ 7 ].
An important special case of CSP is the Boolean/propositional satisfiability prob-
lem (SAT): Given a Boolean formula F

=

, determine if it is satisfiable.
If yes, return the values of variables which make F true.
A Boolean formula is commonly formulated in Conjunctive Normal Form (CNF).
Now we briefly describe the meaning of CNF. A literal is a Boolean variable or its
negation. For instance, x ,

( x 1 , x 2 ,..., x n )

¬ y are two literals. A clause is the disjunction (logical