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

∨ ∨¬ ∨

OR) of one or more literals. The following are two clauses: x z .A

boolean expression/formula is said to be in Conjunctive Normal Form (CNF), if it is
the conjunction (logical AND) of clauses. Here is an example:

y , x y

( x ∨¬ y ) ∧ ( ¬ x ∨ y )

SAT is the first known NP-complete problem. Despite its theoretical hardness,
efficient algorithms have been developed for solving SAT.

6.1.1 Backtracking Algorithms for Solving CSPs

Backtracking is the fundamental complete search methodology for solving CSPs of
finite domains. It is a refinement of the brute force approach, systematically searching
for a solution among all possibilities.
The basic procedure of backtracking is to gradually extend a partial solution
by choosing values for variables until all constraints are satisfied, in which case a
solution is found, or until all possibilities are exhausted. If the current partial solution
cannot be consistently extended, backtracking is needed-the last choice is cancelled
and a new choice is tried.
During the search, a partial solution looks like this: . To extend

the partial solution, we select a variable which does not have a value yet, say x 6 .
Then we choose a value for it, e.g., let x 6 =

x 1 = 4 , x 3 = 2

8. If this assignment does not result in
any inconsistency, we take it, get a new partial solution which has 3 assignments; and
then we try to extend it further. On the other hand, if no good value can be assigned
to x 6 , we need to backtrack, and make a different choice (assigning a different value
to x 3 ). Then we get a different partial solution, e.g., .

Unlike brute force, which simply enumerates and tests all candidate solutions,
backtracking checks if any constraint is violated each time a variable is assigned, so
that some candidate solutions can be abandoned at an earlier stage. The backtracking
search process is often represented as a search tree, where each branch corresponds
to a choice (i.e., variable assignment), and each path represents a candidate partial
solution.

x 1 = 4 , x 3 = 6

6.1.2 Constraint Propagation

When solving a CSP via backtracking search, exploring the whole space of variable
instantiations is too expensive. Constraint propagation is an important technique to
reduce the number of candidate values for variables by detecting local inconsistency.
As a result, some branches with no solution in the search tree can be pruned earlier,
making the problem easier to solve.