Search algorithms that maintain local consistencies are widely used for CSP solving. Some of them have been extended to the non-binary case. For example, maintaining arc consistency (MAC) and forward checking (FC). It has been shown that the non-binary version of MAC (MGAC) applied in a non-binary CSP is equivalent to MAC applied in the HVE of the CSP when only original variables are instantiated and the same variable orderings are used [Stergiou WalshStergiou Walsh1999]. We show that, like MGAC, non-binary extensions of FC can be emulated by equivalent algorithms that run in the HVE.
FC [Haralick ElliotHaralick Elliot1980] was first generalized to handle non-binary
constraints by Van Hentenryck VanHentenryck89.
According to the definition of Van Hentenryck
VanHentenryck89, forward checking is performed after
the -1 variables of an
-ary constraint have been assigned
and the remaining variable is unassigned. This algorithm is called
nFC0 in the paper by Bessiére, Meseguer, Freuder, & Larrosa
bmfl99 where more, and stronger, generalizations of FC
to non-binary constraints were introduced. These generalizations
differ between them in the extent of look-ahead they perform after
each variable instantiation. Algorithm nFC1 applies one pass of
GAC on each constraint or constraint projection involving the
current variable and exactly one future variable4.
Algorithm nFC2 applies GAC on the set of constraints involving the
current variable and at least one future variable, in one pass.
Algorithm nFC3 applies GAC to the set of constraints involving the
current variable and at least one future variable. Algorithm nFC4
applies GAC on the set of constraints involving at least one past
variable and at least one future variable, in one pass. Algorithm
nFC5, which is the strongest version, applies GAC to the set of
constraints involving at least one past variable and at least one
future variable. All the generalizations reduce to simple FC when
applied to binary constraints.
We will show that the various versions of nFC are equivalent, in
terms of visited nodes, to binary versions of FC that run in the
HVE of the problem. This holds under the assumption that the
binary algorithms only assign original variables and they use the
same variable and value ordering heuristics, static or dynamic, as
their non-binary counterparts. Note that if such an algorithm
finds a consistent assignment for all original variables, and
these assignments are propagated to the dual variables, then all
the domains of the dual variables will be reduced to singletons.
That is, the domain of each dual variable will only contain
the single tuple that is consistent with the assignments of the
original variables constrained with
. Therefore, the
algorithm can proceed to assign the dual variables in a
backtrack-free manner.
The equivalence between nFC1 and a version of FC for the HVE, called FC+ [Bacchus van BeekBacchus van Beek1998], has been proved by Bessiére et al. bmfl99. FC+ is a specialized forward checking algorithm for the HVE. It operates like standard binary FC except that when the domain of a dual variable is pruned, FC+ removes from adjacent original variables any value which is no longer supported.
Algorithms nFC2-nFC5 also have equivalent algorithms that operate in the HVE. We call these algorithms hFC2-hFC5. For example, hFC5 will enforce AC on the set of dual variables, and original variables connected to them, such that each dual variable is connected to at least one past original variable and at least one future original variable. Note that nFC0 has no natural equivalent algorithm in the HVE. If we emulate it in the HVE we will get an inefficient and awkward algorithm. In the following, hFC0 will refer to the standard binary FC algorithm and hFC1 will refer to FC+.
Proof:
We prove this for nFC5, the strongest among the generalized FC
algorithms. The proof for the other versions is similar. We only
need to prove that at each node of the search tree algorithms nFC5
and hFC5 will delete exactly the same values from the domains of
original variables. Assume that at some node, after instantiating
the current variable, nFC5 deletes value from a future
variable
. Then there exists some constraint
including
and at least one past variable, and value
of
has
no supporting tuple in
. In the HVE, when hFC5 tries to make
(the dual variable corresponding to
) AC it will remove
all tuples that assign
to
. Hence, hFC5 will delete
from the domain of
. Now in the opposite case, if hFC5
deletes value
from an original variable
it means that
all tuples including that assignment will be removed from the
domains of dual variables that include
and at least one past
variable. In the non-binary representation of the problem, the
assignment of
to
will not have any supporting tuples in
constraints that involve
and at least one past variable.
Therefore, nFC5 will delete
from the domain of
.
Proof:
In Section 3.1 we showed that we can enforce AC
on the HVE of a non-binary CSP with the same worst-case complexity
as GAC in the non-binary representation of the problem. Since
algorithm nFCi enforces GAC on the same part of the problem on
which algorithm hFCi enforces AC, and they visit the same nodes of
the search tree, it follows that the two algorithm have the same
asymptotic cost.
Assuming that is the set of search tree nodes
visited by search algorithm
then the following holds.
Proof:
The proof of 1 is straightforward, see the paper by Bacchus &
van Beek bvb98. Proof of 2-4 is a straightforward
consequence of Proposition 3.1 and Corollary 2
from the paper by Bessiére et al. bmfl99 where the
hierarchy of algorithms nFC0-nFC5 in node visits is given. It is
easy to see that 5 holds since hFC5 applies AC in only a part of
the CSP, while MAC applies it in the whole problem. Therefore, MAC
will prune at least as many values as hFC5 at any given node of
the search tree. Since the same variable and value ordering
heuristics are used, this means that MAC will visit at most the
same number of nodes as hFC5.
Note that in the paper by Bacchus & van Beek bvb98 experimental results show differences between FC in the HVE and FC in the non-binary representation. However, the algorithms compared there were FC+ and nFC0, which are not equivalent. Also, it has been proved that hFC0 can have an exponentially greater cost than nFC0, and vice versa [Bacchus, Chen, van Beek, WalshBacchus et al.2002]. However, these algorithms are not equivalent. As proved in Proposition 3.2, the result of Bacchus et al. bcvbw02 does not hold when comparing equivalent algorithms.
So far we have showed that solving a non-binary CSP directly is in many ways equivalent to solving it using the HVE, assuming that only original variables are instantiated. A natural question is whether there are any search techniques which are inapplicable in the non-binary case, but can be applied in the encoding. The answer is the ability of a search algorithm that operates on the encoding to instantiate dual variables. In the equivalent non-binary representation this would imply instantiating values of more than one variables simultaneously. To implement such an algorithm we would have to modify standard search algorithms and heuristics or devise new ones. On the other hand, in the HVE an algorithm that instantiates dual variables can be easily implemented.
Nikolaos Samaras 2005-11-09