<figure><img src="image_1.png" /></figure>

HAL
open science

# Technical Appendix for Bimodal Depth-First Search for Scalable GAC for AllDifferent

Sulian Le Bozec-Chiffoleau, Charles Prud'Homme, Xavier Lorca, Gilles Simonin, Nicolas Beldiceanu

► To cite this version:

Sulian Le Bozec-Chiffoleau, Charles Prud'Homme, Xavier Lorca, Gilles Simonin, Nicolas Beldiceanu.

Technical Appendix for Bimodal Depth-First Search for Scalable GAC for AllDifferent. IMT Atlan-tique. 2025, 5 p. hal-05062193v2

HAL Id: hal-05062193

https://hal.science/hal-05062193v2

Submitted on 21 Oct 2025

HAL is a multi-disciplinary open access
archive for the deposit and dissemination of sci-
entific research documents, whether they are pub-
lished or not. The documents may come from
teaching and research institutions in France or
abroad, or from public or private research centers.

L'archive ouverte pluridisciplinaire HAL, est
destinée au dépôt et à la diffusion de documents
scientifiques de niveau recherche, publiés ou non,
émanant des établissements d'enseignement et de
recherche français ou étrangers, des laboratoires
publics ou privés.

<figure><img src="image_2.png" /></figure>

Distributed under a Creative Commons Attribution 4.0 International License
# Technical Appendix for Bimodal Depth-First Search for Scalable GAC for AllDifferent

Sulian Le Bozec-Chiffoleau¹, Nicolas Beldiceanu¹, Charles Prud'Homme¹, Gilles Simonin¹ and Xavier Lorca²

¹IMT Atlantique, LS2N, UMR CNRS 6004, F-44307 Nantes, France

²Centre Génie Industriel, IMT Mines Albi, Université de Toulouse, Albi
{sulian.le-bozec-chiffoleau, Nicolas.Beldiceanu, charles.prudhomme, gilles.simonin}@imt-atlantique.fr,
xavier.lorca@mines-albi.fr

## Abstract

This document is the technical appendix for the paper [Le Bozec-Chiffoleau et al., 2025] presented at IJCAI 2025. Section 1 presents the complete proof of Theorem 2. Section 2 details the bimodal algorithm for finding a maximum matching in the variable-value graph. Section 3 details the bimodal algorithm for computing the strongly connected components in the residual graph and finding the variable-value pairs to prune.

## 1 Complete Proof of Theorem 2

In this section we prove the following Theorem:

**Theorem (2).** *Bi-DFS goes through a DFS-forest of $D$ and the time spent exploring a vertex $v \in V$ is:*

* $O(I(v))$ if $f(v) = TRUE$;

* $O(C(v) \times (n - d^{+}(v) + d_{DFS}^{+}(v)))$ if $f(v) = FALSE$.

It is clear that when $f(v) = TRUE$, a) Bi-DFS does not miss any successor of $v$; and b) the time spent exploring $v$ is $O(I(v))$, since we iterate over $N^{+}(v)$, and that the present function of $L$ takes $O(1)$ time.

So it remains to prove the result when $f(v) = FALSE$. For the sake of the proof, we assume that the nodes in the tracking list $L$ are sorted in ascending order, even if it means renumbering them. We consider that $source < v$ for all nodes $v$ different than $source$ and $v < sink$ for all nodes $v$ different than $sink$.

Before continuing with the proof, we introduce some new notations:

* A node $v$ is said to belong to $L$, denoted $v \in L$, if it was initially present in $L$.

* A node $v \in L$ is said to be in the in-list, denoted $v \in L^{in}$, if $remove(v)$ has not been called. Note that $v \in L^{in} \equiv present(v)$.

* A node $v \in L$ is said to be in the out-list, denoted $v \in L^{out}$, if $remove(v)$ has been called. Note that $v \in L^{out} \equiv \neg present(v)$.

* A sequence of removals $R = \langle w_1, ..., w_l \rangle$ is a sequence of calls to $remove(w)$ for $w \in R$.

* A state $S$ of the tracking list $L$ is an assignment of the predecessor $v$. $pred$ and successor $v$. $succ$ of each node $v \in L$ after a sequence of removals $R$.

* A node $v \in L$ is said to be reachable from another node $w \in L$ at a state $S$ if we can reach $v$ by a sequence of calls to $prev$ or $next$ from $w$ at state $S$.

Note that the in-list $L^{in}$ corresponds to the actual doubly linked list, and at any state $S$ we have:

* $prev(v) < v, \forall v \in L \setminus \{source\}$;

* $v < next(v), \forall v \in L \setminus \{sink\}$.

The only function that changes the state of the tracking list is `remove`, and when `remove(v)` is called on a node $v \in L$, it erases the reachability relation from $w$ to $v$ for all nodes $w$ in the in-list at the current state $S$; furthermore, it does not create any new reachability relations.

We first prove the following property on the trackPrev function of the tracking list, which will lead to our complexity result. Note that trackPrev($v$) always exists for any $v \in L$ and at any state, but it may be `source`.

**Lemma 1 (trackPrev Increasing).** *At any state $S$ of the tracking list $L$, and for any $u, v \in L$, if $u \le v$ then trackPrev($u$) $\le$ trackPrev($v$). We say that trackPrev is an increasing function.*

*Proof.* Let us show by recurrence over the sequence of removals $\langle w_1, ..., w_k \rangle$ leading to the state $S_k$ that $\forall (u, v) \in L^2$, $u \le v \implies trackPrev(u) \le trackPrev(v)$ at $S_k$. [Initialisation] The tracking list is initially sorted in ascending order by hypothesis. If there were no call to `remove`, then $trackPrev(v) = v, \forall v \in L$. Thus the property is verified.

[Heredity] Let $S_k$ be the state of $L$ after the sequence of removals $\langle w_1, ..., w_k \rangle$. We suppose that $\forall (u, v) \in L^2$, $u \le v \implies trackPrev(u) \le trackPrev(v)$ in $S_k$. Let $S_{k+1}$ be the state of $L$ after removing $w_{k+1}$ from the state $S_k$. Let $w_{k+1}^p$ (resp. $w_{k+1}^n$) be $prev(w_{k+1})$ (resp. $next(w_{k+1})$) at $S_k$. By definition of the `remove` function, the only change in the digraph of predecessors between $S_k$ and $S_{k+1}$ is that the arc $(w_{k+1}^n, w_{k+1})$ is replaced by the arc $(w_{k+1}^n, w_{k+1}^p)$. However, $w_{k+1}^n$ remains in the in-list, so the only nodes to change their value returned by trackPrev are the nodes $X = \{x \in L : trackPrev(x) = w_{k+1} \text{ in } S_k\}$ and their
new value at $S_{k+1}$ is trackPrev($x$) = $w_{k+1}^p$, since $w_{k+1}$ switches to the out-list. See Figure 1 for an illustration.

<figure><img src="image_3.png" /><figcaption>Figure 1: Illustration of the changes between the predecessors in $S_k$ (up) and $S_{k+1}$ (down) when $w_{k+1}$ is removed from the in-list at $S_k$. And $X$ is the set of nodes whose value returned by trackPrev is changed between $S_k$ and $S_{k+1}$.</figcaption></figure>

Let $u, v \in L$ such that $u \le v$. Thus trackPrev($u$) $\le$ trackPrev($v$) at $S_k$ by recurrence hypothesis.

If $u, v \notin X$, then their value returned by trackPrev did not change, so trackPrev($u$) $\le$ trackPrev($v$) at $S_{k+1}$.

If $u, v \in X$, then trackPrev($u$) = trackPrev($v$) = $w_{k+1}^p$ at $S_{k+1}$, so trackPrev($u$) $\le$ trackPrev($v$) at $S_{k+1}$.

If $u \in X$ and $v \notin X$, then trackPrev($u$) = $w_{k+1}$ at $S_k$, and thus $w_{k+1} \le$ trackPrev($v$) at $S_k$ by recurrence hypothesis. Since $v \notin X$ we have $w_{k+1} \ne$ trackPrev($v$) and then $w_{k+1}^n \le$ trackPrev($v$) at $S_k$ because $w_{k+1}^n$ is the first node on the right of $w_{k+1}$ in the in-list at $S_k$. Then, $v$ did not change its value returned by trackPrev, so $w_{k+1}^n \le$ trackPrev($v$) at $S_{k+1}$. Also, $u \in X$ so trackPrev($u$) = $w_{k+1}^p$ in $S_{k+1}$. As $w_{k+1}^p \le w_{k+1}^n$, we can conclude that trackPrev($u$) $\le$ trackPrev($v$) at $S_{k+1}$.

If $u \notin X$ and $v \in X$, then trackPrev($v$) = $w_{k+1}$ and trackPrev($u$) $\le$ $w_{k+1}$ at $S_k$ by recurrence hypothesis. Furthermore, trackPrev($u$) $\ne$ $w_{k+1}$ so trackPrev($u$) $\le$ $w_{k+1}^p$ at $S_k$ since $w_{k+1}^p$ is the first node on the left of $w_{k+1}$ in the in-list at $S_k$. Then, $u$ has not changed its value returned by trackPrev, so trackPrev($u$) $\le$ $w_{k+1}^p$ at $S_{k+1}$. Furthermore, $v \in X$ so trackPrev($v$) = $w_{k+1}^p$ at $S_{k+1}$. So we can conclude that trackPrev($u$) $\le$ trackPrev($v$) at $S_{k+1}$.

We have shown by recurrence that at any state $S$, reached by a sequence of removals $\langle w_1, ..., w_l \rangle$, trackPrev is an increasing function. $\square$

Now, we focus on Bi-DFS and introduce some other notations. Let $D = (V, A)$ be the input digraph, and $v \in V$ be a vertex. Let $\mathcal{V} = \langle V_0, ..., V_{d_{DFS}^+(v)} \rangle$ be the sequence of all visits of $v$ and let $S = \langle S_0, ..., S_{d_{DFS}^+(v)} \rangle$ be the sequence of corresponding states of the tracking list $L$.

A visit $\mathcal{V}_k$ corresponds to an iteration of the loop line 9, where the tracking list is at a state $S_k$. We distinguish three positions taken by the pointer $p_v$ during $\mathcal{V}_k$:

* $p_{\mathcal{V}_k}^1$: before line 10;

* $p_{\mathcal{V}_k}^2$: after line 10 and before lines 11-12;

* $p_{\mathcal{V}_k}^3$: after lines 11-12.

Note that for two consecutive visits $\mathcal{V}_k$ and $\mathcal{V}_{k+1}$ of $v$, we have $p_{\mathcal{V}_k}^3 = p_{\mathcal{V}_{k+1}}^1$. Also, each one of the three positions may be assigned to source, and if source is traversed by $p_v$ during a visit $\mathcal{V}_k$ of $v$ then it is necessarily assigned to at least $p_{\mathcal{V}_k}^2$. A node $w$ is said to be traversed by $p_v$ in the out-list if there exists a visit $\mathcal{V}_k$ such that $w$ was a position taken by $p_v$ strictly between $p_{\mathcal{V}_k}^1$ and $p_{\mathcal{V}_k}^2$ (e.g. $w_{out}$ in Fig. 2). Similarly, $w$ is said to be traversed by $p_v$ in the in-list if there exists a visit $\mathcal{V}_k$ such that $w$ was a position taken by $p_v$ strictly between $p_{\mathcal{V}_k}^2$ and $p_{\mathcal{V}_k}^3$ (e.g. $w_{in}$ in Fig. 2).

<figure><img src="image_4.png" /><figcaption>Figure 2: Illustration of a node traversed by $p_v$ in the in-list ($w_{in}$) and a node traversed by $p_v$ in the out-list ($w_{out}$) during a visit $\mathcal{V}_k$ of a vertex $v \in V$. The next successor of $v$ to explore is $w_{succ}$.</figcaption></figure>

**Lemma 2.** Let $v \in V$ and $\mathcal{V}_k$ be a visit of $v$ in Bi-DFS, where $L$ is then at state $S_k$. There is no successor of $v$ from source to $p_{\mathcal{V}_k}^3$ in the in-list at $S_k$.

*Proof.* Let us prove it by recurrence over all visits $\mathcal{V}$ of $v$.

[Initialisation] Let $V_0$ be the first visit of $v$; $L$ is then at state $S_0$. We have $p_{V_0}^1 = p_{V_0}^2 = \text{source}$, so $p_v$ moves from source towards right to $p_{V_0}^3$, the last consecutive non-successor of $v$ in the in-list of $L$ at $S_0$. Thus, no successors of $v$ are present in the in-list from source to $p_{V_0}^3$ in the in-list at $S_0$.

[Heredity] Let $\mathcal{V}_k$, with $0 \le k \le d_{DFS}^+(v)$, be a visit of $v$ where $L$ is then at state $S_k$. We suppose that there is no successor of $v$ from source to $p_{\mathcal{V}_k}^3$ in $L^{in}$ at $S_k$.

Let $\mathcal{V}_{k+1}$ be the next visit of $v$, where $L$ is then at state $S_{k+1}$, and let $w$ be a successor of $v$ that is still unvisited during $\mathcal{V}_{k+1}$. Thus, $w$ was also unvisited during $\mathcal{V}_k$, so $p_{\mathcal{V}_k}^3 < w$ by recurrence hypothesis. By definition of trackPrev and because $\text{prev}(x) < x$ for all $x \in L \setminus \{\text{source}\}$ and at any state $S$, we have trackPrev($p_{\mathcal{V}_{k+1}}^3$) < $w$ at $S_{k+1}$. Since $p_{\mathcal{V}_{k+1}}^1 = p_{\mathcal{V}_k}^3$ and $p_{\mathcal{V}_{k+1}}^2 = \text{trackPrev}(p_{\mathcal{V}_{k+1}}^1)$ at $S_{k+1}$, we have $p_{\mathcal{V}_{k+1}}^2 < w$ at $S_{k+1}$. Next, $p_{\mathcal{V}_{k+1}}^3$ is the last consecutive non-successor of $v$ from $p_{\mathcal{V}_{k+1}}^3$ in the in-list at state $S_{k+1}$, so $p_{\mathcal{V}_{k+1}}^3 < w$. Thus, there is no successor of $v$ from source to $p_{\mathcal{V}_{k+1}}^3$ in the in-list at $S_{k+1}$. $\square$

**Lemma 2** ensures that Bi-DFS does not miss any successor of a vertex $v \in V$ when $f(v) = \text{FALSE}$, so the DFS-forest is correct.

**Lemma 3.** Let $v \in V$ and $\mathcal{V}_k$ be a visit of $v$ in Bi-DFS. Every node traversed by $p_v$ from $p_{\mathcal{V}_k}^1$ to $p_{\mathcal{V}_k}^2$ is either source or a non-successor of $v$.

*Proof.* Let $v \in V$ and $\mathcal{V}_k$ be a visit of $v$. If $\mathcal{V}_k$ is the first visit of $v$ ($k = 0$), then $p_{\mathcal{V}_0}^1 = p_{\mathcal{V}_0}^2 = \text{source}$. So, no successor of $v$ is traversed between $p_{\mathcal{V}_0}^1$ and $p_{\mathcal{V}_0}^2$.
We suppose that $\mathcal{V}_k$ is not the first visit of $v$ ($k > 0$). Let $\mathcal{V}_{k-1}$ be the previous visit of $v$. Let $L(k-1)$ denote the set of nodes from source to $p_{\mathcal{V}_{k-1}}^3$ in the in-list at $S_{k-1}$. According to Lemma 2, there is no successor of $v$ in $L(k-1)$. It is not possible to traverse a node outside $L(k-1)$ by calling trackPrev on a node from $L(k-1)$ in any future state $S_{k'}$, with $k' \ge k$, because remove does not create any new reachability relations and $\text{prev}(v) < v$, $\forall v \in L \setminus \{\text{source}\}$. In particular, at state $S_k$, no successor of $v$ is traversed by $p_v$ when calling trackPrev($p_{\mathcal{V}_{k-1}}^3$). Since $p_{\mathcal{V}_k}^1 = p_{\mathcal{V}_{k-1}}^3$ and $p_{\mathcal{V}_k}^2 = \text{trackPrev}(p_{\mathcal{V}_k}^1)$ at $S_k$, we have proven the claimed statement. $\square$

Lemma 2 implies that all nodes traversed by $p_v$ strictly between positions $p^2$ and $p^3$ are non-successors of $v$. So with Lemma 3, all nodes traversed by $p_v$ strictly between positions $p^1 - p^2$ and $p^2 - p^3$ are non-successors of $v$ in the graph $D$.

Now, we prove that every node is traversed by $p_v$ a limited number of times over all visits of $v$.

**Lemma 4.** *Over all visits $\mathcal{V}$ of a vertex $v \in V$, each node is traversed by $p_v$ in the out-list at most once.*

*Proof.* Let $w_{\text{out}}$ be a node traversed by $p_v$ in the out-list. Let $\mathcal{V}_k$ be the first visit during which $w_{\text{out}}$ is traversed in the in-list. By definition, $p_{\mathcal{V}_k}^3$ is in the in-list and $w_{\text{out}}$ is in the out-list at $S_k$. Then, there is no path from $p_{\mathcal{V}_k}^3$ to $w_{\text{out}}$. Since the remove function does not create new reachability relations, there is no way to reach $w_{\text{out}}$ with $p_v$ by the prev and next functions during future visits. Thus, $w_{\text{out}}$ cannot be traversed by $p_v$ in the out-list any more. $\square$

**Lemma 5.** *Over all visits $\mathcal{V}$ of a vertex $v \in V$, each node is traversed by $p_v$ in the in-list at most once.*

*Proof.* Let $w_{\text{in}}$ be a node traversed by $p_v$ in the in-list. Let $\mathcal{V}_k$ be the first visit during which $w_{\text{in}}$ is traversed in the in-list. Then $w_{\text{in}} \le p_{\mathcal{V}_k}^3$. Let $\mathcal{V}_{k+1}$ be the next visit of $v$, where $L$ is at the state $S_{k+1}$.

If $w_{\text{in}} \in L^{\text{out}}$ at $S_{k+1}$, then it cannot be traversed by $p_v$ in the in-list any more.

If $w_{\text{in}} \in L^{\text{in}}$ at $S_{k+1}$, we have trackPrev($w_{\text{in}}) \le$ trackPrev($p_{\mathcal{V}_k}^3$) at $S_{k+1}$ by Lemma 1. Because $p_{\mathcal{V}_k}^3 = p_{\mathcal{V}_{k+1}}^1$ and $p_{\mathcal{V}_{k+1}}^2 = \text{trackPrev}(p_{\mathcal{V}_{k+1}}^1)$, we have $w_{\text{in}} \le p_{\mathcal{V}_{k+1}}^2$. So $w_{\text{in}}$ cannot be traversed by $p_v$ in the in-list during $\mathcal{V}_{k+1}$. Furthermore, we have $w_{\text{in}} \le p_{\mathcal{V}_{k+1}}^3$ by definition of $p_{\mathcal{V}_{k+1}}^3$. So we can proceed with this reasoning for $\mathcal{V}_{k+2}$, and so on. $\square$

Then by Lemmas 4 and 5, the number of nodes traversed by $p_v$ strictly between positions $p^1 - p^2$ and $p^2 - p^3$ is $O(n - d^+(v))$. In addition, at most three different nodes are assigned to the positions $p^1$, $p^2$ or $p^3$ per visit of $v$. The number of visits of $v$ is $d_{\text{BFS}}^+(v) + 1$, so the number of nodes assigned to the positions $p^1$, $p^2$ or $p^3$ is $O(d_{\text{BFS}}^+(v))$. Thus, the total number of nodes traversed by $p_v$ is $O(n - d^+(v) + d_{\text{BFS}}^+(v))$. We can also deduce that the number of times check is called to assess whether a given vertex is a successor of $v$ in the graph is $O(n - d^+(v) + d_{\text{BFS}}^+(v))$ as well.

This proves the complexity result stated in Theorem 2 when $f(v) = \text{FALSE}$.

## 2 Maximum Matching in the Variable-Value Graph

In this section we provide further details about the algorithm that finds a maximum matching in the variable-value graph. The algorithm is called Bi-MM-VVG and the pseudo-code is presented in Algorithm 1. As described in the main paper, it is based on Khun's algorithm for computing a maximum matching in a bipartite graph. Hereafter, we provide the implementation details and data structures management.

**Unvisited Values** To represent the set of unvisited values, we use a bdlL $L$ whose functions remove, present, hasNext, next and reinsert run in $O(1)$ time.

We define another function refill that reinserts all the removed nodes, in reverse removal order. In practice, a stack is used to store the values removed from $L$ and this stack is popped when refill is called.

**Matching** To encode the matching $M$, for each variable $x$ (resp. value $v$), we store its matched value $M(x)$ (resp. variable $M(v)$) if matched, and a dedicated symbol if not. Thus, we are able to check if a given variable or value is matched and if a given variable-value pair belongs to $M$ in $O(1)$ time. This structure takes $O(d)$ space.

**BFS-Tree** To encode the explored BFS-tree, for each value $v$ we store its parent $P(v)$ if it exists, and a dedicated symbol if not. If a variable $x$ other than the root is explored during the BFS, then $x$ is matched and its parent is its matched value $M(x)$, so no need to store the parent of the variables. This structure takes $O(d)$ space.

**Augmenting Path** If an unmatched value $v$ is reached during the BFS, then the path from the root $x$ to this value is an augmenting path. So we run through this path from $v$ to $x$ thanks to $P$ and $M$ and switch the edges belonging to $M$.

**Reset of the Structures** When starting a new BFS, there is no need to reset $P$, since the useful information will be updated during the search. And we refill $L$ instead of reinitialising it, which is done in $O(r)$ time, since at most $r+1$ values are explored during the BFS thanks to the stop condition.

**Complexity** We place ourselves under the same assumptions as in Sect. 4.2 of the main paper. Bi-MM-VVG starts by initialising $L$ and $M$, which takes $O(d)$ time. Then, as in Kuhn's algorithm, it does look for at most $r$ augmenting paths, and each one of them is found with a modified Bi-BFS running in $O(d + \tilde{m})$ time by Corollary 1. However, thanks to an efficient reset of the structures, avoiding reinitialising $P$ and $L$ entirely, the modified Bi-BFS does run in $O(r + \tilde{m})$ time instead.

Thus, Bi-MM-VVG runs in $O(d + r \times (r + \tilde{m}))$ time and uses $O(d)$ space. Also, if the Incremental Matching is used, Bi-MM-VVG takes $O(d + k \times (r + \tilde{m}))$ time, where $k$ is the number of unmatched variables before calling the algorithm.
**Algorithm 1 Bi-MM-VVG**

**Require:** X, D, V and a Boolean function f over X

**Ensure:** Find a maximum matching in the variable-value graph

1: L ← V ▷ bdl of the unvisited values

2: M ← ∅ ▷ The matching is initially empty

3: **for** x ∈ X : x ∉ M **do** ▷ Run a BFS from each unmatched variable to find an augmenting path starting from it

4: v ← AUGMENTINGPATH(x)

5: **if** v = null **then** return null ▷ The constraint cannot be satisfied

6: **while** P(v) ≠ x **do** ▷ Switch the edges of M on the augmenting path

7: vnext ← M(P(v))

8: M(v) ← P(v)

9: M(P(v)) ← v

10: v ← vnext

11: M(v) ← x

12: M(x) ← v

13: return M

14: **procedure** AUGMENTINGPATH(root)

15: Lrefill() ▷ Refill L with the nodes removed during the last iteration

16: Qbfs ← {root} ▷ Queue of the variables to explore

17: **while** Qbfs is not empty do

18: x ← Qbfs .dequeue()

19: **if** f(v) **then** ▷ x has a small domain → use iteration on D ( x )

20: for v ∈ D ( x ) **do

21: if L .present(v) ∧ STOP( x, v ) then return v

22: **else** ▷ x has a large domain → iterate over L and use check on D ( x )

23: v ← L .source;

24: **while** L .hasNext(v) **do**

25: v ← L .next(v)

26: if v ∈ D ( x ) ∧ STOP( x, v ) then return v

27: return null

28: **procedure** STOP(x, v)

29: P(v) ← x ▷ Store the parent of v in the BFS-tree

30: **if** v ∈ M **then** ▷ v ∈ M → The exploration continues

31: L.remove(v)

32: Qbfs .enqueue(M(v))

33: return FALSE

34: **else** ▷ v / ∈ M → An augmenting path has been found

35: return TRUE

3 Strongly Connected Components of the
Residual Graph and Domain Pruning

In this section we provide further details about the algo-
rithm that computes the strongly connected components of
the residual graph and that prunes the pairs linking a variable
and a value that are neither in the matching nor in the same
SCC. The algorithm is called Bi-SCC-RG and the pseudo-
code is presented in Algorithm 2. As described in the main
paper, it uses Tarjan’s algorithm to find the SCCs. In the fol-
lowing, we will specify the implementation details and data
structures management.

**Unvisited Values** To represent the set of unvisited values, we use a tracking list *L* since we need the trackPrev function for the bimodal DFS.

**Matching** The matching encoding is the same as in Bi-BFS.

**Tarjan’s Stack** The stack ST is used to store the unvisited values still unassigned to an SCC, as in Tarjan’s algorithm. ST is of size O(d) and managing it takes O(d) time.

**Low Point and Pre-Visit Order** We use an array to store the low point v .low and the pre-visit order v .pre of each value v . Both arrays are of size O ( d ) .

**Complement SCC** When an SCC is discovered, the PRUNE procedure is called over it. As we may iterate over

the complement of the SCC or assess the presence of a value
within it, we use a bdl compSCC to represent this comple-
ment. It is initialised at the beginning of the algorithm, con-
taining every value of V, and when PRUNE(SCC) is called,
the values in SCC are removed from compSCC, and once
the pruning is done, compSCC is refilled. Thus, this data
structure is of size O(d) and managing it takes O(d) time.

**Algorithm 2 Bi-SCC-RG**

**Require:** X, D, V, a Boolean function f over X and a maximum matching M of the variable-value graph

**Ensure:** Ensure the GAC of the ALLDIFFERENT constraint

1: num ← 1 ▷ The visits start at 1 since t is the first visit

2: S<sub>T</sub> ← ∅ ▷ Tarjan's stack storing the values V only

3: compSCC ← ∅ ▷ Doubly linked list of the complement of the SCC in V

4: L ← V ▷ Tracking list of the unvisited vertices of V

5: **for** v ∈ L : v ∈ M **do** EXPLORE(M(v)) ▷ Start the exploration from t

6: PRUNE(S<sub>T</sub>) ▷ The remaining vertices are in the same SCC as t

7: **procedure** EXPLORE(x)

8: M(x).pre ← num, M(x).low ← num

9: num ← num + 1

10: L.remove(M(x))

11: S<sub>T</sub>.push(M(x))

12: **if** f(v) **then** ▷ x has a small domain → use iteration on D ( x )

13: **for** v ∈ D ( x ) **do**

14: **if** L .present(v) **then** PROCESSNODE(x, v)

15: **else** if v is in S<sub>T</sub> then M(x).low ← min(M(x).low, v.pre)

16: **else** ▷ x has a large domain → iterate over L and use check on D ( x )
      p<sub>x</sub> ← L .source

17: **while** L .hasNext(p<sub>x</sub>) **do** ▷ Explore the childrens of x in the DFS-tree

18: p<sub>x</sub> ← L .trackPrev(p<sub>x</sub>)

19: while L .hasNext(p<sub>x</sub>) ∧ L .next(p<sub>x</sub>) /∈ D ( x ) **do

20: p<sub>x</sub> ← L .next(p<sub>x</sub>)

21: **if** L .hasNext(p<sub>x</sub>) **then** PROCESSNODE(x, L .next(p<sub>x</sub>))

22: **for** v ∈ S<sub>T</sub> **do** ▷ Get the most ancient value of x to update the low point

23: **if** v ∈ D ( x ) ∨ v .pre ≥ M ( x ) .low **then**

24: M(x).low ← min(M(x).low, v.pre)

25: **break**

26: **if** M(x).pre = M(x).low **then** ▷ Detect the root of an SCC

27: SCC ← ∅

28: repeat

29: v ← S<sub>T</sub>.pop()

30: SCC.add(v)

31: **until** v ≠ M(x)

32: PRUNE(SCC)

33: **procedure** PROCESSNODE(x, v)

34: **if** v ∈ M **then**

35: EXPLORE(M(v))

36: M(x).low ← min(M(x).low, v.low)

37: **else** ▷ v leads to t, so we artificially explore it

38: v .pre ← num, v .low ← 0

39: num ← num + 1

40: L.remove(v)

41: S<sub>T</sub>.push(v)

42: M(x).low ← 0

43: **procedure** PRUNE(SCC)

44: **for** v ∈ SCC **do** compSCC.remove(v)

45: **for** v ∈ SCC : v ∈ M **do**

46: u ← M(v)

47: **if** f(v) **then** ▷ x has a small domain → iterate over D ( x )

48: **for** w ∈ D ( x ) : w ∈ compSCC **do** Remove w from D ( x )

49: **else** ▷ x has a large domain → iterate over compSCC

50: **for** w ∈ compSCC : w ∈ D ( x ) **do** Remove w from D ( x )

51: compSCCrefill()

**Complexity** We place ourselves under the same assump-
tions as in Sect. 4.2 of the main paper. Bi-SCC-RG starts by
initialising the different structures in *O*(*d*) time. Then, as in
Tarjan’s algorithm, it performs a DFS on the residual graph.
As we use Bi-DFS, the DFS forest is found in *O*(*d* + *m̃*) time
by Corollary 2. Getting the additional information to update
the low points is also done in $O(d + \tilde{m})$ as explained in the
main paper about $v_{anc}$.

Also, finding inconsistent pairs to prune takes $O(d + \tilde{m} + k)$ time, where $k$ is the number of pairs to prune. The time complexity for removing them from the domains, however, is solver dependent due to the events it might generate. Note that in a whole descent of the search tree explored by the CP solver, the total number of pruned pairs (the sum of the $k$ for each call to the algorithm) is bounded by $r \times d$.

References

[Le Bozec-Chiffoleau et al., 2025] Sulian Le Bozec-Chiffoleau, Nicolas Beldiceanu, Charles Prud'homme, Gilles Simonin, and Xavier Lorca. Bimodal depth-first search for scalable gac for alldifferent. In James Kwok, editor, *Proceedings of the Thirty-Fourth International Joint Conference on Artificial Intelligence, IJCAI-25*, pages 2610–2618. International Joint Conferences on Artificial Intelligence Organization, 8 2025. Main Track.