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