A Bitwise GAC Algorithm for Alldifferent Constraints

1 Introduction

In constraint programming (CP), many problems can be modeled using the alldifferent constraint. This constraint forces every constrained variable to take distinct values [Lauriere, 1978; Bessiere et al., 2009]. Constraint propagation is a core process for filtering fruitless search space to solve CP problems. At present, there are many filtering algorithms for propagating alldifferent constraint. They can be classified into bound consistency (BC) [L´opez-Ortiz et al., 2003], range consistency (RC) [Leconte, 1996] and generalized arc consistency (GAC) [R´egin, 1994] according to their pruning ability (consistency) from weak to strong. Among them, GAC is more more suitable for solving hard problem instances due to its stronger pruning ability via more complex inference.

The classic GAC filtering algorithm for the alldifferent constraint was presented by R´egin [R´egin, 1994] (hereinafter, called R´egin algorithm). It computes a maximum matching, enumerates strongly connected components (SCCs), and then removes the unmatched edges between independent SCCs (i.e., redundant edges) in the residual graph of the constraint, which is based on a corollary of Berge [Berge, 1973]. The most time-consuming part of the this algorithm is the excavation and enumeration of SCCs, which is commonly solved via the Tarjan algorithm [Tarjan, 1972].

∗Corresponding authors

To improve the performance of the Tarjan algorithm, many studies have been carried out to reduce the number of SCCs that need to be computed. Examples include: 1) SCCsplitting [Gent et al., 2008], which only computes an SCC where the domain of its variable has been changed during the backtracking search, thus reducing the range of variables required to compute SCCs. 2) Bitwise operation [Van Kessel and Quimper, 2012], which employs a bitwise approach to accelerate propagation based on the WordRam model and have always been an important means of accelerating consistency algorithms [Lecoutre and Vion, 2008; Wang et al., 2016; Demeulenaere et al., 2016; Li et al., 2021]. 3) Matching optimization [Zhang et al., 2018], which proves that redundant edges can be divided into two classes, one of them can be removed directly without computing the corresponding SCCs. 4) Early detection [Zhang et al., 2020], which avoids the computation of the unimportant edges whose deletion will not split the current SCCs.

However, all of the optimizations mentioned above involve excavating all strongly connected components (SCCs) and maintaining corresponding information using complex data structures such as queues, stacks, traversal orders, and SCC IDs for each node. The GAC algorithm is embedded in the entire backtracking search solution framework and is invoked iteratively, frequently updating and resetting these complex data structures. This causes a significant overhead in both execution time and memory space. Furthermore, due to the complexity of the data structures, it is difficult to integrate different optimization schemes in a synergistic way, resulting in lower overall efficiency.

In fact, our analysis shows that the essential task of the GAC algorithm is to delete inconsistent nodes. Therefore, it only cares whether a node in the graph is in an SCC or not, rather than which SCC it belongs to. Based on this key observation, we transform a 'which' problem into a 'yesor-no' one. This enables us to propose a bitwise GAC algorithm called Alldiff bit . Alldiff bit employs complete bitwise data structures and performs the 'yes-or-no' problem via simple bitwise 'OR' operations during the traversal of the bit-adjacency matrix of the graph model. Additionally, the bitwise data structures and operations also enable Alldiff bit to easily incorporate existing optimizations, including: 1) SCC-Splitting by improving the SCC partition representation mechanism; 2) matching optimization via bit-BFS of adjacency bit-matrix; and 3) early detection by prioritizing the checking of the connectivity of deleted edges. These existing optimizations can work organically when integrated into Alldiff bit .

Our experiments on large numbers of constraint problems (CPs) show that Alldiff bit is both efficient and stable. Compared to the GAC algorithms implemented by state-of-the-art CP solver [Prud'homme et al., 2017], Alldiff bit achieves an average performance speedup of 60.65% per group across 18 series instances. We believe that Alldiff bit is a powerful contender against existing algorithms.

2 Background and Preliminaries

A constraint satisfaction problem (CSP) P is a triple P = ⟨X , D, C⟩, in which X is a set of n variables X = {x1, x2, ..., xn}, D is a set of domains D = {D(x1), D(x2), ..., D(xn)}, where D(xi) is a finite set of possible values for variable xi, and C is a set of e constraints C = {c1, c2, ..., ce}. A constraint c restricts an ordered set of variables X(c) = {x1, x2, ..., xr}, and also restricts a subset of the Cartesian product D(x1) × D(x2) × ... × D(xr), which specifies the allowed combinations of values for X(c). The domain of c is the union of domain, which is denoted by D(c) = ⋃x∈X(c) D(x). In addition, we use Bc(a) to denote the set of variables in X(c) whose domain contains a (i.e., Bc(a) = {x | x ∈ X(c), a ∈ D(x)}). A solution to a CSP is an assignment of a value to each variable, so that all the constraints are satisfied.

Definition 1 (Generalized Arc Consistency, GAC). Given a constraint network P = ⟨X , D, C⟩:

• A constraint c is GAC iff ∀ x ∈ X(c) and ∀ a ∈ D(x), there exists a support for (x, a) on c.
• A constraint network P is GAC iff all constraints in C are GAC.

An alldifferent constraint c: {x1, ..., xr} (r > 1) is an rarity constraint that ensures that the values assigned to constrained variables are all distinct. The GAC algorithms are based on Berge's graph theory, particularly on maximum matching and strongly connected components. A matching is a set of edges that do not have common vertices. In this paper, if variable x is matched to value a, it can be written as x = M(a) and a = M(x), otherwise M(a) = ⊥ and M(x) = ⊥. A maximum matching is one that has maximum cardinality. If a node is connected with a matched edge, it is called a matched node; otherwise, it is called a free node. An alternating path is a path whose edges alternate between matched and unmatched nodes. An augmenting path is a path whose starting and ending nodes are both free nodes.

Definition 2 (Residual Graph). The residual digraph is defined as R = ⟨VR, ER⟩, where VR = X(c) ∪ D(c) ∪ {t}, t is a sink node linked to D(c), ER = EM ∪ EU ∪ Et1 ∪ Et2 . Specifically, the matching edges EM connect variables to their respective matching values: EM = {x ↦→ a | x ∈ X(c), a = M(x)}. The unmatched edges EU connect values to their respective unmatching variables: EU = {a ↦→ x | a ∈ D(c), x ∈ Bc(a) \ {M(a)}}. The edges in Et1 connect matching value nodes to t: Et1 = {a ↦→ t | M(a) ∈ X(c)}. The edges in Et2 connect t to unmatching value nodes (i.e., free nodes): Et2 = {t ↦→ a | M(a) /∈ X(c)}.

Each edge e ∈ EM ∪EU represents a variable-value pair in constraint c. A redundant edge is one that does not appear in any maximum matching. An allowed edge is one belonging to some but not all maximum matchings. A node is allowed, iff, for an arbitrary maximum matching M, it can be reached by an even alternating path that begins at a free node [Zhang et al., 2017]. The set of variable nodes in alternating paths is denoted by Γ , and its value nodes set is denoted by A.

Definition 3 (Redundant Edge). For an arbitrary maximum matching, an unmatching edge ea↦→x is redundant iff (1) x ∈ Γ and a ∈ D(c) - A, or (2) x ∈ X(c) - Γ , a ∈ D(c) - A and ea↦→x does not belong to any alternating cycle [Zhang et al., 2018].

In this paper, we call these two type of redundant edges as "type I" and "type II" redundant edges, respectively. Zhang18 algorithm (as shown in Figure 1(b)) develops the graph theory of R´egin algorithm (as shown in Figure 1(a)) by removing type I redundant edge without computing SCCs. For a residual graph R = ⟨VR,ER⟩ and a set of (deleted) edges DE = e1, e2, ..., ek, where ei ∈ EM ∪ EU,(1 ≤ i ≤ k), R′ = ⟨VR,ER \ DE⟩ is consistent, iff, for every start-end node pair (xi, yi) of ei in DE, there exists at least two arcdisjoint alternating paths connecting xi and yi [Zhang et al., 2020]. These edges are called unimportant edges. To be specific, Zhang18's algorithm develops R´egin's algorithm by adding the following steps 3 and 4: (1) Find a maximum matching M from variables to distinct values. If it fails 1 , the constraint is inconsistent. (2) Construct the residual graph R (see Definition 2). (3) Find all alternating paths from all free nodes in R, and put the variable (resp. value) nodes of the alternating paths into Γ (resp. A). (4) Remove all type I redundant edges without finding SCCs. (5) Find all SCCs of R and remove all redundant edges. If R does not have free nodes, steps 3 and 4 will not be executed, and this algorithm will be degraded to R´egin's algorithm. Zhang20's algorithm improves step 5 by detecting whether each deleted edge e is surrounded by a cycle during the DFS for finding SCCs. If so, it is an unimportant edge. If all edges are unimportant, this propagation can be exited early.

3 The AllDiff bit Algorithm

In this section, we propose the Alldiff bit algorithm. Instead of enumerating SCCs to check whether the variable values satisfy GAC, Alldiff bit directly checks their connectivity in the adjacency bit-matrix of the graph. This simplifies the data structures and comprehensively bit-vectorizes them. Furthermore, it enables the synergistic integration of existing optimizations. Specifically, Alldiff bit first reduces the graph model by merging matched nodes and uses the adjacency bit-matrix to represent the merged graph (as depicted in Figure 1(c) and Table 1). Then, it checks the consistency of each variable-value by checking the connectivity of its corresponding edge in a bit-BFS manner. Furthermore, we extend Alldiff bit to accommodate various existing improvements. For SCC Splitting [Gent et al., 2008], our algorithm gives priority to checking the edges that are mutually connected by using a new edge checking order. This order ensures that a complete traversal of an entire SCC is performed when the traversal stops. For matching optimization [Zhang et al., 2018], we also bitwise vectorize the A and Γ sets and quickly calculate them by bit-BFS. For early detection [Zhang et al., 2020], we preferentially traverse the deleted edges, and the propagation can quit early if they all pass the connectivity check.

Bitwise representation of merged graph. When computing SCCs of the reduced residual graph R, the existing algorithms alternately traverse matching and unmatching edges. To eliminate matching edges, the variables and values that are matched can be merged. This results in a merged node that inherits all incoming edges of the original variable node and all outgoing edges of its matched value node. As a result, we obtain a smaller directed graph G = ⟨V, E⟩, where V = X(c), E = {x ↦→ y | x ∈ X(c), y ∈ Bc(M(x)) \ {x}} (see Figure 1(c)). This reduction helps to decrease the size and order of the graph. Based on the above, we introduce the adjacency bit-matrix G to represent the merged graph 2 . If node x can reach node y in the merged graph, then G[x][y] = 1b, otherwise G[x][y] = 0b. The adjacency bit-matrix GF represents the frontier nodes to be expanded during BFS. If x needs to extend y then GF [x][y] = 1b, otherwise GF [x][y] = 0b. If a value (x, a) is valid (i.e., a ∈ D(x) and x ∈ Bc(a)), then B[a][x] = 1b, otherwise B[a][x] = 0b. Table 1 gives the bitwise representation of Figure 1(c). Method mergeMatchedNodes of algorithm 1 initializes the above fields.

1 This means that there is a variable node without a matching value node.

Proposition 1. (Correctness of Merging Nodes) After merging matched nodes, a reduced residual graph R = ⟨VR, ER⟩ can be transformed to a directed graph G = ⟨V,E⟩, where V = X(c), E = {x ↦→ y | x ∈ X(c), y ∈ Bc(M(x)) \{x}}.

Proof. For reduced residual graph R of an alldifferent constraint c, the matching is a mapping from X(c) to D(c), denoted as f: X(c) ↦→ D(c), and the unmatching is a mapping from D(c) to X(c), denoted as g: D(c) ↦→ X(c). Trivially, f ̸= g. We combine f and g to eliminate V to get the composite mapping g ◦ f : X(c) ↦→ X(c), which means x ∈ X(c) gets its neighbor from variables whose domain contains the matching of x. Hence, it corresponds to the directed graph G = ⟨V,E⟩, V = X(c), E = g ◦ f = {x ↦→ y | x ∈ X(c), y ∈ Bc(M(x)) \ {x}}.

Check the connectivity of edges. Our algorithm differs from Tarjan's algorithm in that it does not compute all SCCs at once. Instead, it is driven by the connectivity of edges in the reduced graph, and only checks variable values of an SCC when needed. As described in Definition 3, checking whether an unmatching edge ea↦→x is redundant is equivalent to checking whether eM(a)↦→x belongs to any alternating cycle. If there exists a path from x to M(a), then the path x ↦→M(a) and edge eM(a)↦→x can form a cycle. For a valid variable value (x, a), its corresponding node M(a) can be connected to node x. Checking whether it is in an SCC requires checking the connectivity from node x to node M(a). Method check(x,a) in Algorithm 1 checks the connectivity

2 All of the bitwise data structures are represented in bold font in this paper.

Algorithm 1: FIND SCCS

Input: s: current SCC; DE: deleted edges in s 1 Method findSCCs(s, DE): 2 mergeMatchedNodes(s) 3 if ¬ matchingOpt(s) ∧ ¬ earlyDetect(s, DE) then 4 filterDomains(s) 5 Method mergeMatchedNodes(s): 6 Initial B s.t. B[a][x] = 1b iff x ∈ Bc(a) 7 foreach matched variable x ∈ s do 8 G[x] ←B[M(x)] 9 G[x][x] ← 0b 10 GF [x] ←G[x] 11 Method matchingOpt(s): 12 Γ ← 0; A← ∅ 13 foreach free node a do 14 Γ ← Γ |B[a]; Γ F ← Γ F |B[a]; A[a] ← 1b 15 while x ∈ s s.t. ΓF [x] = 1b do 16 ΓF ←ΓF | (B[M(x)]& ∼ Γ); ΓF [x] ← 0b 17 Γ ← Γ | B[M(x)]; A[M(x)] ← 1b 18 Remove Type I redundant edges 19 Remove Γ from s; add Γ as an independent SCC 20 return |s| = |Γ | 21 Method earlyDetect(s,DE): 22 foreach (x, a) ∈ DE do 23 if ¬(check(x, a)∧check(M(a),M(x))) then 24 return false 25 return true 26 Method check(x, a): 27 while y ∈ s s.t. GF [x][y] = 1b do 28 GF [x] ←GF [x] | (G[y]& ∼G[x]) 29 GF [x][y] ← 0b 30 G[x] ←G[x] | G[y] 31 if G[x][M(a)] = 1b then 32 return true; 33 return false 34 Method filterDomains(s): 35 su ← s; s′ ← s; sc ← ∅; sm ← ∅ 36 while s′ ̸= ∅ do 37 pop x′ from s′ 38 if sc ̸= ∅ then 39 add sc as a independent SCC 40 sc = {x′ }; su = (su ∪ sm) \ {x′ }; sm = ∅ 41 foreach x ∈ sc do 42 foreach unmatched value a ∈ D(x) do 43 if M(a) ∈ su then 44 if check(x, a) then 45 move M(a) to s′ and sc 46 else 47 remove a from D(x); move M(a) to sm 48 else if M(a) ∈ sm ∨M(a) /∈ s then 49 remove a from D(x);

of node x to node a. It uses the bit-BFS method proposed in [Cheriyan and Mehlhorn, 1996]. The method takes an extendable node y of GF [x] (line 27). The connectable nodes of y that have not been visited by x (i.e., G[y]& ∼ G[x]) are added to the frontier GF [x] by bitwise operations (line 28), and then GF [x] clears the bit of extended node y (line 29). Next, all the nodes connected to x are recorded by bitwise anding G[y] to G[x] (line 30). The method continues traversing and returns true until G[x][M(a)] = 1b is detected, which means that x can connect to M(a). If G[x][M(a)] = 0b when the BFS is completed, the method returns false. All search information is stored in G[x] and GF [x] for future calls.

The aforementioned improvements are the core idea of Alldiff bit . Additionally, our algorithm is highly scalable and can be easily extended and integrated to optimize all the related improvements for alldifferent constraints. We will describe these implementations in the following subsections.

Integration of SCC splitting. Since our algorithmdoes not directly compute SCCs, the mechanism of SCC Splitting in Gent algorithm needs to be slightly modified. Suppose s is the current variables partition that needs to compute SCC. We divide it into three subsets: connected, unknown and moved, denoted by sc, su and sm, respectively, where sc denotes the set of nodes (i.e., variables) that are explicitly in the same SCC, sm denotes the set of nodes that are explicitly not in current SCC with sc, the rest of the nodes which need to be checked the connectivity are stored in su, and s′ is a queue of variables to be extended during iteration in method filterDomains. This method initializes su and s′ to s. It also resets both sc and sm to empty set, indicating that the connectivity of all nodes is initially unknown. The method then pushes them into queue s′ to wait for checking if they are in SCC. The outer loop (line 36) iteratively checks the connectivity of each node in s′ . The main loop (lines 41-49) gives priority to traversing the connected node in sc. It moves newly connected nodes to sc and unconnected ones to sm. Since new connected nodes may be added to sc, the main loop continues until all nodes of the current SCC have been fully explored. Once the traversal of the main loop is completed, sc is transformed independently into a new SCC (line 39). This results in the previously traversed sm becoming outdated and reclassified into su (line 40). Then, the outer loop pops a new node x′ from s′ to continue the traversal (line 37). Lines 43 to 49 are the core part for checking connectivity. For a variablevalue pair (x, a), the method check(x,a) is invoked only if M(a) ∈ su. If M(a) is in the moved sub-partition or does not belong to the current SCC s, it can be deleted directly (lines 48-49).

Integration of matching optimizing. Differing from DFS in Zhang18 algorithm, method matchingOpt(s) perform a traversal starting from free nodes in bit-BFS fashion. As G and GF , the method uses Γ to denoted the set Γ and ΓF to denoted the set of nodes which needs to be traversed. The procedure for computing set Γ and A similarly to computing SCC as described above. It first iterates over each free node to initialize Γ and ΓF by bitwise or, and adds the free nodes to A in lines 13 to 14. Then, it iteratively traverses each node x from ΓF and adds new untraversed nodes of x (i.e., B[M(x)]& ∼ Γ) to ΓF for further traversal. Next, the method extends Γ and clears the newly traversed node x at statement ΓF [x] ← 0b. Please note that the same traversal method is used to extend G and GF in method check(x, a). Finally, M(x) is added to A at statement A[M(x)] ← 1b (lines 15-17). After bit-BFS, the type I redundant edges is directly delete in line 18. Γ is removed from current SCC s and added as a independent SCC. According to [Zhang et al., 2018], if Γ = s, all variables in s do not need to be filtered, method filterDomains can be skipped directly.

Integration of early detection. Our algorithm uses valuedriven SCC detection, which makes it more naturally compatible with early detection than the Zhang20 algorithm. As described in [Zhang et al., 2020], the earlyDetect method checks whether the two paths from x to M(a) and M(a) to x exist (line 23) to detect whether a deleted edge (x, a) is an unimportant edge. If (x, a) is in the current SCC s, then ¬(check(x, a)∧ check(M(a),M(x))) returns true, indicating that (x, a) is an unimportant edge. If a deletion is detected to be important, the algorithm skips the detection and directly calls the filterDomains(s) method. Conversely, if all edges in DE pass the detection, the call of method filterDomains can be skipped.

In summary, the algorithm executes the filterDomains method only if the matchingOpt and earlyDetect methods pass, indicating that there are still variables to be filtered. Otherwise, the method is skipped (lines 3-4).

Proposition 2. (Soundness) If (x, a) corresponds to a type II redundant edge on the reduced graph, it cannot pass method check(x, a).

Proof. Suppose (x, a) corresponds to a type II redundant edges. So its corresponding edge is eM(a)↦→x. If it can pass method check(x, a). i.e., we get G[x][M(a)] = 1b after BFS at line 41. This means that there exists a path from x to M(a), and this path and eM(a)↦→x make up a alternating cycle. eM(a)↦→x clearly does not satisfy Definition 3, i.e., (x, a) is not a type II redundant edge. This contradicts the hypothesis, so check(x, a) returns false (i.e., G[x][M(a)] = 0b) if (x, a) is a type II redundant edge.

Proposition 3. (Completeness) All redundant edges can be removed in filterDomains().

Proof. All unmatched nodes need to iteratively check whether they are redundant edges at lines 24-25 in Algorithm 1. We know from [Zhang et al., 2018] that Γ and A are correctly partitioned after matching optimizing. Hence all type I redundant edges can be removed at line 14 in Algorithm 1. And all the type II redundant edges can be removed at line 37 and line 39 in Algorithm 1. Therefore, all redundant edges can be removed in findSCC().

Proposition 4. (Correctness) Our filtering algorithm is correct on the reduced graph.

Proof. Correctness immediately follows fromPropositions 1, 2 and 3.

Complexity. In this paper, we use a bit version FFBFS [Ford and Fulkerson, 1956; Van Kessel and Quimper, 2012] to perform incremental matching in O(km), where k and m are the numbers of unmatched and total edges in the variable-value graph, respectively. Although our lazycomputing SCCs mechanism does not change algorithm's complexity, it significantly reduces the size of the graph after node merging. The time complexity of computing SCCs via R´egin's algorithm is O(|VR|+|ER|) = O(r+2d+1+dr) = O(dr). That of Zhang18's algorithm is O(|VR| + |ER|) = O(r + d + dr) = O(dr), and it can be reduced to O(r2 ) with matching optimizing. And that of our algorithm is O(|V | + |E|) = O(r + r2 ) = O(r2 ). Apparently, for alldifferent constraint, we have r ≤ d, so our algorithm has a lower time complexity than R´egin's algorithm. Although our algorithm has the same complexity as Zhang18's algorithm, it requires less computational cost in practice due to the reduced digraph. In addition, using bit representation can further reduce memory consumption.

4 Experimental Results

We evaluated the performance of our algorithm by comparing it to backtracking search algorithm that embed arc consistency algorithms: Gent, WordRam, Zhang18 and Zhang20. 3 WordRam algorithm uses bitwise FF-BFS and bitwise Tarjan algorithm to compute maximum matching and SCCs, respectively. The default incremental matching algorithm for GAC algorithms are FF-BFS for non bit algorithms and bit FFBFS for WordRam and our algorithm. We evaluate the performance of these embedded GAC algorithms by comparing search resolution algorithms. To conduct a comprehensive evaluation, we used various alldifferent CP instances from the XCSP3 website [Boussemart et al., 2016] 4 . All series names are listed in Table 2 and we tested over 800 instances. Our experiments were conducted on a PC with an AMD Ryzen 9 7950X CPU @ 4.5GHz, 32 GB RAM, and 64-bit Windows 11. The timeout was set to 1200 seconds for each instance. The number of non-timeout instances (and total instances) for each series is given below the series name after "#=". All the algorithms were implemented in the Java-based CP solver, Choco [Prud'homme et al., 2017] 5 using OpenJDK 19. To ensure fairness, We used binary branching search with DOM [Dechter and Meiri, 1994] as the variable ordering heuristic, and "min value" as the value ordering heuristic. This ensured that all algorithms generated the same shape of search trees when solving, avoiding interference with experimental results due to differences in their shapes. For a straightforward impression of the algorithms' efficacy, we first compared the solving time per series. While most CPs contain alldifferent constraints, they may also contain other types of constraints. To provide a microscopic observation, we also compared the filtering time for solved instances. Additionally, we presented the proportion of different improvement points in the propagation process.

3 The source code and dataset are available at https://github.com/leezear2022/alldiff-choco. Our testing includes many academic and practical instances that require hashing of domains during propagation. However, this may decrease the efficiency of WordRAM and Alldiff bit .

4 http://xcsp.org/

5 https://choco-solver.org/

Table 2 presents the efficiency of the algorithm for each instance. Instances that timed out during testing are excluded from statistical averaging. The average CPU time (in seconds) for solving the problem and computing SCCs for the remaining instances are presented in the "S" and "F" rows, respectively. Gent serves as the baseline algorithm in Table 2. The results of Alldiff bit with a 50% to 100% increase in efficiency are underlined, while those above 100% are bolded. We first compare the average solving time of the instances. Our algorithm solves the instances in the shortest time on all 18 groups of instances. This is because our algorithm integrates and improves all the improvement points. In particular, our algorithm achieves a lead of 50% to 100% on 7 series and even more than 100% on 3 series. In short, our algorithm's solving efficiency is improved by an average of 60.65% across all series. It is worth noting that our algorithm also achieves the best results in instances where Zhang18 or Zhang20 algorithm are better, such as CryptoPuzzle and GolombRuler for Zhang18 algorithm, and Kakuro, Openstacks, and QuadraticAssignment for Zhang20 algorithm. This is due to our algorithm's integration and improvement of these enhancements. We continue to compare the time it takes for each algorithm to compute SCCs. To better analyze the improvements, we are blocking out other distracting factors, such as computation of matching, propagation of other types of constraints, search algorithms, etc. Similar to the trend of solving time, our algorithm is the most efficient in calculating SCCs. Moreover, it achieves a higher acceleration ratio compared to the other algorithms. In fact, our algorithm won and achieved more than 100% acceleration in 16 series of instances, and even more than 5 times acceleration in 2

series.

To compare the performance of the core idea presented in this paper with our integration algorithm - Alldiff bit - we implemented a simple algorithm "base" with bitwise representation and "Check the Connectivity of Edges", which we provisionally refer to as "base." Figure 2 shows a scatter plot that allows us to compare the efficiency of three bitwise GAC algorithms when executing the method findSCC for each instance. The vertical and horizontal axes represent the CPU time (in seconds) used by Alldiff bit and other bitwise GAC algorithms to compute SCCs, respectively. In general, as the time increases, most of the dots are located at the bottom right of the diagonal. This indicates that Alldiff bit is more efficient for easy to hard instances. It is worth noting that the main difference between the two bit-based algorithms, WordRam and Alldiff bit , is the traversal method.

The Wordram algorithm uses bit-DFS, which requires maintaining a bit vector during traversal to record the nodes to be extended at each propagation. Due to the need for complex data structures to enumerate SCCs, they are difficult to vectorize, which increases maintenance costs. In contrast, our algorithm only retains G and GF for bit-BFS since no prior enumeration of SCCs is required. As a result, their maintenance is lightweight, which significantly improves the efficiency of the overall method execution. As Alldiff bit is an integrated algorithm, we observe that the dots of the base algorithm cluster on an "oblique line" below the diagonal. This is because Alldiff bit is a direct improvement of the base algorithm, implying that our algorithm has a more stable improvement. Nevertheless, the base algorithm is more efficient than the WordRam algorithm. In summary, the solution efficiency of Alldiff bit improves by an average of 60.65% per group across all series.

Finally, in order to observe the impact of the various improvement points, we counted the proportion of their occurrence in computing SCCs (referred to the propagation type) during the solution process of the solved instances. If the type I (resp. II) redundant edges are deleted, we call it the type I (resp. II) deletion, and denote it as "P1" (resp. "P2"). And if it is skipped due to early detection, it is denoted as "Skip," otherwise, it is denoted as "None." As shown in Figure 3, for series CryptoPuzzle, GolumbRuler, and Kakuro, the type I deletion occupies a particular proportion. This is consistent with the results in Table 2, which show that the Zhang18 has better performance on these series compared to the baseline algorithm. While for other series, the type II deletion still accounts for a large proportion. This is because if there are no free nodes, no match optimization is performed on line 13 of algorithm 1. For other series, however, the type II deletion still accounts for a large proportion. This is because if there are no free nodes, no match optimization is performed on line 13 of algorithm 1. The early detection identifies a large amount of redundant propagation. While this may incur additional overhead in some degree of presentation, it substantially reduces the number of computed SCCs on many series instances. Therefore, considering the overhead, Zhang20 performs better on some series with a higher proportion of partial early detection than the baseline algorithm.

5 Conclusion

In this paper, we present Alldiff bit , an improved GAC filtering algorithm for alldifferent constraints. Our main idea is based on the observation that it is unnecessary to enumerate strongly connected components (SCCs) in order to determine whether a variable-value satisfies GAC. Instead, only the edges of the graph model need to be checked for strong connectivity. This allows the data structures used by graph traversal to be simplified as fully bit vectorized, thus substantially reducing the overhead of graph traversal. Additionally, Alldiff bit integrates the SCC splitting of Gent, the matching optimization of Zhang18, and the early detection method of Zhang20 algorithm, making it strongly extensible. Our algorithm further improves upon these algorithms. Extensive experiments show that Alldiff bit significantly outperforms existing GAC algorithms. All of these results illustrate that Alldiff bit completes a staged integration and optimization of the GAC algorithm for alldifferent constraints.

Acknowledgments

The authors would like to thank the anonymous reviewers for their helpful comments. This work is supported by the NSF of Hunan ProvinceNo.2022JJ10066, theNational Nature Science Foundation of China No.62272477 and 62276060.