%
% Use:
%	strongly k-consistent
%	strong k-consistency
%	locally consistent
%	local consistency
%	conflict sets
%
\documentclass[11pt]{article}
\usepackage{jair}
\usepackage{theapa}
\usepackage{epsfig}
\usepackage{psfig}
\usepackage{theorem}
\usepackage{dcolumn}

\jairheading{14}{2001}{53-81}{8/00}{3/01}
\ShortHeadings{Conflict-Directed Backjumping Revisited}
	      {Chen \& van Beek}
\firstpageno{53}

\title{
	Conflict-Directed Backjumping Revisited
}
\author{\name Xinguang Chen
	\email xinguang@cs.ualberta.ca \\
	\addr Department of Computing Science, University of Alberta\\
	Edmonton, Alberta, Canada  T6G 2H1
	\AND
	\name Peter van Beek
	\email vanbeek@uwaterloo.ca \\
	\addr Department of Computer Science, University of Waterloo\\
	Waterloo, Ontario, Canada  N2L 3G1
}
\theoremstyle{plain} \newtheorem{definition}{Definition}
\theoremstyle{plain} \newtheorem{theorem}{Theorem}
\theoremstyle{plain} \newtheorem{lemma}[theorem]{Lemma}
\theoremstyle{plain} \newtheorem{proposition}[theorem]{Proposition}
\theoremstyle{plain} \newtheorem{observation}{Observation}
\theoremstyle{plain} \newtheorem{corollary}[theorem]{Corollary}
\theoremstyle{plain} \newtheorem{remark}{Remark}
\theoremstyle{plain} \newtheorem{example}{Example}
\newenvironment{proof}[1][Proof]{\begin{trivlist}
\item[\hskip \labelsep {\bfseries #1}]}{\end{trivlist}}
\newcommand{\qed}{\nobreak \ifvmode \relax \else
           \ifdim\lastskip<1.5em \hskip-\lastskip
           \hskip1.5em plus0em minus0.5em \fi \nobreak
           \vrule height0.75em width0.5em depth0.25em\fi}
\newcommand{\dash}{.}
\date{}
\begin{document}
\maketitle


\begin{abstract}
In recent years, many improvements to backtracking algorithms
for solving constraint satisfaction problems have been proposed.
The techniques for improving backtracking algorithms can
be conveniently classified as \emph{look-ahead} schemes
and \emph{look-back} schemes.
Unfortunately, look-ahead and look-back schemes are not
entirely orthogonal as it has been observed empirically
that the enhancement of look-ahead techniques is sometimes
counterproductive to the effects of look-back techniques. In
this paper, we focus on the relationship between the two most
important look-ahead techniques---using a variable ordering
heuristic and maintaining a level of local consistency
during the backtracking search---and the look-back technique of
conflict-directed backjumping (CBJ). We show that there exists
a ``perfect'' dynamic variable ordering such that CBJ becomes
redundant. We also show theoretically that as the level of local
consistency that is maintained in the backtracking search is
increased, the less that backjumping will be an improvement.
Our theoretical results partially explain why a backtracking
algorithm doing more in the look-ahead phase cannot benefit
more from the backjumping look-back scheme. Finally, we show
empirically that adding CBJ to a backtracking algorithm that
maintains generalized arc consistency (GAC), an algorithm that
we refer to as GAC-CBJ, can still provide orders of magnitude
speedups. Our empirical results contrast with Bessi\`ere and
R\'egin's conclusion (1996) that CBJ is useless to an algorithm
that maintains arc consistency.
\end{abstract}

\section{Introduction}

Constraint satisfaction problems (CSPs) are a generic problem
solving framework. A constraint satisfaction problem consists
of a set of variables, each associated with a domain of values,
and a set of constraints. Each of the constraints is expressed
as a relation, defined on some subset of the variables, denoting
the consistent value assignments that satisfy the constraint. A
solution to a CSP is an assignment of a value to every variable,
in such a way that every constraint is satisfied.

Constraint satisfaction problems are usually solved by
search methods, among which the backtracking algorithm
and its improvements are widely used. The techniques
for improving backtracking algorithms can be conveniently
classified as \emph{look-ahead schemes} and \emph{look-back
schemes} \cite{Dechter92survey}. Look-ahead schemes are
invoked whenever the algorithm is preparing to extend the
current partial solution. Look-ahead schemes include the
functions that choose the next variable to be instantiated,
choose the next value to give to the current variable,
and reduce the search space by maintaining a certain
level of local consistency during the search (e.g.,
\citeR{BavR95,BeRe96,HaEl80,McGregor79,Nadel89,SaFr94}).
Look-back schemes are invoked whenever the algorithm encounters
a dead-end and prepares for the backtracking step. Look-back
schemes include the functions that decide how far to backtrack
by analyzing the reasons for the dead-end (backjumping)
and decide what new constraints to record so that the same
conflicts do not arise again later in the search (e.g.,
\citeR{Bruynooghe81,Dechter90,FrDe94b,Gaschnig78,Prosser93,ScVe94}).

A backtracking algorithm can be a hybrid of both look-ahead
and look-back schemes \cite{Prosser93}. In this paper, we focus
on the relationship between the two most important look-ahead
techniques---using a variable ordering heuristic and maintaining
a level of local consistency during the backtracking search---and
the look-back technique of conflict-directed backjumping (CBJ)
\cite{Prosser93}. Unfortunately, these look-ahead and look-back
schemes are not entirely orthogonal as it can be observed in
previous experimental work that as the level of consistency
that is maintained in the backtracking search is increased and
as the variable ordering heuristic is improved, the effects of
CBJ are diminished \cite{BavR95,BeRe96,Prosser93a,Prosser93}.
For example, it can be observed in Prosser's \citeyear{Prosser93}
experiments that, given a static variable ordering, increasing
the level of local consistency maintained from none to the
level of forward checking, diminishes the effects of CBJ.
Bacchus and van Run \citeyear{BavR95} observe from their experiments
that adding a dynamic variable ordering (an improvement over
a static variable ordering) to a forward checking algorithm
diminishes the effects of CBJ. In their experiments the effects
are so diminished as to be almost negligible and they present
an argument for why this might hold in general. Bessi\`ere
and R\'egin \citeyear{BeRe96} observe from their experiments that
simultaneously increasing the level of local consistency
even further to arc consistency and further improving the
dynamic variable ordering heuristic diminishes the effects
of CBJ so much that, in their implementation, the overhead of
maintaining the data structures for backjumping actually slows
down the algorithm. They conjecture that when arc consistency
is maintained and a good variable ordering heuristic is used,
``CBJ becomes useless''.

In this paper, we present theoretical results that deepen our
understanding of the relationship between look-ahead techniques
and the CBJ look-back technique. We show that there exists a
``perfect'' dynamic variable ordering for the chronological
backtracking algorithm such that CBJ becomes redundant. The
more that a variable ordering heuristic is consistent with the
``perfect'' heuristic, the less chance CBJ has to reduce the
search effort. We also show that CBJ and an algorithm that
maintains strong $k$-consistency in the backtracking search
are incomparable in that each can be exponentially better than
the other. This result is refined by introducing the concept
of \emph{backjump level} in the execution of a backjumping
algorithm and showing that an algorithm that maintains strong
$k$-consistency never visits more nodes than a backjumping
algorithm that is allowed to backjump at most $k$ levels. Thus,
as the level of local consistency that is maintained in the
backtracking search is increased, the less that backjumping
will be an improvement. Together, our theoretical results
partially explain why a backtracking algorithm doing more in
the look-ahead phase cannot benefit more from the backjumping
look-back scheme. Our results also extend the partial ordering
of backtracking algorithms presented by Kondrak and van Beek
\citeyear{KovB97} to include backtracking algorithms and their
CBJ hybrids that maintain levels of local consistency beyond
forward checking, including the important algorithms that
maintain arc consistency.

We also present empirical results that show that, although the
effects of CBJ may be diminished, adding CBJ to a backtracking
algorithm that maintains generalized arc consistency (GAC),
an algorithm that we refer to as GAC-CBJ, can still provide
orders of magnitude speedups. Our empirical results contrast
with Bessi\`ere and R\'egin's \citeyear{BeRe96} conclusion that
CBJ is useless to an algorithm that maintains arc consistency.

\section{Background}

In this section, we formally define constraint satisfaction
problems, and briefly review local consistency and the search
tree explored by a backtracking algorithm.

\subsection{Constraint Satisfaction Problems}

\begin{definition}[CSP]
An instance of a constraint satisfaction problem is a
tuple $P = (\mathcal{V}, \mathcal{D}, \mathcal{C})$,
where\footnote{Throughout the paper, we use $n$, $d$, $m$, and $r$ to
denote the number of variables, the maximum domain size, the
number of constraints, and the maximum arity of the
constraints in the CSP, respectively. }
\begin{itemize}
\item $\mathcal{V}$ = $\{x_{1}, \ldots, x_{n}\}$ is a finite set of $n$
variables,
\item $\mathcal{D}$ = $\{dom(x_{1}), \ldots, dom(x_{n})\}$ is a set of
domains. Each variable $x \in \mathcal{V}$ is associated with a
finite domain of
possible values, $dom(x)$. The maximum domain size $max_{x \in
\mathcal{V}}|dom(x)|$
is denoted by $d$,
\item $\mathcal{C}$ = $\{C_{1}, \ldots,C_{m}\}$ is a finite set of $m$
constraints or relations. Each constraint $C \in \mathcal{C}$ is a pair
$(vars(C), rel(C))$, where
\begin{itemize}
\item $vars(C) = \{x_{i_{1}}, \ldots, x_{i_{r_{i}}}\}$ is an ordered
subset of the variables, called the constraint scope or
scheme, the size of $vars(C)$ is known as the arity of the
constraint. If the arity of the constraint is equal to 2, it
is called a binary constraint. A \emph{non-binary} constraint
is a constraint with arity greater than 2. The maximum arity
of the constraints in $\mathcal{C}$, $max_{C \in \mathcal C
}|vars(C)|$, is denoted by $r$, \item $rel(C)$ is a subset of
the Cartesian product $dom(x_{i_{1}}) \times \cdots \times
dom(x_{i_{r_{i}}})$ that specifies the allowed combinations
of values for the variables in $vars(C)$. An element of
the Cartesian product $dom(x_{i_{1}}) \times \cdots \times
dom(x_{i_{r_{i}}})$ is called a tuple on $vars(C)$. Thus,
$rel(C)$ is often regarded as a set of tuples over $vars(C)$.
\end{itemize}
\end{itemize}
\label{DEFN:csp}
\end{definition}

In the following, we assume that for any variable $x \in
\mathcal{V}$, there is at least one constraint $C \in
\mathcal{C}$ such that $x \in vars(C)$. By definition, a
tuple over a set of variables $X = \{x_{1}, \ldots, x_{k}\}$
is an ordered list of values $(a_{1}, \ldots, a_{k})$ such
that $a_{i} \in dom(x_{i})$, $i = 1, \ldots, k$. A tuple over
$X$ can also be regarded as a set of variable-value pairs
$\{ x_{1}\leftarrow a_{1}, \ldots, x_{k}\leftarrow a_{k}
\}$. Furthermore, a tuple over $X$ can be viewed as a function
$t : X \rightarrow \cup_{x \in X} dom(x)$ such that for each
variable $x \in X$, $t[x] \in dom(x)$. For a subset of variables
$X' \subseteq X$, we use $t[X']$ to denote a tuple over $X'$
by restricting $t$ over $X'$. We also use $vars(t)$ to denote
the set of variables for tuple $t$.

An \emph{assignment} to a set of variables $X$ is a tuple
over $X$. We say an assignment $t$ to $X$ is \emph{consistent}
with a constraint $C$ if either $vars(C) \not\subseteq X$ or
$t[vars(C)] \in rel(C)$. A \emph{partial solution} to a CSP
is an assignment to a subset of variables. We say a partial
solution is \emph{consistent} if it is consistent with each
of the constraints. A \emph{solution} to a CSP is a consistent
partial solution over all the variables. If no solution exists,
the CSP is said to be insoluble. A CSP is \emph{empty} if
either one of its variables has an empty domain or one of its
constraints has an empty set of tuples. Obviously, an empty
CSP is insoluble.
Given two CSP instances $P_{1}$ and $P_{2}$, we say $P_{1} =
P_{2}$ if they have exactly the same set of variables, the same
set of domains and the same set of constraints; i.e.,
they are syntactically the same.

\begin{definition}[projection]
Given a constraint $C$ and a subset of variables $S \subseteq vars(C)$, the
projection $\pi_{S}C$ is a constraint, where $vars(\pi_{S}C) = S$ and
$rel(\pi_{S}C) = \{ t[S] \mid t \in rel(C)\}$.
\label{DEFN:projection}
\end{definition}

\begin{definition}[selection]
Given a constraint $C$ and an assignment $t$ to a subset of variables $X
\subseteq vars(C)$, the selection $\sigma_{t}C$ is a constraint, where
$vars(\sigma_{t}C) = vars(C)$ and $rel(\sigma_{t}C) = \{ s \mid s[X] = t
\mbox{ and } s \in rel(C)\}$.
\label{DEFN:selection}
\end{definition}

\subsection{Local Consistency}

An \emph{inconsistency} is a consistent partial solution over
some of the variables that cannot be extended to additional
variables and so cannot be part of any global solution. If we
are using a backtracking search to find a solution, such an
inconsistency can lead to a dead end in the search. This insight
has led to the definition of properties that characterize
the level of consistency of a CSP and to the development of
algorithms for achieving these levels of consistency by removing
inconsistencies (e.g., \citeR{Mackworth77,Montanari74}), and
to effective backtracking algorithms for finding solutions to
CSPs that maintain a level of consistency during the search
(e.g., \citeR{Gaschnig78,HaEl80,McGregor79,SaFr94}).

Mackworth \citeyear{Mackworth77} defines three properties of
binary CSPs that characterize local consistencies: node,
arc, and path consistency. Mackworth \citeyear{Mackworth77IJCAI}
generalizes arc consistency to non-binary CSPs.

\begin{definition}[arc consistency]
Given a constraint $C$ and a variable $x \in vars(C)$, a value $a \in dom(x)$
is \emph{supported} in $C$ if there is a tuple $t \in rel(C)$,
such that $t[x] = a$. $t$ is then called a \emph{support}
for $\{x\leftarrow a\}$ in $C$. C is \emph{arc consistent} if
for each of the variables $x \in vars(C)$, and each of the
values $a \in dom(x)$, $\{x\leftarrow a\}$ is supported in $C$.
A CSP is \emph{arc consistent} if each of its constraints is
arc consistent.
\label{DEFN:AC}
\end{definition}

\noindent
Freuder \citeyear{Freuder78} generalizes node, arc,
and path consistency, to $k$-consistency.

\begin{definition}[$k$-consistency]
A CSP is $k$-consistent if and only if given any consistent partial
solution over $k-1$ distinct variables, there exists an instantiation
of any $k^{th}$ variable such that the partial solution plus that
instantiation is consistent. A CSP is strongly $k$-consistent if
it is $j$-consistent for all $1 \leq j \leq k$.
\label{DEFN:KC}
\end{definition}

For binary CSPs, node, arc and path consistency correspond to
one-, two- and three-consistency, respectively. However, the
definition of $k$-consistency does not require the CSP to be
binary and arc consistency is not the same as two-consistency
for non-binary CSPs. A strongly $n$-consistent CSP has
the property that any consistent partial solution can be
successively extended to a full solution of the CSP without
backtracking.

\subsection{Search Tree and Backtracking Algorithms}

The idea of a \emph{backtracking algorithm} is to extend
partial solutions. At each stage, an uninstantiated variable
is selected and assigned a value from its domain to extend
the current partial solution\footnote{Throughout this paper,
we assume that a static \emph{value}
ordering is used in the backtracking search.}.
Constraints are used to check
whether such an extension may lead to a possible solution
of the CSP and to prune subtrees containing no solutions
based on the current partial solution. During a backtracking
search, the variables can be divided into three sets: \emph{past
variables} (already instantiated), \emph{current variable}
(now being instantiated), and \emph{future variables}
(not yet instantiated). A \emph{dead-end} occurs when all
values of the current variable are rejected as not leading
to a full solution. In such a case, some instantiated
variables become \emph{uninstantiated}; i.e., they
are removed from the current partial solution. This process
is called \emph{backtracking}. If only the most recently
instantiated variable becomes uninstantiated then it is called
\emph{chronological backtracking}; otherwise, it is called
\emph{backjumping}. A backtracking algorithm terminates when
all possible assignments have been tested or a certain number
of solutions have been found.

A backtracking search may be seen as a \emph{search tree}
traversal. In this approach we identify tuples (assignments of
values to variables) with nodes: the empty tuple is the root of
the tree, the first level nodes are 1-tuples (representing an
assignment of a value to a single variable), the second level
nodes are 2-tuples, and so on. The levels closer to the root
are called \emph{shallower levels} and the levels farther from the
root are called \emph{deeper levels}. Similarly, the variables
corresponding to these levels are called shallower and deeper.
We say that a backtracking algorithm visits a node in the
search tree if at some stage of the algorithm's execution the
current partial solution identifies the node. The nodes visited
by a backtracking algorithm form a subset of all the nodes
belonging to the search tree. We call this subset, together
with the connecting edges, the \emph{backtrack tree}
generated by a backtracking algorithm.

The backtracking algorithm conflict-directed backjumping
(CBJ)~\cite{Prosser93} maintains a {\em conflict set} for every
variable. Every time an instantiation of the current
variable $x_i$ is in conflict with an instantiation
of some past variable $x_h$, the variable $x_h$ is added to
the conflict set of $x_i$. When there are no more values to
be tried for the current variable $x_{i}$, CBJ backtracks to
the deepest variable $x_h$ in the conflict set of $x_{i}$. At
the same time, the variables in the conflict set of $x_{i}$,
with the exception of $x_h$, are added to the conflict set of
$x_h$, so that no information about conflicts is lost.

Throughout the paper we refer to the following backtracking
algorithms (see \citeR{KovB97,Prosser93} for detailed explanations
and examples of most of these algorithms):
chronological backtracking (BT),
backjumping (BJ)
	\cite{Gaschnig78},
conflict-directed backjumping (CBJ)
	\cite{Prosser93},
forward checking (FC)
	\cite{HaEl80,McGregor79},
forward checking and conflict-directed backjumping (FC-CBJ)
	\cite{Prosser93},
maintaining arc consistency (MAC)
	\cite{Gaschnig78,SaFr94}, and
maintaining arc consistency and conflicted-directed backjumping (MAC-CBJ)
	\cite{Prosser95}.

\section{Variable Ordering Heuristics and Backjumping}

In this section, we present theoretical results that deepen
our understanding of the relationship between the look-ahead
technique of using a variable ordering heuristic and the
look-back technique of CBJ.

In previous work, Kondrak and van Beek \citeyear{KovB97} show
that, given the same deterministic static or dynamic
variable ordering heuristic, CBJ never visits more nodes
than BT. Bacchus and van Run \citeyear{BavR95} show that BJ,
a restricted version of CBJ, visits exactly the same nodes
as BT if the fail-first dynamic variable ordering heuristic
is used. Previous empirical work shows that the number of
nodes that CBJ saves depends on the variable ordering heuristic
used \cite{BavR95,BeRe96,Prosser93}.

We show that, given a CSP and a variable ordering for CBJ, there
exists a ``perfect'' variable ordering for the chronological
backtracking algorithm (BT) such that BT never visits more
nodes than CBJ. The more that a variable ordering heuristic
is consistent with the ``perfect'' heuristic, the less chance
CBJ has to reduce the search effort.

We first consider the case of insoluble CSPs. When CBJ is
applied to an insoluble CSP, it always backjumps from a dead-end
state; i.e., it does not terminate or backjump from a
situation in which a solution of the CSP was found.

\begin{lemma}
Given an insoluble CSP and a variable ordering for CBJ, there
exists a variable ordering for BT such that BT never visits
more nodes than CBJ to show that no solution exists.
\label{Lemma:CBJ<BT:Insoluble}
\end{lemma}
\begin{proof}
In the backtrack tree generated by CBJ under the variable
ordering, let the last backjump that terminates the execution
of CBJ be from variable $x_{j}$ to the root of the backtrack
tree. We choose $x_{j}$ to be the first variable for BT. For
each value $a$ in the domain of $x_{j}$, if the current node
in the backtrack tree for CBJ is {\em consistent} (not a leaf
node), the next variable chosen to be instantiated after
assigning $a$ to $x_{j}$ is the variable that backjumps to
$x_{j}$ and causes the assignment $x_{j}\leftarrow a$ to be
revoked. The entire variable ordering for BT can be worked
out in a similar, recursive manner.
For this variable ordering for BT to be well-defined, it remains
to show that if the current node in the backtrack tree for CBJ
is inconsistent (a leaf node), the corresponding node in the
backtrack tree for BT is also inconsistent (and therefore no
next variable needs to be chosen). We show that the variables
skipped in the variable ordering constructed for BT are
irrelevant to the dead-end states encountered by CBJ. Suppose
at a stage we have ordered the variables to be instantiated
for BT as $x_{j_{1}}, \ldots, x_{j_{k}}$, and for value $a \in
dom(x_{j_{k}})$ we choose the next variable $x_{j_{k+1}}$ as the
variable which backjumps to the current variable $x_{j_{k}}$
in the CBJ backtrack tree. We prove by induction that
the conflict set of $x_{j_{k+1}}$ used in the backjumping
is subsumed by $\{x_{j_{1}}, \ldots, x_{j_{k}}\}$. $k=1$ is
the case of the last backjump that terminates the execution
of CBJ. The hypothesis is true because the conflict set of
$x_{j_{1}}$ is an empty set. Suppose it is true for the case
of $k > 1$. Because $x_{j_{k+1}}$ backjumps to $x_{j_{k}}$, the
conflict set of $x_{j_{k+1}}$ is merged in the conflict set
of $x_{j_{k}}$. From the inductive assumption, the conflict
set of $x_{j_{k}}$ is subsumed by $\{x_{j_{1}}, \ldots,
x_{j_{k-1}}\}$, and thus the conflict set of $x_{j_{k+1}}$
is subsumed by $\{x_{j_{1}}, \ldots, x_{j_{k}}\}$. Therefore,
the hypothesis holds for the case of $k+1$. If CBJ finds out
that instantiation $x_{j_{k}}\leftarrow a$ is inconsistent
with the assignments of some past variables which are added
to the conflict set of $x_{j_{k}}$, BT is also able to find
out the inconsistency because the conflict set of $x_{j_{k}}$
is subsumed by $\{x_{j_{1}},\ldots, x_{j_{k-1}}\}$. Thus, the
variable ordering for BT is well-defined.
\qed
\end{proof}

For soluble CSPs, we further distinguish the problem between
finding one solution and finding all solutions.

\begin{lemma}
Given a CSP and a variable ordering for CBJ to find the first
solution, there exists a variable ordering for BT such that
BT never visits more nodes than CBJ to find the first solution.
\label{Lemma:CBJ<BT:Find-One-Solution}
\end{lemma}
\begin{proof}
Without loss of generality, let $\{x_{1}\leftarrow a_{1},
\ldots, x_{n}\leftarrow a_{n}\}$ be the first solution found.
A variable ordering for BT can be constructed in the following
way. The first variable chosen for BT is $x_{1}$ as it is the
first variable in the path from the root to the solution in the
CBJ backtrack tree. Because we assume a static value ordering
in the backtracking search, all values in the domain of $x_{1}$
that precede value $a_{1}$ must be rejected by CBJ and BT before
value $a_{1}$ is used to instantiate $x_{1}$. Furthermore,
because $\{x_{1}\leftarrow a_{1}, \ldots, x_{n}\leftarrow
a_{n}\}$ is the first solution encountered by CBJ under the
above variable ordering and value ordering, the instantiation
of $x_{1}$ with a value preceding $a_{1}$ leads to an insoluble
subproblem and eventually CBJ backjumps from a deeper
variable to $x_{1}$ to revoke that assignment. Note that
$x_{1}$ cannot be skipped by a backjump from a deeper
variable because $x_{1}$ is on the first level of the search
tree and there is a solution for the CSP.
Assigning $x_{1}$ with each of the values that precede
$a_{1}$ in its domain leads to insoluble subproblems and the
instantiation order for BT can be arranged as in
Lemma~\ref{Lemma:CBJ<BT:Insoluble}.
Whenever $x_{k}$ is instantiated with value
$a_{k}$, $x_{k+1}$ is chosen to be the next variable, as it
follows $x_{k}$ in the path from the root to the solution in the
CBJ backtrack tree. Again, all values in the domain of $x_{k+1}$
that precede $a_{k+1}$ in the value ordering must be rejected
by CBJ and BT before $a_{k+1}$ is assigned to $x_{k+1}$. The
instantiation of $x_{k+1}$ with each of these values leads
to an insoluble subproblem and eventually CBJ backjumps from
a deeper variable to $x_{k+1}$. Similarly, $x_{k+1}$
cannot be skipped by a backjump from a deeper variable
because otherwise at least one of the assignments to $x_{1},
\ldots, x_{k}$ must be changed so that $\{x_{1}\leftarrow
a_{1}, \ldots, x_{n}\leftarrow a_{n}\}$ is not the first
solution encountered by CBJ. In each of these insoluble
subproblems, the instantiation order for BT can be arranged
as in Lemma~\ref{Lemma:CBJ<BT:Insoluble}. Finally, $x_{n}$
is instantiated with $a_{n}$ and BT finds the solution. \qed
\end{proof}

When CBJ is used to find all solutions, special steps must
be taken to handle the conflict sets. The problem here is
that the conflict sets of CBJ are meant to indicate which
instantiations are responsible for some previously discovered
inconsistency. However, after a solution is found, conflict
sets cannot always be interpreted in this way. It is the search
for other solutions, rather than an inconsistency, that causes
the algorithm to backtrack. We need to differentiate between
two causes of CBJ backtracks: (1) detecting an inconsistency,
and (2) searching for other solutions. In the latter case,
the backtrack must be always chronological; that is, to
the immediately preceding variable. A simple solution is to
remember the number of solutions found so far when a variable
is chosen to be instantiated, and later when a dead-end state
is encountered at this level, we compare the recorded number
with the current number of solutions. A difference indicates
that some solutions have been found in this interval of search,
and forces the algorithm to backtrack chronologically. Otherwise
the algorithm performs a normal backjumping by analyzing the
conflict set of the current variable.

\begin{lemma}
Given a CSP and a variable ordering for CBJ to find
all solutions, there exists a variable ordering for BT such
that BT never visits more nodes than CBJ to find all solutions.
\label{Lemma:CBJ<BT:Find-All-Solution}
\end{lemma}

\begin{proof}
Let the first solution found by CBJ be $\{x_{1}\leftarrow a_{1},
\ldots, x_{n}\leftarrow a_{n}\}$ in the order of $x_{1},
\ldots, x_{n}$. We first construct the variable ordering
for BT as it is applied to find the first solution. However,
because BT follows a strict chronological backtracking, it
will inevitably visit all the nodes $\{x_{1}\leftarrow a_{1},
\ldots, x_{j-1}\leftarrow a_{j-1}, x_{j}\leftarrow a'_{j}\}$,
where $1 \leq j \leq n$ and $a'_{j}$ comes after $a_{j}$ in the
domain of $x_{j}$. If CBJ skips any of these nodes, for example,
from a deeper level variable $x_{h}$ to $x_{j-1}$, while  the
instantiations of $x_{1}, \ldots, x_{j}$ have not been changed,
BT will possibly visit more nodes than CBJ. We will show
this cannot happen by induction on the distance between the
current level $j$ and the deepest level $n$. After CBJ has
found the solution at level $n$, it will try other values for
$x_{n}$ and eventually backtrack to $x_{n-1}$. So the nodes at
level $n$ cannot be skipped. Suppose it is true for the case of
level $j+1$ and now we consider the case of level $j$. Because
$x_{j}\leftarrow a_{j}$ was not skipped in the backjumping, if
$a_{j}$ is the last value in its domain, CBJ will backtrack to
$x_{j-1}$ because the number of solutions has been changed. So
it is true for the case of $j$. Otherwise CBJ will change the
instantiation of $x_{j}$ to the next value in its domain. Let
the current partial solution be $t =\{x_{1}\leftarrow a_{1},
\ldots, x_{j-1}\leftarrow a_{j-1}, x_{j}\leftarrow a'_{j}\}$. If
the subtree rooted by $t$ contains solutions, from the inductive
hypothesis, CBJ will not skip this node because it is on
level $j$. If the subtree rooted by $t$ contains no solution,
there exists a backjump from a deeper level variable $x_{h}$
to escape this subtree. Could it jump beyond $x_{j}$ such that
$t$ is skipped? In that case, the conflict set of $x_{h}$ is
subsumed in $\{x_{1},\ldots, x_{j-1}\}$. From the definition
of conflict set, we know that the current instantiations
of the variables in the conflict set cannot lead to a
solution. However the current instantiations of $\{x_{1},\ldots,
x_{j-1}\}$ do lead to a solution, $\{x_{1}\leftarrow a_{1},
\ldots, x_{n}\leftarrow a_{n}\}$. That is a contradiction. So
the conflict set of $x_{h}$ must contain $x_{j}$ and thus
the node $t$ at level $j$ cannot be skipped. After all the
values in the domain of $x_{j}$ have been tried, CBJ will
chronologically backtrack to $x_{j-1}$ because the number
of solutions has changed. Thus, $x_{j-1}\leftarrow a_{j-1}$
will not be skipped. The hypothesis is true for the case of
any level $j$. Then we construct the variable ordering for
BT in the following way: If the current partial solution $t
=\{x_{1}\leftarrow a_{1}, \ldots, x_{j-1}\leftarrow a_{j-1},
x_{j}\leftarrow a'_{j}\}$ cannot be extended to a solution, we
construct a variable ordering for the insoluble subproblem. If
$t$ can be extended to a solution, we construct a variable
ordering for BT as the case of finding the first solution
in this subproblem, and recursively apply the above steps
until a backjump to level $x_{j}$ changes the instantiation
$x_{j}\leftarrow a'_{j}$. Under the above variable ordering,
BT will never visit more nodes than CBJ.
\qed
\end{proof}

\begin{theorem}
Given a CSP and a variable ordering for CBJ, there exists a
variable ordering for BT such that BT never visits more nodes
than CBJ in solving the CSP.
\label{Theorem:CBJ<BT}
\end{theorem}
\begin{proof}
Follows from
Lemmas \ref{Lemma:CBJ<BT:Insoluble},
       \ref{Lemma:CBJ<BT:Find-One-Solution}, and
       \ref{Lemma:CBJ<BT:Find-All-Solution}. \qed
\end{proof}

\begin{figure}
\begin{center}
\input{figs/bt-cbj-ex.pstex_t}
\end{center}
\caption{An illustration of the variable ordering constructed for BT
from a CBJ backtrack tree (for the CSP shown upper left).}
\label{FIGURE:CBJ<BT:Example}
\end{figure}

\begin{example}
Figure \ref{FIGURE:CBJ<BT:Example} shows the BT backtrack tree based
on the variable ordering constructed from the execution of CBJ to
solve a CSP under a (hypothetical) dynamic variable ordering.
The first solution found by
CBJ is $\{x_{1}\leftarrow 0, x_{2}\leftarrow 0, x_{3}\leftarrow 2,
x_{5}\leftarrow 0, x_{4}\leftarrow 0\}$. Thus, BT first instantiates
$x_{1}$ and $x_{2}$ to 0. The node $\{x_{1}\leftarrow 0,
x_{2}\leftarrow 0, x_{3}\leftarrow 0\}$ and $\{x_{1}\leftarrow 0,
x_{2}\leftarrow 0, x_{2} \leftarrow 1\}$ in the CBJ backtrack tree
lead to insoluble subproblems. The variable ordering for BT at
each of these nodes is constructed as in the case of insoluble CSPs.
For example, in the CBJ backtrack tree, the last backjump to revoke
the node $\{x_{1}\leftarrow 0, x_{2}\leftarrow 0, x_{3}\leftarrow 0\}$
is from $x_{5}$ to $x_{3}$, so the next variable instantiated in BT at
this node is $x_{5}$. Under such an ordering, BT avoids instantiating
$x_{4}$ and visits fewer nodes than CBJ. Then BT instantiates $x_{3}$
to 2, $x_{5}$ to 0, and $x_{4}$ to 0, and finds the first solution.
\end{example}

We have shown that there exists a ``perfect'' variable ordering
such that CBJ becomes redundant. Of course, the ``perfect''
ordering would not be known \emph{a priori}, and in practice,
the primary goal in designing variable ordering heuristics
is not to simulate the execution of CBJ, but to reduce the
size of the overall backtrack tree. As an example,
the popular fail-first heuristic selects as the next variable
to be instantiated the variable with the minimal remaining
domain size (the size of the domain after removing values
that are in conflict with past instantiations) as this can be
shown to minimize the size of the overall tree under certain
assumptions. A secondary effect, however, is that variables
that have conflicts with past instantiations are likely to
be instantiated sooner, thus approximating the ``perfect''
ordering and diminishing the effects of backjumping.

\section{Maintaining Consistency and Backjumping}

In this section, we present theoretical results that deepen
our understanding of the relationship between the look-ahead
technique of maintaining a level of local consistency during
the backtracking search and the look-back technique of CBJ.

In previous work, Kondrak and van Beek \citeyear{KovB97} show that,
given the same deterministic static or dynamic variable ordering
heuristic, CBJ never visits more nodes than BT and FC-CBJ never
visits more nodes than FC. Prosser \citeyear{Prosser93a} shows
that the removal of an inconsistent value from the domain
of a variable can diminish the effects of CBJ and that CBJ
can visit fewer nodes than an algorithm that combines CBJ
with the discovery and removal of some inconsistent values.
Previous empirical work shows that the number of nodes that CBJ
saves depends on the level of local consistency maintained
\cite{BavR95,BeRe96,Prosser93}.

We extend the partial ordering of backtracking algorithms
presented by Kondrak and van Beek \citeyear{KovB97} to include
backtracking algorithms and their CBJ hybrids that maintain
levels of local consistency beyond forward checking, including
the important algorithms that maintain arc consistency. We show
that CBJ and an algorithm that maintains strong $k$-consistency
in the backtracking search are incomparable in that each can
be exponentially better than the other. This result is refined
by using the concept of \emph{backjump level} in the execution
of a backjumping algorithm and showing that an algorithm that
maintains strong $k$-consistency never visits more nodes than
a backjumping algorithm that is allowed to backjump at most
$k$ levels. Thus, as the level of local consistency that is
maintained in the backtracking search is increased, the less
that backjumping will be an improvement.

In Section~\ref{SUBSECTION:backjump-level},
we consider the backjumping algorithms and define the
series of algorithms BJ$_{k}$.
In Section~\ref{SUBSECTION:maintain-consistency},
we consider the look-ahead algorithms that maintain a level of
local consistency and define the series of algorithms MC$_{k}$.
Finally, in Section~\ref{SUBSECTION:relationship}, we
consider the relationships between the backjumping and the
look-ahead algorithms and their hybrids.
The reader who is not interested in the technical proofs of the
results should jump directly to this section.

\subsection{Backjump Level and BJ$_{k}$}
\label{SUBSECTION:backjump-level}

To analyze the influence of the level of consistency on the
backjumping, we need the notion of \emph{backjump level}.
Informally, the level of a backjump is the distance, measured
in backjumps, from the backjump destination to the ``farthest''
dead-end.

\begin{definition}[backjump level, \citeR{KovB97}]
The definition of backjump level is recursive:\\
1. A backjump from variable $x_{i}$ to variable $x_{h}$ is of
level 1 if it is performed directly from a dead-end state in
which every value of $x_{i}$ fails a consistency check. \\
2. A backjump from variable $x_{i}$ to variable $x_{h}$ is
of level $d \geq 2$, if all backjumps performed to variable
$x_{i}$ are of level less than $d$, and at least one of them
is of level $d-1$.
\label{DEFN:BJ-Level}
\end{definition}

\begin{figure}
\begin{center}
\input{figs/bj-level-tree.pstex_t}
\end{center}
\caption{An illustration of backjump levels in a CBJ backtrack tree
(for the CSP shown upper right).}
\label{FIGURE:BJ-Levels:Search-Tree}
\end{figure}

\begin{example}
Figure \ref{FIGURE:BJ-Levels:Search-Tree} shows the backjump
levels in an example CBJ backtrack tree. There is a one-level
backjump from $x_{5}$ to $x_{3}$ because every value in the
domain of $x_{5}$ fails a consistency check. Then CBJ finds
two solutions for the problem and thus it chronologically
backtracks from $x_{4}$ to $x_{5}$, and later to $x_{3}$. The
backjumps are of level one and two respectively. At last there
is a three-level backjump from $x_{3}$ to $x_{2}$.
\end{example}

By classifying the backjumps performed by a backjumping
algorithm into different levels, we can now weaken CBJ into
a series of backjumping algorithms which perform limited
levels of backjumps. BJ$_{k}$ is a backjumping algorithm
which is allowed to perform at most $k$-level backjumps and it
chronologically backtracks when a $j$-level backjump for $j > k$
is encountered\footnote{BJ$_{k}$ is only of theoretical interest
since in practice one would use CBJ rather than artificially
prevent backjumping; i.e., one has to actually add
code to prevent backjumping.}. BJ$_{n}$ is equivalent to CBJ,
which performs unlimited backjumps, and BJ$_{1}$ is equivalent
to Gaschnig's \citeyear{Gaschnig78} BJ, which only does the first
level backjumps or backjumps from dead-ends.

One may immediately conclude that BJ$_{k+1}$ is always
better than BJ$_{k}$ because it does one more level of
backjumps. However, to be more precise, we need to justify
that a situation where BJ$_{k}$ may skip a node visited by
BJ$_{k+1}$ does not exist. Similar to a result by
Kondrak and van Beek (Theorem 11, \citeyearR{KovB97}),
we can show that:
\begin{theorem}
BJ$_{k}$ visits all the nodes that BJ$_{k+1}$ visits.
\end{theorem}

\subsection{Maintaining Strong $k$-consistency (MC$_{k}$)}
\label{SUBSECTION:maintain-consistency}

Although backtracking algorithms that maintain arc consistency
(or a truncated form of arc consistency called forward checking)
during the search have been well-studied, a backtracking
algorithm that maintains strong $k$-consistency (MC$_{k}$) has
never been fully addressed in the literature. In order to
study the relationship between BJ$_{k}$ and MC$_{k}$, we need to
specify precisely the MC$_{k}$ algorithms.

A generic scheme to maintain a level of local consistency
in a backtracking search is to perform at each node in the
search tree one full cycle of consistency achievement. A
consistency achievement algorithm is applied to the CSP which is
\emph{induced} by the current partial solution. If, as a result,
the induced CSP becomes empty after applying the consistency
algorithm, the instantiation of the current variable is a
dead-end and should be rejected. If the resulting CSP is not
empty, the instantiation of the current variable is accepted
and the search continues to the next level.

The simplest form of an induced CSP is to restrict the domains
of the instantiated variables to have only one value and leave
the set of constraints unchanged. This idea can be traced back
to Gaschnig's \citeyear{Gaschnig78} implementation of MAC,
referred to as DEEB; i.e., Domain Element Elimination with
Backtracking. However, in order to establish a relation between
BJ$_{k}$ and MC$_{k}$, we need a more restricted definition
of the induced CSP, where the constraints in the induced CSP
are the selections and projections of the constraints in the
original CSP with respect to a partial solution.

\begin{definition}[induced CSP]
Given a consistent partial solution $t$ of a CSP $P$, the CSP induced by
$t$, denoted by $P|_{t}$, has all the variables
in $P$ except those instantiated by $t$, the domain of each
variable is the same as in $P$, and for each constraint $C$
in $P$ where $vars(C) \not\subseteq vars(t)$, there is a constraint
$C' = \pi_{vars(C) - vars(t)}(\sigma_{t[vars(C) \cap vars(t)]}(C))$
in $P|_{t}$.
\label{DEFN:Induced-CSP}
\end{definition}

\begin{example}
Consider the graph coloring problem and the
corresponding CSP shown in Figure \ref{FIGURE:KC-Proof-Tree}.
The original CSP has four variables, $x_{1},\ldots,x_{4}$, where
$x_{1}, x_{2}, x_{3} \in \{r,g,b\}$ and $x_{4}\in \{r\}$, and
five binary constraints, $x_{1}\not=x_{2}$, $x_{1}\not= x_{3}$,
$x_{2}\not= x_{3}$, $x_{2}\not= x_{4}$ and $x_{3}\not=x_{4}$.
Given a partial solution
$t = \{x_{1} \leftarrow g, x_{2} \leftarrow b\}$,
the CSP induced by $t$, $P|_{t}$, has two variables, $x_{3}$
and $x_{4}$, and the unary and binary constraints shown
in Figure \ref{FIGURE:KC-Proof-Tree-Conv1}.
\label{Example:Induced-CSP}
\end{example}

The maintaining strong $k$-consistency algorithm (MC$_{k}$)
at each node in the backtrack tree applies a strong
$k$-consistency achievement algorithm to the CSP induced by
the current partial solution. Under such an architecture,
FC can be viewed as maintaining one-consistency, and
for binary CSPs, MAC can be viewed as maintaining strong
two-consistency.

An algorithm enforcing strong $k$-consistency on a CSP instance
should detect and remove all those inconsistencies $t =
\{x_{1}\leftarrow a_{1}, \ldots, x_{j}\leftarrow a_{j-1}\}$
where $1 \leq j \leq k$ and $t$ is consistent but cannot be
consistently extended to some $j^{th}$ variable $x_{j}$. To
remove an inconsistency, we make it inconsistent in the
resulting CSP by removing values from domains,
removing inconsistent tuples from existing constraints, or
adding new constraints to the CSP.

We use the concept of a $k$-proof-tree in characterizing the
tuples that are removed by a strong $k$-consistency achievement
algorithm.

\begin{definition}[$k$-proof-tree]
A $k$-proof-tree for a partial solution $t$ over at most $k$
variables in a CSP is a tree in which each node is associated
with a partial solution over at most $k$ variables in the
CSP, where (1) the root of the $k$-proof-tree is associated
with $t$, and (2) each leaf node of the $k$-proof-tree is
inconsistent in the CSP, and (3) each non-leaf node
$s$ of the $k$-proof-tree is consistent in the CSP, and
the children of $s$ at the next level are nodes $s'\cup
\{x\leftarrow a_{1}\},\ldots, s'\cup \{x\leftarrow a_{l}\}$
such that $s' \subseteq s$, $x \not\in vars(s)$, and
$dom(x) = \{a_{1},\ldots, a_{l}\}$.
\label{DEFN:K-Proof-Tree}
\end{definition}

\begin{example}
Figure \ref{FIGURE:KC-Proof-Tree} shows a three-proof-tree
(more than one is possible) for $t = \{x_{1}\leftarrow g\}$ in
the given graph coloring problem. Each non-leaf node, including
the root $t$, is consistent, and each leaf node is inconsistent
in the CSP. Since we have constructed a three-proof-tree for
the tuple $t$ it cannot be part of a solution to the CSP and
a strong $3$-consistency achievement algorithm would remove it.
\end{example}

In general, if a $k$-proof-tree for an inconsistency in
a CSP can be constructed, an algorithm achieving strong
$k$-consistency would deduce and remove the inconsistency.
After applying a strong $k$-consistency achievement
algorithm on the CSP, if all the children of a node in the
$k$-proof-tree are inconsistent in the resulting CSP, that node
is also inconsistent in the resulting CSP because one of its
subtuples cannot be consistently extended to an additional
variable. Because all the leaf nodes in the $k$-proof-tree
are inconsistent in the original CSP, in a bottom-up manner
the inconsistency of the root of the tree can be deduced and
removed from the resulting CSP.
As a special case, if a $k$-proof-tree for the empty
inconsistency in a CSP can be constructed, the CSP will be
empty after enforcing strong $k$-consistency since every way to
extend a variable has been shown to lead to an inconsistency
(and therefore, each value would be removed from the domain
resulting in the empty domain).
On the other hand, after a CSP has been made strongly
$k$-consistent, if a partial solution $t$ over at most $k$
variables is inconsistent in the resulting CSP, a $k$-proof-tree
for $t$ in the original CSP can be constructed. If $t$ is
inconsistent in the original CSP, the $k$-proof-tree contains
the single node $t$. Otherwise, $t$ or a subtuple $t'$ of $t$
cannot be extended to an additional variable $x$; i.e., all
the partial solutions $t' \cup \{x\leftarrow a_{1}\}, \ldots,
t'\cup \{x\leftarrow a_{l}\}$, where $dom(x) = \{a_{1},\ldots,
a_{l}\}$, are inconsistent in the resulting CSP. Then we can
construct the $k$-proof-tree recursively for each of those
inconsistencies.
As a special case,
if a CSP is empty after enforcing strong $k$-consistency,
a $k$-proof-tree for the empty
inconsistency in the original CSP can be constructed.

\begin{figure}[thb]
\begin{center}
\input{figs/KC-proof-tree.pstex_t}
\end{center}
\caption{A three-proof-tree for $\{x_{1}\leftarrow g\}$ in the graph
coloring problem. All leaf nodes in the proof-tree are
inconsistent in the CSP.}
\label{FIGURE:KC-Proof-Tree}
\end{figure}

The following lemmas (Lemma \ref{Lemma:induced-CSP:t=t'}
to Lemma \ref{Lemma:KC-6}) reveal some basic properties
about induced CSPs and strong $k$-consistency enforcement
on induced CSPs, which are used in the proofs of Theorem
\ref{Theorem:MCK-KNode} and Theorem \ref{Theorem:BJk<MCk}.

\begin{lemma}
Given a CSP $P$ and two partial solutions $t$ and $t'$ of $P$, if
$t \subset t'$, then $P|_{t'} = (P|_{t})|_{t'-t}$.
\label{Lemma:induced-CSP:t=t'}
\end{lemma}
\begin{proof}
Clearly $P|_{t'}$ and $(P|_{t})|_{t'-t}$ have the same set of
variables and the same set of domains. Because
$\pi_{vars(C)-vars(t')}\sigma_{t'}C$
$=$
$\pi_{vars(C)-vars(t')}\sigma_{t'-t}(\pi_{vars(C)-vars(t)}\sigma_{t}C)$,
for each constraint $C$ in $P$,
the same selection and projection are made in
$P|_{t'}$ and $(P|_{t})|_{t'-t}$.
Therefore, $P|_{t'}$ and $(P|_{t})|_{t'-t}$
have the same set of constraints.
\qed
\end{proof}

\begin{figure}
\begin{center}
\input{figs/KC-proof-tree-convert1.pstex_t}
\end{center}
\caption{Proof-tree for the empty inconsistency
in the CSP $P|_{t}$ induced by
$t = \{x_{1} \leftarrow g, x_{2} \leftarrow b\}$
constructed from
the proof-tree for $\{x_{1} \leftarrow g\}$
in the CSP $P$ shown in
Figure \ref{FIGURE:KC-Proof-Tree}.
}
\label{FIGURE:KC-Proof-Tree-Conv1}
\end{figure}

\begin{lemma}
Given a CSP $P$ and a consistent partial solution $t$ of $P$,
if
(i) $P$ is empty after achieving strong $k$-consistency, or
(ii) there exists a variable $x \in vars(t)$ such that the
value $t[x]$ is removed from the domain of $x$ when achieving
strong $k$-consistency on $P$,
then
$P|_{t}$ is empty after achieving strong $k$-consistency,
\label{Lemma:KC-1}
\end{lemma}
\begin{proof}
We first show that,
given a consistent partial solution $t$ of a CSP $P$, and a
$k$-proof-tree $T$
for an inconsistency $s$ in $P$,
there is a corresponding well-defined
$k$-proof-tree $T_{t}$
for the inconsistency
$s' = s[vars(s)-vars(t)]$,
in the induced CSP $P|_{t}$,
provided $s$ does not contain any assignments that are inconsistent
with the assignments in $t$.
$T_{t}$ is constructed from $T$ in three steps
(see Figure \ref{FIGURE:KC-Proof-Tree-Conv1} for an example):
(Step 1) Remove from $T$ all nodes and their descendants which
contain assignments that are inconsistent with the assignments
in $t$.
(Step 2) Replace each remaining node $t'$ in $T$ with the node
$t'' = t'[vars(t')-vars(t)]$; i.e., remove those variables which
occur in $t$ and thus do not occur in $P|_{t}$. If $t'$ is not
a leaf node in $T$, then by definition $t'$ is consistent in
$P$. It is possible that the corresponding node $t''$ in $T_{t}$
is inconsistent in $P|_{t}$. Should this be the case, we make
$t''$ into a leaf node by removing all of its descendants.
If $t'$ is a leaf node in $T$, then by definition $t'$ is
inconsistent in $P$; i.e., there exists a constraint $C$ in
$P$ such that $t'$ does not satisfy $C$. It must be the case
that $vars(C) \not\subseteq vars(t)$ (since $vars(C) \subseteq
vars(t)$ contradicts the fact that $t'$ is inconsistent with $C$
and $t$ is consistent and therefore consistent with $C$, but $t'$
and $t$ agree on their assignments by Step 1). Hence, there
is a corresponding constraint $C'$ in $P|_{t}$ which is the
selection and projection of $C$ in $P$. Now, it is easy to
verify that the corresponding node $t''$ is also inconsistent
with $C'$ and is therefore a well-defined leaf node.
(Step 3) Remove all subsumed nodes from $T$, where node $t_2$ is
subsumed by node $t_1$ if $t_2$ is a (necessarily only) child of
$t_1$ and $vars(t_2) \subseteq vars(t_1)$. All children of a
subsumed node $t_2$ are made children of the parent of $t_2$.

Now,
suppose $P$ is empty after achieving strong $k$-consistency.
Then there is a $k$-proof-tree for the empty inconsistency
in $P$ and we can construct a $k$-proof-tree for the empty
inconsistency in $P|_{t}$. Therefore, $P|_{t}$ is empty after
achieving strong $k$-consistency.
Suppose there exists a variable $x \in vars(t)$, such
that the value $t[x]$ is removed from the domain of $x$ when
achieving strong $k$-consistency on $P$. Then there is a
$k$-proof-tree for $\{x\leftarrow t[x]\}$ in $P$ and we can
construct a $k$-proof-tree for the empty inconsistency in
$P|_{t}$. Therefore $P|_{t}$ is empty after achieving strong
$k$-consistency.
\qed
\end{proof}

\begin{lemma}
Given a CSP $P$ and an assignment \{$x \leftarrow a$\},
$a \in dom(x)$, if the induced CSP $P|_{\{x\leftarrow a\}}$
is empty after achieving strong ($k-1$)-consistency, then the
value $a$ is removed from the domain of $x$ when achieving
strong $k$-consistency on $P$.
\label{Lemma:KC-6}
\end{lemma}

\begin{proof}
Suppose $P|_{\{x\leftarrow a\}}$ is empty after achieving strong
($k-1$)-consistency. Thus, there is a ($k-1$)-proof-tree for the
empty inconsistency in $P|_{\{x \leftarrow a\}}$. We now convert
the ($k-1$)-proof-tree to a $k$-proof-tree for $\{x\leftarrow a\}$
in $P$. Each node $t$ in the original ($k-1$)-proof-tree is
replaced by $t \cup \{x\leftarrow a\}$. Thus, the root of the
tree becomes $\{x\leftarrow a\}$. Furthermore, if $t$ is not a
leaf node in the original ($k-1$)-proof-tree; i.e., $t$ is
consistent in $P|_{\{x\leftarrow a\}}$, it is easy to verify that
$t\cup \{x\leftarrow a\}$ is consistent in $P$. If $t$ is a leaf node
in the original ($k-1$)-proof-tree; i.e., $t$ is inconsistent
in $P|_{\{x\leftarrow a\}}$, there is a constraint $C'$ in
$P|_{\{x\leftarrow a\}}$ such that $t$ does not satisfy $C'$.
Let $C'$ be the selection and projection of the constraint $C$ in $P$.
Thus, $t\cup \{x\leftarrow a\}$ does not satisfy the constraint
$C$ in $P$ and is therefore inconsistent in $P$. Hence, we
have constructed a $k$-proof-tree for $\{x\leftarrow a\}$
in $P$ and thus $a$ would be removed from the domain of $x$
when achieving strong $k$-consistency on $P$.
\qed
\end{proof}

MC$_{k}$ extends the current node if the CSP induced by
the current partial solution is not empty after achieving strong
$k$-consistency. The node is thus called a \emph{$k$-consistent
node}.

\begin{definition}[$k$-consistent node]
A node $t$ in the search tree is a \emph{$k$-consistent node} if the CSP
induced by $t$ is not empty after enforcing strong $k$-consistency.
A node which is not $k$-consistent is called $k$-inconsistent.
\label{DEFN:KNode}
\end{definition}

\begin{lemma}
If node $t$ is $k$-consistent, its ancestors are also $k$-consistent.
\label{Lemma:KC->AncestorKC}
\end{lemma}
\begin{proof}
Let $t'$ be one of $t$'s ancestors. Because $t' \subset t$,
from Lemma \ref{Lemma:induced-CSP:t=t'},
$P|_{t} = (P|_{t'})|_{t-t'}$.
Thus, $P|_{t}$ is an induced subproblem of $P|_{t'}$.
From Lemma \ref{Lemma:KC-1}, if $P|_{t}$ is not empty after
achieving strong $k$-consistency, $P|_{t'}$ is not empty either
after achieving strong $k$-consistency. Thus, $t'$ is $k$-consistent. \qed
\end{proof}

The following theorem applies to the case of finding all solutions.
\begin{theorem}
If MC$_{k}$ visits a node, then its parent is $k$-consistent.
If a node is $k$-consistent, then MC$_{k}$ visits the node.
\label{Theorem:MCK-KNode}
\end{theorem}
\begin{proof}
The first part is true because MC$_{k}$ would not branch on this node
if its parent was found $k$-inconsistent. We prove the second
part by induction on the depth of the search tree. The
hypothesis is trivial for $j = 1$. Suppose it is true for $j > 1$ and we
have a $k$-consistent node $t$ at level $j+1$. Let the current variable
be $x$. From Lemma \ref{Lemma:KC->AncestorKC}, $t$'s parent $t'$ at
level $j$ is $k$-consistent. Thus, MC$_{k}$ will visit $t'$. From Lemma
\ref{Lemma:induced-CSP:t=t'}, $P|_{t} = (P|_{t'})
|_{\{x\leftarrow t[x]\}}$. Because
$(P|_{t'})|_{\{x\leftarrow t[x]\}}$ is not empty after
achieving strong $k$-consistency, from Lemma \ref{Lemma:KC-1},
value $t[x]$ will not be removed from the domain of $x$ when achieving strong
$k$-consistency in $P|_{t'}$. As a consequence, MC$_{k}$ will
visit $t$. \qed
\end{proof}

A necessary and sufficient condition for MC$_{k}$ to visit
a node $t$ is that $t$'s parent is $k$-consistent and the value
assigned to the current variable by $t$ has not been removed
from its domain when enforcing strong $k$-consistency on
$t$'s parent.

\begin{theorem}
Given a CSP and a variable ordering,
MC$_{k}$ visits all the nodes that MC$_{k+1}$ visits.
\label{Theorem:MCk<MCk+1}
\end{theorem}
\begin{proof}
Follows from
Theorem \ref{Theorem:MCK-KNode} and
Lemma \ref{Lemma:KC-1}. \qed
\end{proof}

\subsection{Relationship Between BJ$_{k}$ and MC$_{k}$}
\label{SUBSECTION:relationship}

Kondrak and van Beek \citeyear{KovB97} have shown that for
binary CSPs, BJ (BJ$_{1}$) visits all the nodes that FC
(MC$_{1}$) visits, and FC-CBJ (MC$_{1}$-CBJ) and CBJ are
incomparable. We extend their partial ordering of backtracking
algorithms to include the relationship between MC$_{k}$,
BJ$_{k}$, and MC$_{k}$-CBJ, $1 \leq k \leq n$. All of our
results are for the case of general CSPs; i.e., they are not
restricted to binary CSPs.

We begin by characterizing an important property of the CBJ
algorithm.

\begin{lemma}
If CBJ performs a one-level backjump from a deeper
variable $x_{i}$ to a shallower variable $x_{h}$, the node $t_{h}$ at
the level of $x_{h}$ is one-inconsistent.
\label{Lemma:BJ1<MC1}
\end{lemma}
\begin{proof}
Let $S_{i}$ be the conflict set of $x_{i}$ used in
the backjumping in which $x_{h}$ is the deepest
variable. We show that $x_{i}$ will experience a domain
wipe out when enforcing one-consistency on the induced CSP
$P|_{t_{h}[S_{i}]}$. Each node $t_{i}$ at the level of
$x_{i}$ is a leaf node; i.e., $t_{i}$ is inconsistent
in $P$. Suppose $t_{i}$ does not satisfy constraint $C$
where $x_{i} \in vars(C)$ and $vars(C) \subseteq S_{i}\cup
\{x_{i}\}$. The selection of $C$ in $P|_{t_{h}[S_{i}]}$,
which constrains only one variable $\{x_{i}\}$, should
prohibit value $t_{i}[x_{i}]$ of $x_{i}$. Thus, $x_{i}$ will
experience a domain wipe out when enforcing one-consistency
on $P|_{t_{h}[S_{i}]}$. Note that $P|_{t_{h}}$ is an
induced subproblem of $P|_{t_{h}[S_{i}]}$. From Lemma
\ref{Lemma:KC-1}, $P|_{t_{h}}$ is empty after enforcing
one-consistency. Thus, $t_{h}$ at the level of $x_{h}$ is
one-inconsistent.
\qed
\end{proof}

\begin{lemma}
If CBJ performs a $k$-level backjump from a deeper variable $x_{i}$
to a shallower variable $x_{h}$, the current
node $t_{h}$ at the level of $x_{h}$ is $k$-inconsistent.
\label{Lemma:BJK<MCK}
\end{lemma}
\begin{proof}
Let $S_{i}$ be the current conflict set of $x_{i}$ in
which $x_{h}$ is the deepest variable. We show that if
there is a $k$-level backjump from $x_{i}$ to $x_{h}$,
then $P|_{t_{h}[S_{i}]}$ is empty after enforcing strong
$k$-consistency and thus $t_{h}$ is $k$-inconsistent. The
proof is by induction on $k$. $k=1$ is true from Lemma
\ref{Lemma:BJ1<MC1}. Suppose the hypothesis is true for
the case of $k-1$ but it is not true for the case of $k$;
i.e., there is a $k$-level backjump from $x_{i}$ to $x_{h}$,
but the induced CSP $P|_{t_{h}[S_{i}]}$ is not empty after
enforcing strong $k$-consistency. So there is at least one
value $a$ left in the domain of $x_{i}$ after enforcing strong
$k$-consistency on $P|_{t_{h}[S_{i}]}$. We know that the node
$t_{i}$ at the level of $x_{i}$ instantiating $x_{i}$ with $a$
is either incompatible with $t_{h}$ (i.e., it is a leaf node)
or is $l$-level backjumped from some deeper variable $x_{j}$,
for some $1\leq l < k$ (see Figure~\ref{FIGURE:Proof-Scenario}).
However, $t_{i}$ cannot be a leaf node as otherwise $a$ would
be removed from the domain of $x_{i}$ when enforcing strong
$k$-consistency. Let $S_{j}$ be the conflict set
of $x_{j}$. From the hypothesis, the induced CSP
$P|_{t_{i}[S_{j}]}$ is empty after achieving strong
$l$-consistency. Because
value $a$ is not removed from the resulting CSP, from
Lemma \ref{Lemma:KC-6}, the induced CSP $P|_{t_{h}[S_{i}]
\cup \{x_{i} \leftarrow a\}}$ is not empty after achieving
strong ($k-1$)-consistency. Because $t_{i}[S_{j}] \subseteq
t_{h}[S_{i}] \cup \{x_{i} \leftarrow a\}$, the induced CSP
$P|_{t_{i}[S_{j}]}$ is not empty after achieving strong
($k-1$)-consistency. That leads to a contradiction. Thus
$P|_{t_{h}[S_{i}]}$ is empty after achieving strong
$k$-consistency and $t_{h}$ at the level of $x_{h}$ is
$k$-inconsistent. \qed
\end{proof}

\begin{figure}[thb]
\begin{center}
\input{figs/bjk-mck-proof.pstex_t}
\end{center}
\caption{A scenario in the CBJ backtrack tree used in the proof of
Lemma \ref{Lemma:BJK<MCK}.}
\label{FIGURE:Proof-Scenario}
\end{figure}

\begin{theorem}
Given a CSP and a variable ordering,
BJ$_{k}$ visits all the nodes that MC$_{k}$ visits.
\label{Theorem:BJk<MCk}
\end{theorem}
\begin{proof}
The proof is by induction on the level of the search
tree. If MC$_{k}$ visits a node at level $j$ in the search tree,
BJ$_{k}$ visits the same node. $j = 1$ is trivial. Suppose
that it is true for the case of $j > 1$ and we have a node $t$
visited by MC$_{k}$ at level $j+1$. We know both MC$_{k}$
and BJ$_{k}$ visit $t$'s parent at level $j$. The only
chance that $t$ may be skipped by BJ$_{k}$ is that BJ$_{k}$
backjumps from some deeper variable $x_{i}$ at level $i$
to a shallower variable $x_{h}$ at level $h$, such that $h <
j+1 < i$. Thus, the node at level $h$ is $k$-inconsistent
(by Lemma~\ref{Lemma:BJK<MCK}). Since the node at level $h$ is
an ancestor of $t$ and we know $t$'s parent is $k$-consistent
from Lemma \ref{Lemma:KC->AncestorKC}, the node at level $h$
is $k$-consistent. That is the contradiction. Therefore,
BJ$_{k}$ visits $t$ at level $j+1$. \qed
\end{proof}

MC$_{k}$ can be combined with backjumping, namely MC$_{k}$-CBJ,
provided the conflict sets are computed correctly after
achieving strong $k$-consistency on the induced CSPs.

\begin{theorem}
Given a CSP and a variable ordering,
MC$_{k}$ visits all the nodes that MC$_{k}$-CBJ visits.
\label{Theorem:MCK<MCK-CBJ}
\end{theorem}
\begin{proof}
Because MC$_{k}$-CBJ behaves exactly the same as MC$_{k}$ in
the forward phase of a backtracking search, it is easy to verify
that MC$_{k}$-CBJ visits a node $t$ only if $t$'s parent is
$k$-consistent and the value assigned to the current variable
by $t$ was not removed from its domain when achieving strong
$k$-consistency on $t$'s parent. Therefore, MC$_{k}$-CBJ
never visits more nodes than
MC$_{k}$ does. \qed
\end{proof}

In Figure \ref{FIGURE:BJK-MCK-CBJ}, we present a hierarchy in
terms of the size of the backtrack tree for BJ$_{k}$,
MC$_{k}$, and MC$_{k}$-CBJ. If there is a path from algorithm
$\mathcal{A}$ to algorithm $\mathcal{B}$ in the figure,
we know that $\mathcal{A}$
never visits more nodes than
$\mathcal{B}$ does.
For example, MC$_{k}$
never visits more nodes than
BJ$_{j}$, for all $j \leq k$.
Otherwise, there are instances to show $\mathcal{A}$ may be
exponentially better than $\mathcal{B}$, and \emph{vice versa}.

\clearpage

\begin{figure}
\begin{center}
\input{figs/bjk-mck.pstex_t}
\end{center}
\caption{A hierarchy for BJ$_{k}$, MC$_{k}$, and MC$_{k}$-CBJ
in terms of the size of the backtrack tree.}
\label{FIGURE:BJK-MCK-CBJ}
\end{figure}

As the following example shows, for any fixed integer $k < n$, there
exists a CSP instance such that CBJ visits exponentially fewer
nodes than an algorithm that maintains strong $k$-consistency in
the backtracking search\footnote{Independently, Bacchus
and Grove \citeyear{BaGr99} present a similar example to
show that given a fixed $k$, CBJ may be exponentially better
than an algorithm called $MIkC$, which essentially maintains
$k$-consistency in the backtracking search.}.

\begin{example}
Given a fixed integer $k$, we can construct a binary CSP with
$n+k+2$ variables, $x_{1}, \ldots, x_{n-k+1}, y_{1}, \ldots,
y_{k+1}, x_{n-k+2}, \ldots, x_{n+1}$, where $dom(x_{i}) =
\{1, \ldots, n\}$ for $1 \leq i \leq n+1$ and $dom(y_{j}) =
\{1, \ldots, k\}$ for $1 \leq j \leq k+1$. The constraints
are: $x_{i} \not= x_{j}$, for $i \not= j$, and $y_{i} \not=
y_{j}$, for $i \not = j$. The problem consists of two separate
pigeon-hole subproblems, one over variables $x_{1}, \ldots,
x_{n+1}$ and the other over variables $y_{1}, \ldots, y_{k+1}$,
and is insoluble. As we can see, the pigeon-hole problem is
highly locally consistent. The first subproblem is strongly
$n$-consistent and the second is strongly $k$-consistent. Under
the above static variable ordering, a backtracking algorithm
maintaining strong $k$-consistency would not encounter a
dead-end until $x_{n-k+1}$ is instantiated. Then it would find
that the subproblem of $x_{n-k+2}, \ldots, x_{n+1}$ is not
strongly $k$-consistent. Thus, the algorithm will backtrack
before it reaches the second pigeon-hole subproblem. It will
explore $\frac{n!}{k!}$ nodes at level $n-k+1$ of the search
tree and thus take an exponential number of steps to find
the problem is insoluble. CBJ does not encounter a dead-end
at the level of $x_{n-k+1}$ and it continues to the second
pigeon-hole problem. Eventually it will find the second-pigeon
hole problem is insoluble and backjump to the root of the
search tree. The total number of nodes explored is bounded
by a constant, $O((k+1)^{k})$, for a fixed $k$. Therefore,
CBJ can be exponentially better than an algorithm maintaining
strong $k$-consistency.
\label{Example:CBJ}
\end{example}

Example~\ref{Example:CBJ} also shows that,
although MC$_{k}$ visits fewer nodes than BJ$_{k}$ by
Theorem~\ref{Theorem:BJk<MCk}, BJ$_{k+1}$ can be exponentially
better than MC$_{k}$. However, BJ$_{k+1}$ can be better
than MC$_{k}$ only if there is a $(k+1)$-level backjump that
is not also a chronological backtrack. To see that this is
true, suppose that on a particular instance all $(k+1)$-level
backjumps are also chronological backtracks (i.e., the backjump
is to the immediately preceding variable in the variable
ordering and only that single variable becomes uninstantiated
and is removed from the current partial solution). In this
case, the freedom to backjump one additional level rather
than chronologically backtrack does not make a difference and
BJ$_{k+1}$ is effectively BJ$_{k}$ and thus cannot be better
than MC$_{k}$. Thus, BJ$_{k+1}$ can be better than MC$_{k}$
only if there is a $(k+1)$-level non-chronological backjump.
We note, however, that since the number of backjumps of level
$k+1$ is less than or equal to the number of backjumps of
level $k$, as $k$ increases this gets more and more unlikely.
Thus, as the level of local consistency that is maintained in
the backtracking search is increased, the less that backjumping
will be an improvement.

Consider Example \ref{Example:CBJ} again. At each level of the
backtrack tree for MC$_{k}$, the instantiation of each of the
past variables removes one distinct value from the domain of the
current variable (recall that MC$_{k}$ never instantiates the
variable $y_{1}$ as it reaches a dead-end at $x_{n-k+1}$). If
we were to maintain conflict sets for the variables, the
conflict set for the current variable would include all of
its past variables and thus when a dead-end is encountered by
the algorithm, any backjump computed from the conflict sets
would also necessarily be a chronologically backtrack. Thus,
as this example shows, MC$_{k}$-CBJ and MC$_{k}$ can visit
exactly the same nodes and consequently BJ$_{k+1}$ can be
exponentially better than MC$_{k}$-CBJ. Furthermore, because
MC$_{k-1}$-CBJ can reach the second pigeon-hole problem without
encountering a dead-end, it can finally retreat from the second
pigeon-hole problem to the root of the search tree
by backjumps. Thus, MC$_{k-1}$-CBJ may be exponentially better
than MC$_{k}$-CBJ.
In particular, this shows the surprising result that MAC-CBJ
can visit exponentially more nodes than FC-CBJ.

Finally, as the following example shows, for any fixed integer
$k < n$, there exists a CSP instance such that an algorithm
that maintains strong $k$-consistency in the backtracking
search visits exponentially fewer nodes than CBJ.

\begin{example}
Consider the CSP as defined in Example~\ref{Example:CBJ},
but searched with the static variable ordering
$y_{1}, \ldots, y_{k},
x_{1}, \ldots, x_{n+1},
y_{k+1}$.
\end{example}


\section{Empirical Evaluation of Adding CBJ to GAC}

In this section, we report on experiments that examined the
effect of adding CBJ to a backtracking algorithm that maintains
generalized arc consistency (GAC), an algorithm that we refer
to as GAC-CBJ. Previous work has shown the importance of
algorithms that maintain arc consistency (e.g., \citeR{SaFr94,BeRe96}).
We show that adding CBJ to a backtracking algorithm that
maintains generalized arc consistency can speed up the algorithm
by several orders of magnitude on hard, structured problems.

Previous empirical studies of adding CBJ to a backtracking
algorithm that maintains a level of local consistency have
led to mixed conclusions. Adding CBJ to forward checking,
a truncated form of arc consistency, has been shown to
give improvements but not always significant ones. Prosser
\citeyear{Prosser93} observes that with a static variable ordering,
FC-CBJ is about three times faster than FC on the Zebra problem.
Smith and Grant \citeyear{SmGr95} observe that with a dynamic
variable ordering, adding CBJ to FC led to significant savings
but only on hard random problems that occur in the easy region.
Bacchus and van Run \citeyear{BavR95} observe that with a dynamic
variable ordering, adding CBJ to FC only led to at most a 5\%
improvement on the Zebra problem, $n$-Queens problems, and
random binary problems. Bayardo and Schrag \citeyear{BaSc96,BaSc97}
show that adding CBJ to the well-known Davis-Putnam algorithm,
the SAT version of forward checking, can be a significant
improvement on hard random and real-world 3-SAT problems.

Adding CBJ to an algorithm that maintains full arc consistency
has received less attention in the literature.
In the one study that we are aware of,
Bessi\`ere and R\'egin \citeyear{BeRe96} observe that adding CBJ
to MAC (the binary version of GAC) actually slows down the
algorithm on random binary problems due to the overhead of
maintaining the conflict sets. They conjecture that ``when
MAC and a good variable ordering heuristic are used, CBJ
becomes useless''.

Our empirical results lead us to differ with Bessi\`ere and
R\'egin's conclusion about the usefulness of adding CBJ to
an algorithm that maintains full arc consistency. In our
implementation we were able to significantly reduce the
overhead of maintaining the conflict sets through the use
of additional data structures\footnote{See the online appendix
for the source code and a description of the key data structures
in our implementations of GAC and GAC-CBJ.}. On problems where
adding CBJ does not lead to many savings in nodes visited,
our implementation of CBJ also does not degrade performance
by any significant factor. We demonstrate the improvement by
re-doing Bessi\`ere and R\'egin's \citeyear{BeRe96} experiments
on random binary problems. We then show through experiments
in two structured domains that GAC-CBJ can sometimes improve
GAC by several orders of magnitude on hard instances.

In our experiments, we ran both GAC and GAC-CBJ on each instance
of a problem and recorded the CPU times. Comparing CPU times
is appropriate as the underlying code for GAC and GAC-CBJ is
identical, with GAC-CBJ containing only \emph{additional}
code to maintain the conflict sets and to determine how
far to jump back. Two dynamic variable orderings were used:
the popular \emph{dom+deg} heuristic which chooses the next
variable with the minimal domain size and breaks ties by
choosing the variable with the maximum degree (the number of the
constraints that constrain that variable) and the \emph{dom/deg}
heuristic proposed by Bessi\`ere and R\'egin \citeyear{BeRe96}
which chooses the next variable with the minimal value of the
domain size divided by its degree. All experiments were run
on 400 MHz Pentium II's with 256 Megabytes of memory.

\subsection{Random Problems}

The run time performance of GAC and GAC-CBJ were compared on
sets of randomly generated binary CSPs. A set of random
problems is defined by a $5$-tuple $(n,d,r,m,t)$, where
$n$ is the number of the variables,
$d$ is the uniform domain size,
$r$ is the uniform arity of the constraints,
$m$ is the number of randomly generated constraints, and
$t$ is the uniform tightness or number of tuples in each constraint.
In each case, the constraint tightness $t$ was chosen so that
approximately half of the instances in the population were insoluble;
i.e., the instances were from the phase transition region.

\begin{table}[thb]
\caption{
Effect of domain size on average time (seconds) to solve
random instances from $(50,d,2,95,t)$.
Each set contained 100 random instances.
Both GAC-CBJ and GAC used the \emph{dom/deg} variable ordering.
}\label{TABLE:Random}
\begin{center}
\begin{tabular}{r|D{.}{.}{4}|D{.}{.}{4}|D{.}{.}{2}}
\multicolumn{1}{c|}{$d$}
        & \multicolumn{1}{c|}{GAC-CBJ}
        & \multicolumn{1}{c|}{GAC}
        & \multicolumn{1}{c}{ratio} \\\hline
%------------------------------------
%  d  |   GAC   | GAC-CBJ | GAC /   |
%     |         |         | GAC-CBJ |
%------------------------------------
   5  &  0.0027 &  0.0030 &  0.90  \\
  10  &  0.026  &  0.027  &  0.96  \\
  15  &  0.10   &  0.10   &  1.00  \\
  20  &  0.41   &  0.41   &  1.00  \\
  25  &  0.79   &  0.78   &  1.01  \\
  30  &  2.46   &  2.47   &  1.00  \\
  35  &  3.82   &  3.80   &  1.01  \\
  40  & 10.98   & 10.75   &  1.02
%------------------------------------
\end{tabular}
\end{center}
\end{table}

Bessi\`ere and R\`egin \citeyear{BeRe96} examine the effect of
domain size on the average time to solve random instances from
$(50,d,2,95,t)$ (see Figure 5 (right) in \citeR{BeRe96}).
With their implementation of CBJ, adding CBJ steadily
worsens performance as domain size increases until at $d
= 40$ MAC-CBJ is about 1.7 times slower than MAC alone.
With our implementation, the difference in performance between
GAC-CBJ and GAC was negligible on these problems (see Table
\ref{TABLE:Random}).

The remaining sets of random problems that Bessi\`ere and
R\`egin used in their experiments to compare the performance
of MAC-CBJ and MAC are now too simple to provide a meaningful
comparison as they can be solved in less than 0.01 seconds
on a 400 MHz Pentium II computer. Thus, we chose harder sets
of random binary problems. On each instance we ran both GAC
and GAC-CBJ and recorded the CPU times. Here we report the
average ratio of the CPU times (GAC over GAC-CBJ). Each set
contained 100 random instances. On the first set of problems,
$(150,5,2,750,19)$, the average ratio for the \emph{dom+deg}
variable ordering was 0.90 and the average ratio for the
\emph{dom/deg} variable ordering was 0.88. On the second set of
problems, $(150,5,2,1500,21)$, the average ratios for both the
\emph{dom+deg} and \emph{dom/deg} variable orderings was 0.93.
In other words, on average GAC was a little over 10\% faster
than GAC-CBJ on these problems.

\subsection{Planning Problems}

Planning, where one is required to find a sequence of actions
from an initial state to a goal state, can be formulated as a
CSP. In the formulation we used in our experiments, each state
is modeled by a collection of variables and the constraints
enforce the assignments of variables to represent a consistent
state or a valid transition between states.
(See \citeR{KaSe92,vBCh99} for more details on the formulation
of planning as a CSP.)

\begin{table}[th]
\caption{
Time (seconds) to solve instances of the grid planning problem.
The absence of an entry indicates that the problem
was not solved within 72000 seconds (20 hours)
of CPU time.}\label{TABLE:Grid}
\begin{center}
\begin{tabular}{c|r|r|r|r}
\multicolumn{1}{c|}{}
        & \multicolumn{2}{c|}{ \emph{dom+deg} }
        & \multicolumn{2}{c}{ \emph{dom/deg} } \\\hline
\multicolumn{1}{c|}{}
        & \multicolumn{1}{c|}{ GAC }
        & \multicolumn{1}{c|}{ GAC-CBJ }
        & \multicolumn{1}{c|}{ GAC }
        & \multicolumn{1}{c}{ GAC-CBJ } \\\hline
%------------------------------------------------------
% problem |    GAC   | GAC-CBJ  |    GAC   | GAC-CBJ  |
%------------------------------------------------------
    1     &    0.66  &    0.68  &    1.58  &     0.86 \\
    2     &\bf{762.47}&\bf{33.33}&\bf{3965.10}&\bf{321.17}\\
    3     &   \dash  &   \dash  &   \dash  &   \dash  \\
    4     &\bf{\dash}&\bf{1753.13}& \dash   &   \dash \\
    5     &   \dash  &   \dash  &   \dash  &   \dash
%--------------------------------
\end{tabular}
\end{center}
\end{table}

In the experiments we used all 130 instances used in the First
AI Planning Systems Competition, June 6--9, 1998. The instances
come from five different domains: gripper, mystery, mprime,
logistics, and grid. In the experiments we report, both GAC and
GAC-CBJ were based on AC3 \cite{Mackworth77} as this was found
to give the best performance.

For the gripper, mystery, and mprime domains, each of the
instances could be solved in under 25 seconds by both GAC
and GAC-CBJ. On these easy problems, the increased overhead
of CBJ rarely led to savings, and overall GAC was 10-15\%
faster than GAC-CBJ.

Table \ref{TABLE:Grid} shows the comparison between GAC and
GAC-CBJ in solving the 5 instances of the grid problems. GAC-CBJ
showed improvement on the grid problems. For example, it solved
problem 4 in about half an hour, but GAC failed to find
a solution in 20 hours.

Table \ref{TABLE:Logistics} shows the comparison between GAC and
GAC-CBJ in solving the 30 instances of the logistics problem. On
about one third of the instances, GAC-CBJ improved on GAC. For
example, on instances 18, 20 and 27, GAC-CBJ ran several
orders of magnitude faster than GAC, and on instance 15,
GAC exhausted the 20 hours time limit but GAC-CBJ found a
solution within 3 minutes. GAC-CBJ and GAC performed similarly
on easier instances and sometimes GAC-CBJ was about 10\%
slower than GAC.

\clearpage

\begin{table}
\caption{Time (seconds) to solve instances of the logistics planning problem.
The absence of an entry indicates that the problem
was not solved within 72000 seconds (20 hours)
of CPU time.}\label{TABLE:Logistics}
\begin{center}
\begin{tabular}{c|r|r|r|r}
\multicolumn{1}{c|}{}
        & \multicolumn{2}{c|}{ \emph{dom+deg} }
        & \multicolumn{2}{c}{ \emph{dom/deg} } \\\hline
\multicolumn{1}{c|}{}
        & \multicolumn{1}{c|}{ GAC }
        & \multicolumn{1}{c|}{ GAC-CBJ }
        & \multicolumn{1}{c|}{ GAC }
        & \multicolumn{1}{c}{ GAC-CBJ } \\\hline
%------------------------------------------------------
% problem |    GAC   | GAC-CBJ  |    GAC   | GAC-CBJ  |
%------------------------------------------------------
    1     &    0.03  &    0.03  &     0.03 &     0.03 \\
    2     &    0.03  &    0.05  &     0.03 &     0.06 \\
    3     &\bf{10.91}&\bf{0.86} &\bf{9.63} &\bf{0.81} \\
    4     &    0.16  &    0.17  &     0.14 &     0.18 \\
    5     &    1.51  &    1.54  &     1.54 &     1.57 \\
    6     &\bf{36.49}&\bf{16.86}&\bf{35.77}&\bf{16.76}\\
    7     &    0.08  &    0.08  &     0.08 &     0.09 \\
    8     &    0.15  &    0.15  &     0.14 &     0.16 \\
    9     &    0.30  &    0.33  &     0.32 &     0.33 \\
   10     &   \dash  &   \dash  &    \dash &    \dash \\
   11     &    0.04  &    0.05  &     0.05 &     0.05 \\
   12     &    0.11  &    0.13  &     0.11 &     0.11 \\
   13     &    0.54  &    0.57  &     0.54 &     0.56 \\
   14     &    0.63  &    0.64  &     0.64 &     0.68 \\
   15     &\bf{\dash}&\bf{182.51}&\bf{\dash}&\bf{8540.58} \\
   16     &\bf{12.49}&\bf{0.42}  &\bf{12.32}&\bf{0.41} \\
   17     &\bf{264.46}&\bf{0.32} &\bf{261.33}&\bf{0.32}  \\
   18     &\bf{15382.82}&\bf{1165.54}&\bf{15157.71}&\bf{1184.67}\\
   19     &    1.29  &    1.37  &     1.33 &     1.31 \\
   20     &\bf{6268.16}&\bf{27.66}&\bf{6125.87}&\bf{28.55}\\
   21     &    0.66  &    0.70  &     0.68 &     0.74 \\
   22     &   \dash  &   \dash  &    \dash &    \dash \\
   23     &   \dash  &   \dash  &    \dash &    \dash \\
   24     &    0.08  &    0.09  &     0.08 &     0.09 \\
   25     &   34.03  &   13.03  &    11.58 &    12.10 \\
   26     &   \dash  &   \dash  &    \dash &    \dash \\
   27     &\bf{12239.26}&\bf{47.06}&\bf{12105.62}&\bf{47.76}\\
   28     &   \dash  &   \dash  &    \dash &    \dash \\
   29     &   \dash  &   \dash  &    \dash &    \dash \\
   30     &   \dash  &   \dash  &    \dash &    \dash
%--------------------------------------------------------
\end{tabular}
\end{center}
\end{table}

\clearpage

\subsection{Crossword Puzzle Problems}

Crossword puzzle generation, where one is required to fill
in a grid with words from a dictionary, can be formulated
as a CSP. In the formulation we used in our experiments,
each of the unknown words is represented by a variable which
takes values from the dictionary. Binary constraints enforce
that intersecting words agree on their intersecting letter
and that a word from the dictionary appears at most once in
a solution. Figure \ref{FIGURE:Crossword-Puzzle} shows an
example 5 $\times$ 5 crossword puzzle grid. A CSP model of this
grid has 10 variables, 21 binary ``intersection'' constraints,
and 13 ``not equals'' constraints.

\begin{figure}[thb]
\begin{center}
\psfig{file=figs/crossword.ps}
\end{center}
\caption{A crossword puzzle.}
\label{FIGURE:Crossword-Puzzle}
\end{figure}

In the experiments we used 50 grids and two dictionaries for
a total of 100 instances of the problem that ranged from easy
to very hard. For the grids, we used 10 instances at each of
the following sizes:
 5$\times$5,
15$\times$15,
19$\times$19,
21$\times$21, and
23$\times$23.
For the dictionaries we used the UK dictionary, which collects
about 220,000 words and in which the largest domain for a
word variable contains about 30,000 values, and the Linux
dictionary, which collects 45,000 words and in which the
largest domain for a word variable has about 5,000 values.
In the experiments we report, both GAC and GAC-CBJ were
based on AC7 \cite{BeRe97} as this was found to give the
best performance (see \citeR{Sillito-thesis} for a discussion
of integrating AC7 into backtracking search).

\begin{figure}[thb]
\noindent
\begin{center}
\mbox{\psfig{figure=figs/ratios.ps,height=2.75in,width=4.125in}}
\end{center}
\caption{Effect on execution time of GAC of adding
conflict-directed backjumping (GAC-CBJ).
A curve represents 100 tests on instances of the
crossword puzzle problem where the tests are ordered
by the ratio of time taken to solve the instance by
GAC over time taken to solve the instance by GAC-CBJ.
}\label{FIGURE:ratios}
\end{figure}

Figure~\ref{FIGURE:ratios} shows approximate cumulative
frequency curves for the empirical results, where we are
plotting the ratio of the time taken to solve an instance by
GAC over the time taken to solve the instance by GAC-CBJ. Thus,
for example, we can read from the curve representing the
\emph{dom+deg} variable ordering that for approximately 85\%
of the tests adding CBJ had little effect and that for the
remaining 15\% of the tests it led to orders of magnitude
improvements. We can also read from the curves the 0, 10,
\ldots, 100 percentiles of the data sets (where the value of
the median is the 50{\em th} percentile or the value of the
50{\em th} test). The crossover point, where GAC-CBJ starts
to perform as well as or better than GAC occurs around the
35{\em th} percentile. Tables \ref{TABLE:PuzzleSummary1}
and \ref{TABLE:PuzzleSummary2} examine the data more closely
by showing the actual times to solve the instances where GAC
performed best and the instances where GAC-CBJ performed best.

\begin{table}[thb]
\caption{
	GAC versus GAC-CBJ on instances of the crossword puzzle problem.
	The ten best improvements in time (seconds) of GAC over GAC-CBJ
	to solve an instance are presented.
}\label{TABLE:PuzzleSummary1}
\begin{center}
\begin{tabular}{c|r|r|r|r}
\multicolumn{1}{c|}{}
        & \multicolumn{2}{c|}{ \emph{dom+deg} }
        & \multicolumn{2}{c}{ \emph{dom/deg} }\\\hline
\multicolumn{1}{c|}{rank}
        & \multicolumn{1}{c|}{ GAC }
        & \multicolumn{1}{c|}{ GAC-CBJ }
        & \multicolumn{1}{c|}{ GAC }
        & \multicolumn{1}{c }{ GAC-CBJ }\\\hline
%--------------------------------------------------------
% number  |    GAC    | GAC-CBJ  |    GAC    | GAC-CBJ  |
%--------------------------------------------------------
    1     &    1.21   &    1.35  &    1.11   &    1.23 \\
    2     &    1.10   &    1.20  &    0.95   &    1.02 \\
    3     &    6.12   &    6.53  &    1.16   &    1.24 \\
    4     &    0.78   &    0.81  &   56.66   &   60.36 \\
    5     &  110.23   &  114.52  &    1.30   &    1.37 \\
    6     &   68.67   &   71.28  &    4.86   &    5.11 \\
    7     &   47.16   &   48.42  &    0.22   &    0.23 \\
    8     &   32.69   &   33.63  &   14.23   &   14.76 \\
    9     &   25.17   &   26.08  &   74.38   &   77.52 \\
   10     &   20.73   &   21.37  &    7.43   &    7.67
%--------------------------------------------------------
\end{tabular}
\end{center}
\end{table}

\begin{table}[thb]
\caption{
	GAC versus GAC-CBJ on instances of the crossword puzzle problem.
	The ten best improvements in time (seconds) of GAC-CBJ over GAC
	to solve an instance are presented.
	The absence of an entry indicates that the problem
	was not solved within 36000 seconds (10 hours) of CPU time.
}\label{TABLE:PuzzleSummary2}
\begin{center}
\begin{tabular}{c|r|r|r|r}
\multicolumn{1}{c|}{}
        & \multicolumn{2}{c|}{ \emph{dom+deg} }
        & \multicolumn{2}{c}{ \emph{dom/deg} }\\\hline
\multicolumn{1}{c|}{rank}
        & \multicolumn{1}{c|}{ GAC }
        & \multicolumn{1}{c|}{ GAC-CBJ }
        & \multicolumn{1}{c|}{ GAC }
        & \multicolumn{1}{c }{ GAC-CBJ }\\\hline
%--------------------------------------------------------
% number  |    GAC    | GAC-CBJ  |    GAC    | GAC-CBJ  |
%--------------------------------------------------------
    1     &  \dash    &   37.85  &  \dash    &   54.60 \\
    2     &  \dash    &   41.43  &  10311.32 &   33.43 \\
    3     &  \dash    &   67.07  &  \dash    &  225.92 \\
    4     &  \dash    &   82.58  &  \dash    &  244.81 \\
    5     &  \dash    &  276.00  &  \dash    &  308.04 \\
    6     &  \dash    &  542.80  &  \dash    &  374.72 \\
    7     &  \dash    &  939.71  &  \dash    &  832.68 \\
    8     &   2716.86 &  115.87  &  \dash    & 1486.43 \\
    9     &    390.91 &   34.90  &  \dash    & 1890.24 \\
   10     &  \dash    & 3336.37  &  \dash    & 3411.83
%--------------------------------------------------------
\end{tabular}
\end{center}
\end{table}

In summary, on some of the smaller, easier crossword puzzle
instances GAC was slightly faster than GAC-CBJ, on many of the
puzzles there was no noticeable difference, and on some of the
larger, harder puzzles GAC-CBJ was orders of magnitude faster
than GAC.

\section{Conclusion}

In this paper, we presented three main results. First, we
showed that the choice of dynamic variable ordering heuristic
can weaken the effects of the backjumping technique. Second,
we showed that as the level of local consistency that is
maintained in the backtracking search is increased, the less
that backjumping will be an improvement. Together these results
partially explain why a backtracking algorithm doing more in
the look-ahead phase cannot benefit more from the backjumping
look-back scheme and they extend the partial ordering of
backtracking algorithms presented by Kondrak and van Beek
\citeyear{KovB97} to include backtracking algorithms and their
CBJ hybrids that maintain levels of local consistency beyond
forward checking. Third, and finally, we showed that adding
CBJ to a backtracking algorithm that maintains generalized
arc consistency can (still) speed up the algorithm by several
orders of magnitude on hard, structured problems. Throughout
the paper, we did not restrict ourselves to binary CSPs.


\acks{The authors wish to thank the referees for their careful
reading of a previous version of the paper and their helpful
comments. The financial support of the Canadian Government
through their NSERC program is gratefully acknowledged.
}

%\bibliographystyle{theapa}
%\bibliography{csp}
\begin{thebibliography}{}

\bibitem[\protect\BCAY{Bacchus\ \BBA\ Grove}{Bacchus\ \BBA\
  Grove}{1999}]{BaGr99}
Bacchus, F.\BBACOMMA\  \BBA\ Grove, A. \BBOP1999\BBCP.
\newblock \BBOQ Looking forward in constraint satisfaction algorithms\BBCQ\
\newblock Unpublished manuscript.

\bibitem[\protect\BCAY{Bacchus\ \BBA\ van Run}{Bacchus\ \BBA\ van
  Run}{1995}]{BavR95}
Bacchus, F.\BBACOMMA\  \BBA\ van Run, P. \BBOP1995\BBCP.
\newblock \BBOQ Dynamic variable ordering in {CSP}s\BBCQ\
\newblock In {\Bem Proceedings of the First International Conference on
  Principles and Practice of Constraint Programming}, \BPGS\ 258--275, Cassis,
  France.
\newblock Available as: Springer Lecture Notes in Computer Science 976.

\bibitem[\protect\BCAY{{Bayardo Jr.}\ \BBA\ Schrag}{{Bayardo Jr.}\ \BBA\
  Schrag}{1996}]{BaSc96}
{Bayardo Jr.}, R.~J.\BBACOMMA\  \BBA\ Schrag, R. \BBOP1996\BBCP.
\newblock \BBOQ Using {CSP} look-back techniques to solve exceptionally hard
  {SAT} instances\BBCQ\
\newblock In {\Bem Proceedings of the Second International Conference on
  Principles and Practice of Constraint Programming}, \BPGS\ 46--60, Cambridge,
  Mass.
\newblock Available as: Springer Lecture Notes in Computer Science 1118.

\bibitem[\protect\BCAY{{Bayardo Jr}\ \BBA\ Schrag}{{Bayardo Jr}\ \BBA\
  Schrag}{1997}]{BaSc97}
{Bayardo Jr}, R.~J.\BBACOMMA\  \BBA\ Schrag, R.~C. \BBOP1997\BBCP.
\newblock \BBOQ Using {CSP} look-back techniques to solve real-world {SAT}
  instances\BBCQ\
\newblock In {\Bem Proceedings of the Fourteenth National Conference on
  Artificial Intelligence}, \BPGS\ 203--208, Providence, RI.

\bibitem[\protect\BCAY{Bessi\`ere\ \BBA\ R\'egin}{Bessi\`ere\ \BBA\
  R\'egin}{1996}]{BeRe96}
Bessi\`ere, C.\BBACOMMA\  \BBA\ R\'egin, J.-C. \BBOP1996\BBCP.
\newblock \BBOQ {MAC} and combined heuristics: Two reasons to forsake {FC} (and
  {CBJ}?) on hard problems\BBCQ\
\newblock In {\Bem Proceedings of the Second International Conference on
  Principles and Practice of Constraint Programming}, \BPGS\ 61--75, Cambridge,
  Mass.

\bibitem[\protect\BCAY{Bessi\`ere\ \BBA\ R\'egin}{Bessi\`ere\ \BBA\
  R\'egin}{1997}]{BeRe97}
Bessi\`ere, C.\BBACOMMA\  \BBA\ R\'egin, J.-C. \BBOP1997\BBCP.
\newblock \BBOQ Arc consistency for general constraint networks: Preliminary
  results\BBCQ\
\newblock In {\Bem Proceedings of the Sixteenth International Joint Conference
  on Artificial Intelligence}, \BPGS\ 398--404, Nagoya, Japan.

\bibitem[\protect\BCAY{Bruynooghe}{Bruynooghe}{1981}]{Bruynooghe81}
Bruynooghe, M. \BBOP1981\BBCP.
\newblock \BBOQ Solving combinatorial search problems by intelligent
  backtracking\BBCQ\
\newblock {\Bem Information Processing Letters}, {\Bem 12}, 36--39.

\bibitem[\protect\BCAY{Chen}{Chen}{2000}]{Chen00}
Chen, X. \BBOP2000\BBCP.
\newblock {\Bem A Theoretical Comparison of Selected {CSP} Solving and Modeling
  Techniques}.
\newblock Ph.D.\ thesis, University of Alberta.

\bibitem[\protect\BCAY{Dechter}{Dechter}{1990}]{Dechter90}
Dechter, R. \BBOP1990\BBCP.
\newblock \BBOQ Enhancement schemes for constraint processing: Backjumping,
  learning, and cutset decomposition\BBCQ\
\newblock {\Bem Artificial Intelligence}, {\Bem 41}, 273--312.

\bibitem[\protect\BCAY{Dechter}{Dechter}{1992}]{Dechter92survey}
Dechter, R. \BBOP1992\BBCP.
\newblock \BBOQ Constraint networks\BBCQ\
\newblock In Shapiro, S.~C.\BED, {\Bem Encyclopedia of Artificial Intelligence,
  2nd Edition}, \BPGS\ 276--285. John Wiley \& Sons.

\bibitem[\protect\BCAY{Freuder}{Freuder}{1978}]{Freuder78}
Freuder, E.~C. \BBOP1978\BBCP.
\newblock \BBOQ Synthesizing constraint expressions\BBCQ\
\newblock {\Bem Comm. ACM}, {\Bem 21}, 958--966.

\bibitem[\protect\BCAY{Frost\ \BBA\ Dechter}{Frost\ \BBA\
  Dechter}{1994}]{FrDe94b}
Frost, D.\BBACOMMA\  \BBA\ Dechter, R. \BBOP1994\BBCP.
\newblock \BBOQ Dead-end driven learning\BBCQ\
\newblock In {\Bem Proceedings of the Twelfth National Conference on Artificial
  Intelligence}, \BPGS\ 294--300, Seattle, Wash.

\bibitem[\protect\BCAY{Gaschnig}{Gaschnig}{1978}]{Gaschnig78}
Gaschnig, J. \BBOP1978\BBCP.
\newblock \BBOQ Experimental case studies of backtrack vs. {Waltz}-type vs. new
  algorithms for satisficing assignment problems\BBCQ\
\newblock In {\Bem Proceedings of the Second Canadian Conference on Artificial
  Intelligence}, \BPGS\ 268--277, Toronto, Ont.

\bibitem[\protect\BCAY{Haralick\ \BBA\ Elliott}{Haralick\ \BBA\
  Elliott}{1980}]{HaEl80}
Haralick, R.~M.\BBACOMMA\  \BBA\ Elliott, G.~L. \BBOP1980\BBCP.
\newblock \BBOQ Increasing tree search efficiency for constraint satisfaction
  problems\BBCQ\
\newblock {\Bem Artificial Intelligence}, {\Bem 14}, 263--313.

\bibitem[\protect\BCAY{Kautz\ \BBA\ Selman}{Kautz\ \BBA\ Selman}{1992}]{KaSe92}
Kautz, H.\BBACOMMA\  \BBA\ Selman, B. \BBOP1992\BBCP.
\newblock \BBOQ Planning as satisfiability\BBCQ\
\newblock In {\Bem Proceedings of the 10th European Conference on Artificial
  Intelligence}, \BPGS\ 359--363, Vienna.

\bibitem[\protect\BCAY{Kondrak\ \BBA\ van Beek}{Kondrak\ \BBA\ van
  Beek}{1997}]{KovB97}
Kondrak, G.\BBACOMMA\  \BBA\ van Beek, P. \BBOP1997\BBCP.
\newblock \BBOQ A theoretical evaluation of selected backtracking
  algorithms\BBCQ\
\newblock {\Bem Artificial Intelligence}, {\Bem 89}, 365--387.

\bibitem[\protect\BCAY{Mackworth}{Mackworth}{1977a}]{Mackworth77}
Mackworth, A.~K. \BBOP1977a\BBCP.
\newblock \BBOQ Consistency in networks of relations\BBCQ\
\newblock {\Bem Artificial Intelligence}, {\Bem 8}, 99--118.

\bibitem[\protect\BCAY{Mackworth}{Mackworth}{1977b}]{Mackworth77IJCAI}
Mackworth, A.~K. \BBOP1977b\BBCP.
\newblock \BBOQ On reading sketch maps\BBCQ\
\newblock In {\Bem Proceedings of the Fifth International Joint Conference on
  Artificial Intelligence}, \BPGS\ 598--606, Cambridge, Mass.

\bibitem[\protect\BCAY{McGregor}{McGregor}{1979}]{McGregor79}
McGregor, J.~J. \BBOP1979\BBCP.
\newblock \BBOQ Relational consistency algorithms and their application in
  finding subgraph and graph isomorphisms\BBCQ\
\newblock {\Bem Inform. Sci.}, {\Bem 19}, 229--250.

\bibitem[\protect\BCAY{Montanari}{Montanari}{1974}]{Montanari74}
Montanari, U. \BBOP1974\BBCP.
\newblock \BBOQ Networks of constraints: Fundamental properties and
  applications to picture processing\BBCQ\
\newblock {\Bem Inform. Sci.}, {\Bem 7}, 95--132.

\bibitem[\protect\BCAY{Nadel}{Nadel}{1989}]{Nadel89}
Nadel, B.~A. \BBOP1989\BBCP.
\newblock \BBOQ Constraint satisfaction algorithms\BBCQ\
\newblock {\Bem Computational Intelligence}, {\Bem 5}, 188--224.

\bibitem[\protect\BCAY{Prosser}{Prosser}{1993a}]{Prosser93a}
Prosser, P. \BBOP1993a\BBCP.
\newblock \BBOQ Domain filtering can degrade intelligent backtracking
  search\BBCQ\
\newblock In {\Bem Proceedings of the Thirteenth International Joint Conference
  on Artificial Intelligence}, \BPGS\ 262--267, Chamb\`{e}ry, France.

\bibitem[\protect\BCAY{Prosser}{Prosser}{1993b}]{Prosser93}
Prosser, P. \BBOP1993b\BBCP.
\newblock \BBOQ Hybrid algorithms for the constraint satisfaction problem\BBCQ\
\newblock {\Bem Computational Intelligence}, {\Bem 9}, 268--299.

\bibitem[\protect\BCAY{Prosser}{Prosser}{1995}]{Prosser95}
Prosser, P. \BBOP1995\BBCP.
\newblock \BBOQ {MAC-CBJ}: Maintaining arc consistency with conflict-directed
  backjumping\BBCQ\
\newblock Research report\ 177, University of Strathclyde.

\bibitem[\protect\BCAY{Sabin\ \BBA\ Freuder}{Sabin\ \BBA\
  Freuder}{1994}]{SaFr94}
Sabin, D.\BBACOMMA\  \BBA\ Freuder, E.~C. \BBOP1994\BBCP.
\newblock \BBOQ Contradicting conventional wisdom in constraint
  satisfaction\BBCQ\
\newblock In {\Bem Proceedings of the 11th European Conference on Artificial
  Intelligence}, \BPGS\ 125--129, Amsterdam.

\bibitem[\protect\BCAY{Schiex\ \BBA\ Verfaillie}{Schiex\ \BBA\
  Verfaillie}{1994}]{ScVe94}
Schiex, T.\BBACOMMA\  \BBA\ Verfaillie, G. \BBOP1994\BBCP.
\newblock \BBOQ Nogood recording for static and dynamic constraint satisfaction
  problems\BBCQ\
\newblock {\Bem International Journal on Artificial Intelligence Tools}, {\Bem
  3}, 1--15.

\bibitem[\protect\BCAY{Sillito}{Sillito}{2000}]{Sillito-thesis}
Sillito, J. \BBOP2000\BBCP.
\newblock \BBOQ {I}mproving and {E}stimating the {C}ost of {B}acktracking
  {A}lgorithms for {CSP}s\BBCQ.
\newblock MSc thesis, University of Alberta, 2000.

\bibitem[\protect\BCAY{Smith\ \BBA\ Grant}{Smith\ \BBA\ Grant}{1995}]{SmGr95}
Smith, B.~M.\BBACOMMA\  \BBA\ Grant, S.~A. \BBOP1995\BBCP.
\newblock \BBOQ Sparse constraint graphs and exceptionally hard problems\BBCQ\
\newblock In {\Bem Proceedings of the Fourteenth International Joint Conference
  on Artificial Intelligence}, \BPGS\ 646--651, Montreal.

\bibitem[\protect\BCAY{van Beek\ \BBA\ Chen}{van Beek\ \BBA\
  Chen}{1999}]{vBCh99}
van Beek, P.\BBACOMMA\  \BBA\ Chen, X. \BBOP1999\BBCP.
\newblock \BBOQ {CPlan}: A constraint programming approach to planning\BBCQ\
\newblock In {\Bem Proceedings of the Sixteenth National Conference on
  Artificial Intelligence}, \BPGS\ 585--590, Orlando, Florida.

\end{thebibliography}

\end{document}
