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

HAL
open science

# Biclique Factorisation of Explanations for a Sparser Implication Graph in Lazy Clause Generation

Sulian Le Bozec-Chiffoleau, Charles Prud'Homme

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

## To cite this version:

Sulian Le Bozec-Chiffoleau, Charles Prud'Homme. Biclique Factorisation of Explanations for a Sparser Implication Graph in Lazy Clause Generation. IMT ATLANTIQUE; LS2N. 2026. hal-05537266

HAL Id: hal-05537266

https://hal.science/hal-05537266v1

Submitted on 5 Mar 2026

HAL is a multi-disciplinary open access archive for the deposit and dissemination of scientific research documents, whether they are published 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_3.png" /></figure>

Distributed under a Creative Commons CC BY 4.0 - Attribution - International License
# Biclique Factorisation of Explanations for a Sparser Implication Graph in Lazy Clause Generation

Sulian Le Bozec-Chiffoleau<fnref n="1" />

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

Charles Prud'homme

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

## Abstract

In the context of lazy clause generation, we propose factorising bicliques in the implication graph to reduce the associated overhead. This process consists of (1) identifying a set *P* of prunings that share a common subset *L* of literals in their reason, (2) introducing an artificial literal *f*, called a factor, and 3) adding the arcs (*L* × *f*) ∪ (*f* × *P*) to the implication graph instead of the arcs *L* × *P*. When *P* and *L* are large, biclique factorisation significantly reduces the number of generated arcs. This technique offers two main advantages: (1) faster explanation generation and (2) a sparser implication graph, leading to more efficient conflict analysis and reduced memory usage. We provide tight worst-case bounds on both the time complexity of explanation generation and the maximum number of generated arcs for two global constraints: **ALLDIFFERENT** and **CUMULATIVE**. Experiments were also conducted to evaluate and validate our approach.

**2012 ACM Subject Classification** Theory of computation → Constraint and logic programming

**Keywords and phrases** lazy clause generation, explanations, implication graph, graph compression, biclique factorisation, global constraint, alldifferent, cumulative

**Funding** Sulian Le Bozec-Chiffoleau: This publication has emanated from research conducted with the financial support of the Futur & Ruptures program co-granted by IMT, Institut Carnot TSN, Institut Carnot M.I.N.E.S. and Fondation Mines-Télécom.

**Acknowledgements** The authors thank Nicolas Beldiceanu, Xavier Lorca and Gilles Simonin for their advices regarding this work.

## 1 Introduction

Designing efficient Constraint Programming (CP) [35] solvers is often a matter of finding an optimal trade-off between inference time and inference strength. Lazy Clause Generation (LCG) [30] is one inference technique which is no exception to this rule. LCG is a hybrid solving framework that combines CP with clause learning from *boolean satisfiability (SAT)* [9]. It extends classical propagation by recording explanations for domain reductions (prunings) and translating them into clauses that are learned during conflict analysis. This integration enables the solver to benefit from powerful global constraints while exploiting nogood learning and non-chronological backtracking, significantly improving performance on combinatorial problems. However, LCG may incur a non-negligible overhead due to literal creation, explanation generation, and implication graph traversal during conflict analysis. This has motivated the introduction of *lazy explanations* [20], which defer explanation generation until conflict analysis, thereby avoiding the computation of explanations that are not useful for clause learning.

In this paper, we propose another method to reduce this overhead: *biclique factorisation*. This idea stems from the observation that many prunings may share a common subset

<footnote n="1">¹ corresponding author</footnote>
of literals in their reasons, leading to a high worst-case time complexity for explanation generation—especially for large global constraints—as well as to a locally, and potentially globally, very dense implication graph. Such density slows down conflict analysis and increases the memory footprint. Biclique factorisation originates from a graph compression technique and consists of (1) identifying a set *P* of prunings that share a common subset *L* of literals in their reason, (2) introducing an artificial literal *f*, called a factor, and (3) adding the arcs (*L* × *f*) ∪ (*f* × *P*) to the implication graph instead of the arcs *L* × *P*. This significantly reduces the number of generated arcs while preserving reachability relationships. This technique offers two main advantages: (1) faster explanation generation and (2) a sparser implication graph, leading to more efficient conflict analysis and reduced memory usage.

We implement biclique factorisation for two core global constraints: **ALLDIFFERENT** [34] and **CUMULATIVE** [1]. We establish tight worst-case bounds on both the time complexity of explanation generation and the maximum number of generated arcs. Experiments are conducted using **Choco-solver** [33] to evaluate and validate the proposed approach. In particular, we highlight the differences in the number of generated arcs in practice with and without biclique factorisation, and show that memory requirements can be significantly affected. Although explanation generation is usually not the main bottleneck in resolution and therefore does not have a major impact on overall performance, we observed noticeable differences in total computation time in some cases.

Section 2 introduces the basics of constraint programming and lazy clause generation. Section 3 presents the general principle of biclique factorisation of explanations. Sections 4 and 5 detail how to efficiently factorise explanations for **ALLDIFFERENT** and **CUMULATIVE**. Finally, Section 6 reports the experimental evaluation conducted with **Choco-solver**.

# 2 Preliminaries

## 2.1 Constraint Programming

*Constraint Programming* (CP) [35] is a paradigm for solving combinatorial problems by modelling them as a set of variables with finite domains subject to constraints, and by combining systematic search with inference mechanisms to efficiently explore the solution space. The modern constraint solver architectures rely on a backtracking search that incrementally assigns values to variables, interleaved with constraint propagation [8] procedures that enforce local consistency properties in order to prune infeasible values from variable domains. Among these, *generalised arc consistency* (GAC) ensures that, for a given constraint, every value in the domain of each variable in its scope participates in at least one assignment satisfying the constraint. *Bound consistency* (BC) enforces that, when domains are considered as intervals, the lower and upper bounds of each variable participate in at least one assignment satisfying the constraint. An algorithm that prunes infeasible variable-value pairs for a given constraint in order to maintain (or approximate) a local consistency is called a *propagator* for that constraint. Constraint propagation consists in iteratively calling the propagators until the fix point is reached, i.e. no more pruning can be done by the propagators. This reduces the search space before and during search while preserving completeness. A central design issue in CP is the trade-off between the strength of inference—i.e., the amount of pruning achieved (measured by the level of consistency enforced)—and its computational cost (measured by the time complexity), often referred to as the inference time/strength trade-off. Stronger propagation can substantially reduce the size of the search tree but may incur higher per-node overhead, whereas weaker propagation is cheaper but may lead to more extensive search.
## 2.2 Lazy Clause Generation

Lazy clause generation (LCG) [17, 30] is a hybrid technique combining the power of CP and boolean satisfiability (SAT) solvers. This is an adaptation to CP of conflict-driven clause learning (CDCL) in SAT [9]. The principle is to encode a boolean variant of the domains, made of equality (([x = v])), disequality (([x ≠ v]) and inequality (([x ≤ v] and [x ≥ v])) literals for each variable x and for each value v in the initial domain of x, and to learn a clause (a disjunction of literals) whenever a conflict arises, i.e. when the current partial assignment has been identified as unsatisfiable. This clause represents a nogood (a partial assignment and a subset of constraints that necessarily lead to a conflict) and is added to a SAT formula in conjunctive normal form (CNF). Unit propagation [9], the propagation mechanism of SAT solvers, is then performed over this formula along the search to get further inference strength.

To be able to learn a clause, the filtering done during constraint propagation is explained: a reason (a set of literals) $R(p)$ is computed for each pruning $p$ (typically $[x \neq v]$, $[x \leq v]$ or $[x \geq v]$) such that if the literals in $R(p)$ are all set to true at some point of the search then the pruning $p$ can safely be operated. All this information is encapsulated within the implication graph which is dynamically updated along the search, where the set of predecessors $N^{-}(v)$ of a given node $v$ is the reason of the corresponding literal. By definition, the decisions that were taken by the search have no reason, and are therefore source nodes of the implication graph, which is a directed acyclic graph (DAG). When a conflict arises, its reason is computed and the implication graph is analysed to find a vertex-cut separating the decision nodes from the conflict node, this is called conflict analysis. This vertex-cut provides a nogood [41] which is then transformed into a clause that is learned. The first unique implication point (1-UIP) vertex-cut is considered to be the best in practice [41, 13] because it can be found in linear time in the size of the explored subgraph [28] while providing a good-quality nogood. The 1-UIP procedure is implemented within modern LCG solvers like Choco-solver [33], Chuffed [11] and OR-Tools [32]. Clause minimisation [37], i.e. removing redundant literals, can also be performed over the found clauses to get stronger nogoods.

Another version of lazy clause generation consists in lazily generating explanations (reasons) [20], in contrast with the version described above that eagerly generate them. The motivation is that most of the explanations generated along the search will never be used during conflict analysis to find the new clause to learn. Their generation is then purely wasted time. To avoid this, when a pruning occurs, sufficient information is stored so that the explanation can be generated later during conflict analysis. By doing this, all generated explanations are actually used to find the clause to learn. Of course, generating explanations afterwards may bring some overhead. Yet, it appears in practice that this overhead can be compensated by the gains achieved by ignoring the useless explanations [20].

In this paper, we do not use lazy explanations but eagerly generate them. The combination of lazy explanations and biclique factorisation constitutes a direction for future work.

# 3 Biclique Factorisation of Explanations

To reduce the overhead of lazy clause generation—particularly when global constraints produce many explanations—we propose to factorise the bicliques that would otherwise be generated in the implication graph. This overhead arises in particular because multiple prunings may share common subsets of literals in their reasons, leading to a large number of arcs and a dense implication graph.

Given a directed graph $G = (V, A)$, let $S_L$ and $S_R$ be two disjoint subsets of V such
4 Biclique Factorisation of Explanations in Lazy Clause Generation

<figure><img src="image_4.png" /><figcaption>Figure 1 The original (left) and a factorised (right) implication graph at some point of the search for the following CSP. Variables: $a \in \{1, \dots, 10\}$, $b \in \{2, \dots, 10\}$, $u \in \{3, \dots, 6\}$, $v \in \{3, \dots, 6\}$, $x \in \{1, \dots, 4\}$ and $y \in \{1, \dots, 4\}$. Constraints: `ALLDIFFERENT(a, b, u, v, x, y)` and `[[u = 3]] ∨ [[u = 4]] ∨ [[v = 3]] ∨ [[v = 4]]`. The explanations for `ALLDIFFERENT` are the ones described in [14].</figcaption></figure>

that $S_L \times S_R \subseteq A$. The subgraph $(S_L \cup S_R, S_L \times S_R)$ is then a complete directed bipartite graph, called a (directed) biclique of G. Factorising this biclique means creating a new vertex f, called the factor, and replacing $(S_L \cup S_R, S_L \times S_R)$ in G by the directed graph $(S_L \cup \{f\} \cup S_R, (S_L \times \{f\}) \cup (\{f\} \times S_R))$. We then say that G has been factorised. By doing this, the number of arcs in G is reduced by $(|S_L| \times |S_R|) - (|S_L| + |S_R|)$ while preserving the reachability relationships. Biclique factorisation is then interesting as soon as both $S_L$ and $S_R$ contain at least 2 vertices and one of them (or both) contain 3 or more vertices.

Let us go back to LCG and the implication graph. Let P be a set of prunings such that $R(p) = L \cup R_p$ for each $p \in P$, where L is the common subset of literals in the reason of the prunings and $R_p$ denotes the other literals in addition to L in the reason of p (potentially $R_p = \emptyset$). Instead of generating all arcs $(\ell, p) \in L \times P$ in the implication graph, we add the artificial node f, the factor, and we create an arc $(\ell, f)$ for each $\ell \in L$ and an arc $(f, p)$ for each $p \in P$ (Figure 1). The arcs $R_p \times \{p\}$ for each $p \in P$ are generated as usual.

When a pruning occurs, the clause representing the pruning and its reason is added to the CNF formula to maintain the consistency between the boolean encoding and the actual domains. This clause will be removed from the formula upon backtracking. Without biclique factorisation, the following clauses are added to the current CNF formula.

$$ (p \lor \bigvee_{\ell \in L} \neg \ell \lor \bigvee_{r \in R_p} \neg r) \quad \forall p \in P $$

With biclique factorisation, the following clauses are added instead.

$$ (f \lor \bigvee_{\ell \in L} \neg \ell) \quad \text{and} \quad (p \lor \neg f \lor \bigvee_{r \in R_p} \neg r) \quad \forall p \in P $$

The same updates will be made by unit propagation. This formulation reminds us of common subclause elimination [5].

Biclique factorisation has already been studied in many fields including circuit design [27], linear boolean operators [24] and graph compression [16]. However, to the best of our knowledge, no such technique was implemented nor described within the CP community for LCG [30, 17, 20, 38, 12], nor within the SAT community for CDCL [41, 6, 3, 9, 2].
## 3.1 Conflict Analysis in the Factorised Implication Graph

The whole point of constructing the implication graph is to analyse it when a conflict occurs to deduce clauses to learn. The question that naturally arises is then the following: Can we adapt the original conflict analysis techniques to the factorised implication graph ? The answer is yes and we shall see why.

The difference brought by biclique factorisation is the way to get access to the reason of a literal. In the presence of factors, one must recursively expand the factors to retrieve the reason, as described in Algorithm 1.

**Algorithm 1** The algorithm skeletons to process the reason of a literal during conflict analysis in the original (left) and factorised (right) implication graph. $N^-(v)$ are the predecessors of a node $v$.

**procedure** PROCESSREASON($v$)
  **for** $u \in N^-(v)$ **do**
    Do something with $u$

**procedure** PROCESSREASON-F($v$)
  **for** $u \in N^-(v)$ **do**
    **if** $u$ is a factor **then**
      PROCESSREASON-F($u$)
    **else**
      Do something with $u$

The 1-UIP procedure [28], as well as *local* [6] and *recursive* [37] minimisation are graph exploration procedures that mark the nodes based on certain properties and that traverse their incoming arcs at most once. Therefore, they run in linear time in the size of the explored subgraph of the implication graph. They can easily be adapted to biclique factorisation by marking the factors as well so that they are not expanded several times when processing the reason of different literals. By doing this, the algorithms will return the same output but in linear time in the size of the explored subgraph of the factorised implication graph, which is sparser. Those three algorithms adapted to biclique factorisation are described in Section A.

Note that the order in which literals appear in the learnt clause may be different when using biclique factorisation, depending on the way explanations are generated by propagators and on the way conflict analysis constructs the clause. This may lead to different search trees because unit propagation may not find the same conflict due to different watched literals. In our case, there will be no difference in the order of literals for the considered explanations and propagators when using biclique factorisation, so the search tree will remain the same.

## 3.2 Implementation for the ALLDIFFERENT and CUMULATIVE constraints

In this paper, we implement biclique factorisation for two core global constraints that are widely used in practice and have received considerable attention in the literature: ALLDIFFERENT [34] (Section 4) and CUMULATIVE [1] (Section 5). We show how to identify bicliques that would be generated in the implication graph and how to factorise them efficiently. This leads to better time complexities for generating explanations for these two constraints. Indeed, we analyse the worst-case time complexity of explanation generation only, excluding the rest of the propagator and focusing solely on the additional overhead introduced by generating explanations. We present theoretical results for a single propagator call as well as over an entire search branch, both with and without biclique factorisation. In particular, we establish upper bounds on the worst-case time complexity and prove their tightness by exhibiting families of instances that attain them. All these complexity results are summarised in Table 1. Upper bounds are obtained by bounding the computation time of
explanations, which simultaneously provides a bound on the output size, which corresponds to the number of generated arcs. Inversely, we derive lower bounds on the running time by establishing lower bounds on the number of generated arcs. Therefore, these tight bounds hold for both the worst-case computation time and the maximum number of generated arcs.

## 4 The ALLDIFFERENT Constraint

Given a set of integer variables, the ALLDIFFERENT constraint (see [21] for a survey) ensures these variables are assigned to a different value:

$$ \text{ALLDIFFERENT}(x_1, \dots, x_r) \equiv x_i \neq x_j \quad \forall (i, j) \in \{1, \dots, r\}^2 \mid i \neq j $$

The number of variables within the scope of the constraint is denoted by $r$ and the total number of distinct values from the variable domains is denoted by $d$. We assume that $r \le d$, otherwise the constraint can not be satisfied.

The state-of-the-art propagators enforcing GAC on ALLDIFFERENT [21, 25] are based on Régin's algorithm [34], which is a three-step procedure:

1. Find a maximum matching in the variable-value graph;

2. Compute the strongly connected components (SCCs) of the residual graph;

3. Prune all variable-value pairs that do not belong to the same SCC.

Specific explanations for ALLDIFFERENT were introduced in [14]. These explanations are based on the variable-value and residual graphs, we thus call them graph explanations.

The variable-value graph is the undirected bipartite graph whose vertices are the variables from the scope and the values from their domains. An edge links together a variable $x$ and a value $v$ whenever $v$ belongs to the domain of $x$. A maximum matching is computed by iteratively finding augmenting paths in the variable-value graph from unmatched variables. An alternating path is a path for which edges alternatively belong or not to the current matching, and an augmenting path is an alternating path whose both extremities are unmatched. The size of the current matching is then increased by one by switching the matching membership of the edges forming the augmenting path. The constraint is unsatisfiable whenever no augmenting path can be found from an unmatched variable $x_u$. The explanation of the conflict $\kappa$ proposed in [14] is then all missing edges between variables reachable from $x_u$ by an alternating path and values that are not (see Figure 2-left). Let $A_{var}(x_u)$ (resp. $A_{val}(x_u)$) denote the set of variables (resp. values) reachable from $x_u$ by an alternating path.

$$ \bigwedge_{x \in A_{var}(x_u)} (\llbracket x \ge v_{min} \rrbracket \wedge \llbracket x \le v_{max} \rrbracket \wedge \bigwedge_{v \in [v_{min}, v_{max}] \mid v \notin A_{val}(x_u)} \llbracket x \ne v \rrbracket) \rightarrow \kappa $$

<table><caption>Table 1 Worst-case time complexity of generating explanations for ALLDIFFERENT [14] and CUMULATIVE [36]. i) For ALLDIFFERENT, there are $r$ variables and initially $d$ distinct values. ii) For CUMULATIVE, the complexity of a single call corresponds to one iteration of the Time-Table propagator, not for reaching the fix point. The number of tasks is $n$ and the time interval is $\Delta$. A question mark ‘?’ means the claim requires further investigation.</caption><thead><tr><th rowspan="2">Worst-Case Time Complexity →<br>Propagator | Explanations ↓</th><th colspan="2">Single Call</th><th colspan="2">Down a Branch</th></tr><tr><th>Original</th><th>Factorised</th><th>Original</th><th>Factorised</th></tr></thead><tbody><tr><td>GAC ALLDIFFERENT | Graph</td><td>Θ(r<sup>3</sup> d)</td><td><b>Θ(r d)</b></td><td>Θ(r<sup>3</sup> d)</td><td><b>Θ(r<sup>2</sup> d)</b></td></tr><tr><td>Time-Table CUMULATIVE | Big-Step</td><td>Θ(n<sup>3</sup>)</td><td><b>Θ(n<sup>2</sup>)</b></td><td>Θ(n<sup>2</sup> | Δ|)</td><td>Θ(n | Δ|)?</td></tr><tr><td>Time-Table CUMULATIVE | Pointwise</td><td>Θ(n<sup>2</sup> | Δ|)</td><td><b>Θ(n | Δ|)</b></td><td>Θ(n<sup>2</sup> | Δ|)</td><td>Θ(n | Δ|)?</td></tr></tbody></table>
<figure><img src="image_5.png" /><figcaption>Figure 2 LEFT: an illustration of a variable-value graph. The current matching is $\{(a, 2), (b, 4), (d, 3)\}$ and there is no augmenting path starting from variable c. The reason of the conflict is made of the visited (black) variables paired with the unvisited (white) values, $R(\kappa) = \{[[a \ge 2]], [[a \le 4]], [[a \ne 3]], [[b \ge 2]], [[b \le 4]], [[b \ne 3]], [[c \ge 2]], [[c \le 4]], [[c \ne 3]]\}$. RIGHT: an illustration of a residual graph. The maximum matching is $\{(a, 2), (b, 4), (c, 1), (d, 3)\}$ and there are two SCCs (black and white). The variable-value pairs $\{(c, 2), (c, 4), (d, 4)\}$ are pruned and because their values belong to the same SCC they have the same reason, which is $\{[[a \ge 2]], [[a \le 4]], [[a \ne 3]], [[b \ge 2]], [[b \le 4]], [[b \ne 3]]\}$.</figcaption></figure>

Where $v_{min}$ and $v_{max}$ are respectively the minimum and maximum values from $A_{val}(x_u)$. Modern LCG solvers [11, 33] use inequality literals to spare many disequality literals.

The residual graph is a directed variant of the variable-value graph where edges are directed from variables and towards values, except for those in the maximum matching which are in the other direction. An artificial vertex $t$ is added along with an arc $(t, v_m)$ for each matched value $v_m$ and an arc $(v_u, t)$ for each unmatched value $v_u$. Whenever a variable $x_p$ and a value $v_p$ from the domain of $x_p$ do not belong to the same SCC, the pair $(x_p, v_p)$ is pruned, i.e. $v_p$ is removed from the domain of $x_p$. However, if $v_p$ is in a singleton SCC and if $x_p$ and $v_p$ are matched together, then $x_p$ is assigned to $v_p$ instead. Let $\mathbf{SCC}(v_p)$ denote the SCC that contains $v_p$. The graph explanation for the pruning $[[x_p \ne v_p]]$ is made of all missing outgoing arcs from $\mathbf{SCC}(v_p)$ (see Figure 2-right). Let $X_{\mathbf{SCC}(v_p)}$ (resp. $V_{\mathbf{SCC}(v_p)}$) denote the set of variables (resp. values) in $\mathbf{SCC}(v_p)$.

$$ \bigwedge_{x \in X_{\mathbf{SCC}(v_p)}} ([[x \ge v_{min}]] \wedge [[x \le v_{max}]] \wedge \bigwedge_{v \in [v_{min}, v_{max}] \mid v \notin V_{\mathbf{SCC}(v_p)}} [[x \ne v]]) \rightarrow [[x_p \ne v_p]] $$

Where $v_{min}$ and $v_{max}$ are respectively the minimum and maximum values from $V_{\mathbf{SCC}(v_p)}$. In case $\mathbf{SCC}(v_p) = \{v_p\}$, the reason is made of the sole equality literal $[[x_m = v_p]]$ instead, where $x_m$ is the variable matched to $v_p$.

Finding a maximum matching can be done in $O(r^{1.5} d)$ time thanks to Hopcroft-Karp's algorithm [23]. The strongly connected components are computed in $O(r d)$ time by Tarjan's algorithm [40] and the domains are then pruned in $O(r d)$ time. When using an incremental matching [34], the time spent computing a maximum matching is $O(r^2 d^2)$ down a branch, because a pair from the matching can be broken at most $r \times d$ times and finding an augmenting path takes $O(r d)$ time. Also, computing the SCCs and pruning the domains takes $O(r^2 d^2)$ time down a branch, because the propagator is called at most $r \times d$ times down a branch.

We provide tight bounds on the worst-case time complexity of generating graph explanations for ALLDIFFERENT both for a single propagator call and down a branch, with and without biclique factorisation. The upper-bound proofs are provided in this section while the lower-bound proofs are in the appendix (Section B).

**Lemma 1.** The number of deletions down a branch performed by a GAC propagator for ALLDIFFERENT is lesser than or equal to $r^2$.

**Proof.** The values removed from the domain of a variable are necessarily matched and belong
to an SCC different from `scc(t)`. Indeed, all unmatched values belong to `scc(t)` which has no incoming arcs because it is the source of the DAG of SCCs. Once a value becomes matched and belongs to an SCC distinct from `scc(t)`, it remains matched and cannot return to `scc(t)` further down the same branch. The number of such values is bounded by the size of the maximum matching, which is *r*. Therefore, the number of values removed down a branch from the domain of a given variable is lesser than or equal to *r*.

**Theorem 2.** *The worst-case time complexity of generating graph explanations is $\Theta(r^3 d)$ for a single propagator call and down a branch.*

**Upper-bound proof.** (i) The graph explanation of a conflict is computed in $O(r d)$ time by scanning the universe of values for each variable visited during the failed attempt to find an augmenting path. At most one conflict can arise down a branch.

(ii) By Lemma 1, the number of pruned variable-value pairs down a branch is $O(r^2)$. Also, a graph explanation for a pruned pair $(x, v)$ is computed in $O(r d)$ time by scanning the universe of values for each variable in `scc(v)`.

Therefore, the worst-case time complexity of generating graph explanations is $O(r^3 d)$ down a branch, and then also $O(r^3 d)$ for a single propagator call.

## 4.1 Factorised Explanations for ALLDIFFERENT

In this section, we show how to factorise graph explanations [14] for the ALLDIFFERENT constraint. First, let us identify the bicliques that would appear in the implication graph.

**Lemma 3.** Let $(x, v)$ and $(x', v')$ be two variable-value pairs pruned by Régine's algorithm and let us consider graph explanations.

$$scc(v) = scc(v') \implies R([x \neq v]) = R([x' \neq v'])$$

$$scc(v) \neq scc(v') \implies R([x \neq v]) \cap R([x' \neq v']) = \emptyset$$

**Proof.** The reason depends only on which SCC the value of the pruned pair belongs to, so two pruned pairs for which the values belong to the same SCC will have the same reason. The reason related to a given SCC *c* corresponds to the non-arcs coming from the variables in and pointing outside *c*. Because the sets of variables of two distinct SCCs are disjoints, the corresponding reasons are also disjoints.

Thanks to Lemma 3, whose claim was already partly mentioned in [20], we can identify at no extra cost which prunings will have the same reason, and thus the bicliques that would be generated in the implication graph during a single call to the propagator. Therefore, we can factorise them without any overhead. To do so, simply store for each SCC if the corresponding explanation has already been generated or not: When a variable-value pair $(x, v)$ is about to be pruned, check if the factor $f_{scc(v)}$ already exists. If not, compute the explanation associated with `scc(v)` and create the factor $f_{scc(v)}$, then add the factor with the corresponding explanation as its predecessors to the implication graph. Finally, add $[x \neq v]$ with $f_{scc(v)}$ as its sole predecessor to the implication graph. When the explanation is made of a unique literal, typically an equality literal, there is no need to create the factor as an intermediary.

**Theorem 4.** *The worst-case time complexity of generating factorised graph explanations is $\Theta(r d)$ for a single propagator call.*
**Upper-bound proof.** (i) The graph explanation of a conflict is computed in $O(r d)$ time.

(ii) At most $r^2$ pairs can be pruned (Lemma 3), and every pruned pair $(x, v)$ has exactly one predecessor in the factorised implication graph: the factor $f_{\text{scc}(v)}$. Thus, computing the predecessors for all the pruned pairs takes $O(r^2)$ time.

(iii) At most one factor is created per SCC. The predecessors of a factor $f_c$ associated with the SCC $c$ are computed by scanning the universe of values for each variable in $c$. This is done in $O(|X_c|d)$ time. The sets of variables of two distinct SCCs are disjoints so $\sum_{c \in \text{SCCs}} |X_c| = r$. Thus, computing the predecessors for all the factors takes $O(r d)$ time.

Therefore, the worst-case time complexity of generating factorised graph explanations is $O(r d)$ for a single propagator call. ◀

Thanks to Theorem 4, generating graph explanations is no longer the theoretical bottleneck in terms of worst-case time complexity for a single propagator call for enforcing GAC on and explaining ALLDIFFERENT.

**Lemma 5.** *The number of calls down a branch to a GAC propagator for ALLDIFFERENT for which pruning occurs is $O(r)$.*

**Proof.** Let us follow the evolution down a branch of the number $n_{var}$ of connected components (CCs) in the variable-value graph that contains at least one variable.

*Between two calls to the propagator.* Let us consider two consecutive calls $a$ and $b$ to the propagator and let $n_{var}^{a,end}$ (resp. $n_{var}^{b,start}$) be $n_{var}$ at the end of call $a$ (resp. at the start of call $b$). Call $b$ happens later than call $a$ on the same branch, some edges may then have been deleted but none has been added to the variable-value graph, so $n_{var}^{a,end} \le n_{var}^{b,start}$.

*Between the start and the end of the same call to the propagator.* Let $c$ be one call to the propagator and let $n_{var}^{c,start}$ (resp. $n_{var}^{c,end}$) be $n_{var}$ at the start of call $c$ (resp. at the end of call $c$). If no pruning occurs during call $c$, then no changes are made in the variable-value graph and $n_{var}^{c,start} = n_{var}^{c,end}$. Let us consider the case where a pair $(x, v)$ is pruned.

First, all inter-SCC arcs in the residual graph are pruned by the propagator. So, the CC in the variable-value graph that contained both $x$ and $v$ is split into at least two new CCs once the propagator has ended: one of the new ones contains $x$, and another $v$.

Second, the unmatched values all belong to $\text{scc}(t)$, which is the source of the DAG of SCCs. So, all pruned variable-value pairs have their value matched. Also, the pairs making the matching are not pruned, so a matched value always remain in the same CC as its matched variable. Then, both $x$ and $v$ will belong to a CC that contains at least one variable. Therefore, $n_{var}$ strictly increases and so we have $n_{var}^{c,start} < n_{var}^{c,end}$.

Finally, $n_{var}$ is bounded by 1 and $r$ by definition, so we deduce that the number of calls to the propagator for which pruning occurs down a branch is $O(r)$. ◀

**Theorem 6.** *The worst-case time complexity of generating factorised graph explanations is $\Theta(r^2 d)$ down a branch.*

**Upper-bound proof.** If no conflict arises nor any pruning occurs during a propagator call, then no time is spent generating graph explanations. Moreover, at most one conflict can arise down a branch, and its reason is computed in $O(r d)$ time. Therefore by Theorem 4 and Lemma 5, the worst-case time complexity of generating factorised graph explanations is $O(r^2 d)$ down a branch. ◀

By Theorem 4 and Theorem 6, biclique factorisation allows for a faster explanation generation for ALLDIFFERENT, as well as a reduced number of generated arcs in the implication graph as explained in Section 3.2, both for a single propagator call and down a branch.
<figure><img src="image_6.png" /><figcaption>Figure 3 LEFT: an illustration of the mandatory part of a task i. RIGHT: an illustration of the mandatory part of tasks a to g, the profile and the rectangle decomposition.</figcaption></figure>

## 5 The CUMULATIVE Constraint

A task i is made of an integer variable $s_i$ defining its starting time, as well as a positive integer $d_i$ corresponding to its duration, and a positive integer $h_i$ called the height and representing the resource consumption of the task. Given a set of tasks, denoted as *Tasks*, and a capacity c, the CUMULATIVE constraint ensures the cumulated resource consumption never exceeds the capacity:

$$ \text{CUMULATIVE}(\text{Tasks}, c) \equiv \sum_{i \in \text{Tasks} \mid s_i \le t_p < s_i+d_i} h_i \le c \quad \forall t_p \in \Delta $$

Where $\Delta = \{min_{i \in \text{Tasks}}(\underline{s_i}), \dots, max_{i \in \text{Tasks}}(\overline{s_i} + d_i) - 1\}$ is the discrete time interval over which the tasks can be performed. The number of tasks is denoted by $n$.

Because the *resource-constrained project scheduling problem* (RCPSP) is NP-Hard [10], enforcing bound consistency on CUMULATIVE is also NP-Hard. So, many filtering rules were proposed for CUMULATIVE, and a filtering rule that received considerable attention in the literature is the *time-table propagator* [7, 26, 31, 19]. In time-table propagation, the resource profile induced by the mandatory parts of the tasks can be represented as a step function over time (Figure 3). For a task i with earliest start time $\underline{s_i}$, latest start time $\overline{s_i}$ and duration $d_i$, the mandatory part is the time interval $[\underline{s_i}, \underline{s_i} + d_i]$ whenever $\overline{s_i} < \underline{s_i} + d_i$. The resource profile obtained by aggregating these mandatory parts is piecewise constant and changes value only at event points corresponding to the start or end of mandatory parts. This profile can be viewed as a decomposition of rectangles $(R_j)_{j \in J}$ in the time-resource plane. A rectangle $R_j$ is defined over a time interval $[a_j, b_j]$ and is made of all tasks whose mandatory part contains $[a_j, b_j]: \text{Tasks}(R_j) = \{i \in \text{Tasks} \mid \overline{s_i} \le a_j \wedge \underline{s_i} + d_i \ge b_j\}$. The height of $R_j$ is then the cumulated mandatory resource consumption over $[a_j, b_j]: h_j = \sum_{\ell \in \text{Tasks}(R_j)} h_\ell$. The number of rectangles can not exceed $2n+1$. During propagation, these rectangles are used to update the bounds of the start times: for each task i and for each rectangle $R_j$, the algorithm verifies whether i would overload $R_j$. More precisely, it verifies whether scheduling i at $\underline{s_i}$ (resp. $\overline{s_i}$) would make i overlap with $[a_j, b_j]$ and cause the total resource consumption to exceed the capacity; if so, $s_i$ (resp. $s_i + d_i$) must be greater than or equal to $b_j$ (resp. lesser than or equal to $a_j$). Rectangles are processed from left to right using a sweep algorithm, resulting in an $O(n^2)$ time complexity for the time-table propagator [19].

Three types of explanations were proposed in [36]: naive, big-step and pointwise. Here, we focus on explanations for bound updates, but explanations are similar for conflicts, i.e. when the constraint is detected as unsatisfiable. Let us consider the earliest start time updates, the latest start time are updated symmetrically. Given a task i that would overload a rectangle $R_j$ over $[a_j, b_j]$, the naive explanation for setting $\underline{s_i}$ to $b_j$ is made of the current lower-bound of $s_i$ and the current bounds of the tasks in $\text{Tasks}(R_j)$. Big-step explanations are more
general by considering sufficient bounds for having this overload:

$$ \llbracket s_i \geq a_j + 1 - d_i \rrbracket \wedge \bigwedge_{\ell \in \text{Tasks}(R_j)} (\llbracket s_\ell \leq a_j \rrbracket \wedge \llbracket s_\ell \geq b_j - d_\ell \rrbracket) \longrightarrow \llbracket s_i \geq b_j \rrbracket $$

Pointwise explanations refine big-step explanations by focusing on individual timepoints rather than whole rectangles. Each timepoint corresponds to a position within a rectangle that would be overloaded; and two consecutive timepoints can not be more than $d_i$ apart for a task $i$. Let $\text{Tasks}(t_p) = \{i \in \text{Tasks} | \bar{s}_i \leq t_p < s_i + d_i\}$ be the set of tasks whose mandatory part overlaps with a timepoint $t_p$. Let $\text{TP}$ be a valid set of timepoints for updating $s_i$, pointwise explanations are generated in increasing timepoint order:

$$ \llbracket s_i \geq t_p + 1 - d_i \rrbracket \wedge \bigwedge_{\ell \in \text{Tasks}(t_p)} (\llbracket s_\ell \leq t_p \rrbracket \wedge \llbracket s_\ell \geq t_p + 1 - d_\ell \rrbracket) \longrightarrow \llbracket s_i \geq t_p + 1 \rrbracket \quad \forall t_p \in \text{TP} $$

A single pointwise explanation can be seen as a big-step explanation whose rectangle that would be overloaded has width 1. There are many ways to choose a valid set of timepoints and the complexity results presented in this section hold for any timepoints choices.

We analyse worst-case time complexity as a function of the parameters that independently affect the running time. These parameters are $n$, $c$ and $|\Delta|$. We assume that the integer variables are represented by their bounds, which is usually the case when considering scheduling problems, so the size of a CUMULATIVE instance is $O(n(\log(|\Delta|) + \log(c)))$ (assuming that the minimum starting time is 0). Then, $c$ and $|\Delta|$ are numeric parameters and are included in the analysis only when they can not be avoided to express the worst-case complexity. The influence of $c$ in the theoretical bounds lies in the maximum number of tasks that can be performed in parallel, which is also bounded by $n$. Because the worst cases are attained when $\min(n, c) = n$, we do not use $c$ to express the worst-case bounds. For the same reason, we do not use $|\Delta|$ in the worst-case complexity of generating (factorised) big-step explanations for a single propagator call. Indeed, $|\Delta|$ influences the maximum number of rectangles, which is also $O(n)$. However, we can not avoid $|\Delta|$ in the other complexity results, meaning that these problems are pseudo-polynomial. The upper-bound proofs are provided in this section while the lower-bound proofs are in the appendix (Section C).

**Theorem 7.** *The worst-case time complexity of generating big-step explanations is $\Theta(n^3)$ for a single propagator call.*

**Upper-bound proof.** During a single propagator call, a big-step explanation is computed at most once per task-rectangle pair. The number of tasks and the number of rectangles are $O(n)$. The number of tasks per rectangle is $O(n)$, so a big-step explanation is computed in $O(n)$ time. Therefore, the worst-case time complexity of generating big-step explanations is $O(n^3)$ for a single propagator call. ◀

**Theorem 8.** *The worst-case time complexity of generating big-step explanations is $\Theta(n^2|\Delta|)$ down a branch.*

**Upper-bound proof.** The number of bound updates, and thus the required number of big-step explanations, can not exceed $n \times |\Delta|$ down a branch. Indeed, beyond $n \times |\Delta|$ bound updates a domain is necessarily emptied and a conflict arises. Furthermore, a big-step explanation is computed in $O(n)$ time. Therefore, the worst-case time complexity of generating big-step explanations is $O(n^2|\Delta|)$ down a branch. ◀

**Theorem 9.** *The worst-case time complexity of generating pointwise explanations is $\Theta(n^2|\Delta|)$ for a single propagator call and down a branch.*
**Upper-bound proof.** The number of bound updates, and thus the required number of pointwise explanations, can not exceed $n \times |\Delta|$ down a branch. Furthermore, a pointwise explanation is computed in $O(n)$ time. Therefore, the worst-case time complexity of generating pointwise explanations is $O(n^2|\Delta|)$ down a branch, and then also $O(n^2|\Delta|)$ for a single propagator call. ◀

## 5.1 Factorised Explanations for CUMULATIVE

In this section, we show how to factorise big-step and pointwise explanations [36] for the time-table propagator for CUMULATIVE. In the formulation of big-step (resp. pointwise) explanations, an explanation can be decomposed into two components: (a) a literal explaining why the updated task intersects the rectangle (resp. the timepoint), and (b) a set of literals explaining the mandatory parts that constitute the rectangle (resp. the timepoint) that would be overloaded. Part (b) is not dependent to which bound is updated, so it gives rise to a large biclique in the implication graph whenever (1) many tasks are performed in parallel due to a high capacity, and (2) multiple explanations are generated for the same rectangle (resp. timepoint). Thanks to this observation, we can efficiently factorise big-step (resp. pointwise) explanations within a single call to the propagator. To do so, simply store for each rectangle (resp. timepoint) if the corresponding part (b) has already been generated or not: When a bound is about to be updated because of a rectangle $R_j$ (resp. a timepoint $t_p$), check if the factor $f_{R_j}$ (resp. $f_{t_p}$) already exists. If not, compute the literals of part (b) and create the factor $f_{R_j}$ (resp. $f_{t_p}$), then add the factor with the literals of part (b) as its predecessors to the implication graph. Finally, add the bound update with the literal of part (a) and $f_{R_j}$ (resp. $f_{t_p}$) as its two predecessors to the implication graph.

**Theorem 10.** *The worst-case time complexity of generating factorised big-step explanations is $\Theta(n^2)$ for a single propagator call.*

**Upper-bound proof.** (i) The big-step explanation of a conflict is computed in $O(n)$ time.

(ii) At most two bound updates (lower and upper) can happen per task and per rectangle during one propagator call. The number of tasks and the number of rectangles are $O(n)$, so the number of bound updates is $O(n^2)$. The predecessors in the factorised implication graph of a bound update for a task $i$ and a rectangle $R_j$ are a literal related to $i$ and the factor $f_{R_j}$. Thus, computing the predecessors for all the bound updates takes $O(n^2)$ time.

(iii) At most one factor is created per rectangle, and its predecessors are computed in $O(n)$ time. Thus, computing the predecessors for all the factors takes $O(n^2)$ time.

Therefore, the worst-case time complexity of generating factorised big-step explanations is $O(n^2)$ for a single propagator call. ◀

**Theorem 11.** *The worst-case time complexity of generating factorised pointwise explanations is $\Theta(n|\Delta|)$ for a single propagator call.*

**Upper-bound proof.** (i) The pointwise explanation of a conflict is computed in $O(n)$ time.

(ii) At most two bound updates (lower and upper) can happen per task and per timepoint during one propagator call. The number of tasks and the number of rectangles are $O(n)$, so the number of bound updates is $O(n|\Delta|)$. The predecessors of a bound update for a task $i$ and a timepoint $t_p$ are a literal related to $i$ and the factor $f_{t_p}$. Thus, computing the predecessors for all the bound updates takes $O(n|\Delta|)$ time.

(iii) At most one factor is created per timepoint, and its predecessors are computed in $O(n)$ time. Thus, computing the predecessors for all the factors takes $O(n|\Delta|)$ time.
Therefore, the worst-case time complexity of generating factorised pointwise explanations is $O(n|\Delta|)$ for a single propagator call. ◀

By Theorem 10 and Theorem 11, biclique factorisation allows for a faster explanation generation for CUMULATIVE for a single propagator call, as well as a reduced number of generated arcs in the implication graph as explained in Section 3.2.

## 5.2 A Stronger Factorisation Down a Branch

It is possible to get a stronger factorisation of big-step and pointwise explanations by reusing past factors from the same branch. For example, let us say that a set *A* of tasks intersected with a given timepoint *t*<sub>*p*</sub> at some point of the search, and that later on the same branch a set *B* of tasks intersect with *t*<sub>*p*</sub>. Because the mandatory parts can only grow down a branch, we necessarily have *A* ⊆ *B*. If *A* = *B*, then reuse *f*<sub>*A*</sub>, the factor previously created for *t*<sub>*p*</sub>. If *A* ⊂ *B*, then create a new factor *f*<sub>*B*</sub> whose predecessors are *f*<sub>*A*</sub> and inequality literals for the tasks in *B*\*A. By doing this, every inequality literal related to a timepoint and every factor is present in the reason of at most one literal, and no more than *n* × |Δ| factors are created, so the number of generated arcs would be *O(n|Δ|)*.

Investigating the possibility of having a $O(n|\Delta|)$ time complexity for generating big-step and pointwise explanations would require studying an explanation-oriented incremental algorithm for the time-table propagator, which is not the purpose of this paper. Yet, this would constitute an interesting future work.

# 6 Experimental Study

The main objective of the experimental evaluation is to demonstrate the contribution of biclique factorisation. Specifically, we aim to quantify the benefits provided by the approach in terms of reduced memory footprint and computation time.

To do this, we selected four distinct problem categories: three involving one or more ALLDIFFERENT constraints and one involving one CUMULATIVE constraint with a large capacity. The three ALLDIFFERENT-based problems include the Golomb Ruler, Latin Square and Langford problems, all sourced from the MiniZinc Challenges [39]. The Latin Square instances converge to a solution without failures, enabling the measured execution time to accurately isolate the cost associated with explanation generation. The fourth category consists of the Large Scheduling problem, from XCSP3 library [4]. For each problem type, we ran multiple instances to observe the behaviour under increasing problem sizes. Note that the threshold below which variables' domain are enumerated and not bounded is set at 6500.

Biclique factorisation was implemented in Choco-solver v5.0.0 and the experiments were carried out with OpenJDK 21.0.1 on an Intel Xeon 6230 (2.10GHz) with up to 8Go RAM per job. The experimental protocol is the following. For each instance, a first resolution using biclique factorisation with a hard time limit of 5 minutes is launched; the number of nodes processed during this phase was recorded. Then, the same instance was solved again under a fixed limit of the recorded node count, with and without biclique factorisation. A dynamic memory management strategy was employed via the Java `-Xmx` flag: if the resolution failed due the memory exhaustion, the available heap was increased iteratively until a successful run was obtained. Once a valid resolution was achieved for the required parameters, this configuration was locked and the instance was resolved 9 more times to ensure statistical stability. Finally, the elapsed time and the cumulative size of generated clauses (i.e., the total number of arcs generated in the implication graph) were aggregated.
<figure><img src="image_7.png" /><figcaption>**Figure 4** Total number of generated arcs and computation time without (a.k.a. 'base') and with biclique factorisation on four problems: Golomb Ruler (upper-left), Latin Square (upper-right), Langford (lower-left) and Large Scheduling (lower-right). For each problem, the top figure represents the total number of generated arcs and values within the rectangles denote the minimum memory required to solve the instance, while empty squares indicate that the memory requirement is identical to that of the previously evaluated rectangle. The bottom figure represents the computation time with the violin plot for each parameter value, the curve passes through the mean value.</figcaption></figure>

The experimental results are presented in Figure 4. Each sub-figure consists of two sub-plots illustrating the performance trade-offs. The upper plot displays the resource overhead, reporting both the total number of generated arcs and the upper memory limit imposed to process the instance as the problem size grows. The lower plot depicts the solving time necessary to either reach the node limit or to fully close the instance, evaluated under the strict memory constraints determined by the protocol.

## Number of Arcs

The upper plots reveal a consistent reduction in the number of arcs when biclique factorisation is activated. Across all problem categories, biclique factorisation significantly decreases the arc count compared to the standard baseline. This compactness translates to a decrease in the memory footprint, an effect that is particularly pronounced in the Golomb Ruler problem. On the largest instances of Golomb Ruler, the memory requirement is reduced by nearly a
factor of three, and one instance could not be solved under 8Go without biclique factorisation, confirming the efficacy of the proposed approach in managing resource consumption without sacrificing solving capability.

## Time

One must first contextualise the variance observed in certain instances, which is primarily attributable to the non-deterministic triggering of the Java Virtual Machine's garbage collector under critical memory pressure. This is particularly evident in the Langford and Large Scheduling problems. Beyond this variability, a strong positive correlation emerges between the reduction in arc count and the improvement in solving speed; the greater the difference in arc count, the more significant the gain observed for the Golomb Ruler, Latin Square, and Langford instances. For the Large Scheduling problem, however, the improvement is less marked and, in some scenarios, slightly favours the baseline without biclique factorisation. This discrepancy arises because the reduction in arc generation is relatively modest for this instance, and crucially, the overhead incurred in creating and analysing clauses upon conflict detection is insignificant when compared to the time spent propagating the CUMULATIVE constraint. Consequently, for this problem, the dominant computational cost lies elsewhere, diluting the relative impact of the optimisation in the implication graph.

## 7 Conclusion

We proposed *biclique factorisation* as a method to reduce the overhead of lazy clause generation, particularly for large global constraints where bicliques naturally arise in the implication graph. We implemented this technique for the *ALLDIFFERENT* and *CUMULATIVE* constraints, and established tight bounds on both the worst-case time complexity of explanation generation and the maximum number of generated arcs. An experimental evaluation conducted with *Choco-solver* demonstrates the practical impact of the approach.

Several directions for future work emerge from this study. First, it would be valuable to implement biclique factorisation for other global constraint propagators. In particular, alternative propagators for *CUMULATIVE* such as *edge-finding* and *energetic reasoning* [22] would be relevant candidates. Also, flow-based global constraints [15]—such as those generalising *ALLDIFFERENT*—also appear to be promising targets for further investigation. Second, combining biclique factorisation with lazy explanations is a natural direction. Moreover, since lazy explanations preserve information accumulated along the current search branch, their integration could potentially yield stronger factorisations. Investigating the extent to which this knowledge can be exploited constitutes an interesting research direction. Finally, an open question is whether factorisation can be extended beyond the scope of a single propagator, by automatically detecting bicliques induced jointly by multiple propagators.
References

1 Abderrahmane Aggoun and Nicolas Beldiceanu. Extending chip in order to solve complex scheduling and placement problems. *Mathematical and Computer Modelling*, 17(7):57-73, 1993.
URL: https://www.sciencedirect.com/science/article/pii/089571779390068A, doi:10.1016/0895-7177(93)90068-A.

2 Sahel Alouneh, Sa'ed Abed, Mohammad H. Al Shayeji, and Raed Mesleh. A comprehensive study and analysis on sat-solvers: advances, usages and achievements. *Artificial Intelligence Review*, 52(4):2575-2601, Dec 2019. doi:10.1007/s10462-018-9628-0.

3 G. Audemard, L. Bordeaux, Y. Hamadi, S. Jabbour, and L. Sais. A generalized framework for conflict analysis. In Hans Kleine Büning and Xishun Zhao, editors, *Theory and Applications of Satisfiability Testing - SAT 2008*, pages 21–27, Berlin, Heidelberg, 2008. Springer Berlin Heidelberg.

4 Gilles Audemard, Christophe Lecoutre, and Emmanuel Lonca. Proceedings of the 2023 xcsp3 competition. arXiv preprint arXiv:2312.05877, 2023.

5 Forrest Sheng Bao, Chris Gutierrez, Jeriah Jn Charles-Blount, Yaowei Yan, and Yuanlin Zhang. Accelerating boolean satisfiability (sat) solving by common subclause elimination. *Artificial Intelligence Review*, 49(3):439-453, Mar 2018. doi:10.1007/s10462-016-9530-6.

6 Paul Beame, Henry Kautz, and Ashish Sabharwal. Towards understanding and harnessing the potential of clause learning. *Journal of artificial intelligence research*, 22:319-351, 2004.

7 Nicolas Beldiceanu and Mats Carlsson. A new multi-resource cumulatives constraint with negative heights. In Pascal Van Hentenryck, editor, *Principles and Practice of Constraint Programming - CP 2002*, pages 63–79, Berlin, Heidelberg, 2002. Springer Berlin Heidelberg.

8 Christian Bessiere. Chapter 3 - constraint propagation. In Francesca Rossi, Peter van Beek, and Toby Walsh, editors, *Handbook of Constraint Programming*, volume 2 of *Foundations of Artificial Intelligence*, pages 29–83. Elsevier, 2006. URL: https://www.sciencedirect.com/science/article/pii/S1574652606800076, doi:10.1016/S1574-6526(06)80007-6.

9 A. Biere, A. Biere, M. Heule, H. van Maaren, and T. Walsh. *Handbook of Satisfiability: Volume 185 Frontiers in Artificial Intelligence and Applications*. IOS Press, NLD, 2009.

10 J. Blazewicz, J.K. Lenstra, and A.H.G.Rinnooy Kan. Scheduling subject to resource constraints: classification and complexity. *Discrete Applied Mathematics*, 5(1):11-24, 1983. URL: https://www.sciencedirect.com/science/article/pii/0166218X83900124, doi:10.1016/0166-218X(83)90012-4.

11 Geoffrey G Chu. *Improving combinatorial optimization*. University of Melbourne, Department of Computer Science and Software Engineering, 2011.

12 Jip J. Dekker, Alexey Ignatiev, Peter J. Stuckey, and Allen Z. Zhong. Towards Modern and Modular SAT for LCG. In Maria Garcia de la Banda, editor, *31st International Conference on Principles and Practice of Constraint Programming (CP 2025)*, volume 340 of *Leibniz International Proceedings in Informatics (LIPIcs)*, pages 42:1-42:12, Dagstuhl, Germany, 2025. Schloss Dagstuhl - Leibniz-Zentrum für Informatik. URL: https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.CP.2025.42, doi:10.4230/LIPIcs.CP.2025.42.

13 Nachum Dershowitz, Ziyad Hanna, and Alexander Nadel. Towards a better understanding of the functionality of a conflict-driven sat solver. In João Marques-Silva and Karem A. Sakallah, editors, *Theory and Applications of Satisfiability Testing - SAT 2007*, pages 287-293, Berlin, Heidelberg, 2007. Springer Berlin Heidelberg.

14 Nicholas Downing, Thibaut Feydy, and Peter J. Stuckey. Explaining alldifferent. In *Proceedings of the Thirty-Fifth Australasian Computer Science Conference - Volume 122*, ACSC '12, page 115-124, AUS, 2012. Australian Computer Society, Inc.

15 Nicholas Downing, Thibaut Feydy, and Peter J. Stuckey. Explaining flow-based propagation. In Nicolas Beldiceanu, Narendra Jussien, and Éric Pinson, editors, *Integration of AI and OR Techniques in Constraint Programming for Combinatorial Optimization Problems*, pages 146-162, Berlin, Heidelberg, 2012. Springer Berlin Heidelberg.
16 T. Feder and R. Motwani. Clique partitions, graph compression and speeding-up algorithms. *Journal of Computer and System Sciences*, 51(2):261-272, 1995. URL: https://www.sciencedirect.com/science/article/pii/S0022000085710653, doi:10.1006/jcss.1995.1065.

17 Thibaut Feydy and Peter J. Stuckey. Lazy clause generation reengineered. In Ian P. Gent, editor, *Principles and Practice of Constraint Programming - CP 2009*, pages 352-366, Berlin, Heidelberg, 2009. Springer Berlin Heidelberg.

18 Mathias Fleury and Armin Biere. Efficient all-uip learned clause minimization. In Chu-Min Li and Felip Manyà, editors, *Theory and Applications of Satisfiability Testing - SAT 2021*, pages 171-187, Cham, 2021. Springer International Publishing.

19 Steven Gay, Renaud Hartert, and Pierre Schaus. Simple and scalable time-table filtering for the cumulative constraint. In Gilles Pesant, editor, *Principles and Practice of Constraint Programming*, pages 149-157, Cham, 2015. Springer International Publishing.

20 Ian P. Gent, Ian Miguel, and Neil C. A. Moore. Lazy explanations for constraint propagators. In Manuel Carro and Ricardo Peña, editors, *Practical Aspects of Declarative Languages*, pages 217-233, Berlin, Heidelberg, 2010. Springer Berlin Heidelberg.

21 Ian P. Gent, Ian Miguel, and Peter Nightingale. Generalised arc consistency for the alldifferent constraint: An empirical survey. *Artificial Intelligence*, 172(18):1973-2000, 2008. Special Review Issue. URL: https://www.sciencedirect.com/science/article/pii/S0004370208001410, doi:10.1016/j.artint.2008.10.006.

22 Stefan Heinz and Jens Schulz. Explanations for the cumulative constraint: An experimental study. In Panos M. Pardalos and Steffen Rebennack, editors, *Experimental Algorithms*, pages 400-409, Berlin, Heidelberg, 2011. Springer Berlin Heidelberg.

23 John E. Hopcroft and Richard M. Karp. An $n^{5/2}$ algorithm for maximum matchings in bipartite graphs. *SIAM Journal on Computing*, 2(4):225-231, 1973. doi:10.1137/0202019.

24 Stasys Jukna and Igor Sergeev. Complexity of linear boolean operators. *Foundations and Trends® in Theoretical Computer Science*, 9(1):1-123, 2013. URL: http://dx.doi.org/10.1561/0400000063, doi:10.1561/0400000063.

25 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. doi:10.24963/ijcai.2025/291.

26 Arnaud Letort, Nicolas Beldiceanu, and Mats Carlsson. A scalable sweep algorithm for the cumulative constraint. In Michela Milano, editor, *Principles and Practice of Constraint Programming*, pages 439-454, Berlin, Heidelberg, 2012. Springer Berlin Heidelberg.

27 Oleg B Lupanov. On rectifier and switching-and-rectifier schemes. In *Dokl. Akad. Nauk SSSR*, volume 111, pages 1171-1174, 1956. URL: https://web.vu.lt/mif/s.jukna/boolean/lupanov56.pdf.

28 J.P. Marques Silva and K.A. Sakallah. Dynamic search-space pruning techniques in path sensitization. In *31st Design Automation Conference*, pages 705-711, 1994. doi:10.1109/DAC.1994.204192.

29 J.P. Marques-Silva and K.A. Sakallah. Grasp: a search algorithm for propositional satisfiability. *IEEE Transactions on Computers*, 48(5):506-521, 1999. doi:10.1109/12.769433.

30 Olga Ohrimenko, Peter J. Stuckey, and Michael Codish. Propagation via lazy clause generation. *Constraints*, 14(3):357-391, Sep 2009. doi:10.1007/s10601-008-9064-x.

31 Pierre Ouellet and Claude-Guy Quimper. Time-table extended-edge-finding for the cumulative constraint. In Christian Schulte, editor, *Principles and Practice of Constraint Programming*, pages 562-577, Berlin, Heidelberg, 2013. Springer Berlin Heidelberg.

32 Laurent Perron and Frédéric Didier. Cp-sat. URL: https://developers.google.com/optimization/cp/cpSolution/.
33 Charles Prud'homme and Jean-Guillaume Fages. Choco-solver: A java library for constraint programming. *Journal of Open Source Software*, 7(78):4708, 2022.

34 Jean-Charles RÉGIN. A filtering algorithm for constraints of difference in csps. In *Proceedings of the Twelfth AAAI National Conference on Artificial Intelligence*, AAAI'94, page 362–367. AAAI Press, 1994.

35 Francesca Rossi, Peter van Beek, and Toby Walsh. *Handbook of Constraint Programming*. Elsevier Science Inc., USA, 2006.

36 Andreas Schutt, Thibaut Feydy, Peter J. Stuckey, and Mark G. Wallace. Explaining the cumulative propagator. *Constraints*, 16(3):250–282, Jul 2011. doi:10.1007/s10601-010-9103-2.

37 Niklas Sörensson and Armin Biere. Minimizing learned clauses. In Oliver Kullmann, editor, *Theory and Applications of Satisfiability Testing - SAT 2009*, pages 237–243, Berlin, Heidelberg, 2009. Springer Berlin Heidelberg.

38 Peter J. Stuckey. Lazy clause generation: Combining the power of sat and cp (and mip?) solving. In Andrea Lodi, Michela Milano, and Paolo Toth, editors, *Integration of AI and OR Techniques in Constraint Programming for Combinatorial Optimization Problems*, pages 5–9, Berlin, Heidelberg, 2010. Springer Berlin Heidelberg.

39 Peter J. Stuckey, Ralph Becket, and Julien Fischer. Philosophy of the MiniZinc challenge. *Constraints*, 15:307–316, 2010.

40 Robert Tarjan. Depth-first search and linear graph algorithms. *SIAM Journal on Computing*, 1(2):146–160, 1972. doi:10.1137/0201010.

41 Lintao Zhang, C.F. Madigan, M.H. Moskewicz, and S. Malik. Efficient conflict driven learning in a boolean satisfiability solver. In *IEEE/ACM International Conference on Computer Aided Design. ICCAD 2001. IEEE/ACM Digest of Technical Papers (Cat. No.01CH37281)*, pages 279–285, 2001. doi:10.1109/ICCAD.2001.968634.
A First-UIP, Local Minimisation and Recursive Minimisation with
Biclique Factorisation

The 1-UIP nogood [29] is found by exploring the reverse implication graph (arcs are in the other direction) by considering the nodes from the top of the trail (the stack of literals added to the implication graph) and replacing them by their reason in the nogood under construction. This is done until exactly one literal *p* from the nogood belongs to the same decision level as the conflict node (*p* is a *unique implication point* (UIP)). A property of the 1-UIP clause is that backtracking to a previous decision level will set the UIP to true by unit propagation, and thus some inference is immediately done. This is called an *asserting* clause. We present in Algorithm 2 the 1-UIP procedure adapted to biclique factorisation.

We assume that all literals of a given decision level are reachable in the implication graph
from the decision node of that same level. This property is ensured, for example, when the
strongest available propagators are systematically used during constraint propagation. If
this assumption does not hold then the presented algorithms should be adapted accordingly.

The found nogood may not be minimal, as some proper subsets of it may be nogoods
themselves. These subsets will then be of better quality as they may be triggered sooner by
unit propagation or allow for greater jumps by non-chronological backtracking. Therefore,
some internal procedures within clause learning based solvers consists in minimising the
found nogood. Two minimisation methods that lead to good practical performances are

■ **Algorithm 2** Finding the 1-UIP nogood with biclique factorisation

Require: The factorised implication graph, the *trail* and the conflict node *κ*

Ensure: Find the 1-UIP nogood

1: $NG \leftarrow \emptyset$ \quad $\triangleright$ The 1-UIP nogood under construction

2: *count* ← 1

3: Mark $κ$

4: **do** \quad $\triangleright$ $κ$ is initially on the top of the *trail*

5: $v \leftarrow \text{trail.pop()}$

6: **if** *v* is marked ∧ *v* is not a factor **then**

7: PROCESSREASON-F-1-UIP(*v*)

8: $count \leftarrow count - 1$

9: **while** *count* > 1

10: **do**

11: $p \leftarrow \text{trail.pop()}$

12: **while** *p* is not marked

13: Add *p* to *NG*

14: **return** *NG*

15: **procedure** PROCESSREASON-F-1-UIP(*v*)

16: **for** $u \in N^-(v) : level(u) > 0$ **do** \quad $\triangleright$ Ignore literals from initial propagation

17: **if** *u* is not marked **then**

18: **if** *u* is a factor **then**

19: PROCESSREASON-F-1-UIP(*u*)

20: **else if** level(*u*) = level(*κ*) **then** \quad $\triangleright$ Literal from conflict level

21: $count \leftarrow count + 1$

22: **else**

23: Add *u* to *NG*

24: Mark *u*

$\triangleright$ Literal from anterior level
**Algorithm 3** Local minimisation of the 1-UIP nogood with biclique factorisation

**Require:** The factorised implication graph, the 1-UIP nogood *NG* and its *UIP* *p*

**Ensure:** Apply local minimisation to *NG*

1: $NG_{init} \leftarrow NG$ ▷ Store the information of the initial nogood
2: **for** $n \in NG_{init} \setminus \{p\}$ **do**
3: &nbsp;&nbsp;&nbsp;&nbsp;**if** *n* is not a decision ∧ **PROCESSREASON-F-LOCAL**(*v*) **then**
4: &nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;**Remove** *n* from *NG*
5: &nbsp;&nbsp;&nbsp;&nbsp;**procedure** **PROCESSREASON-F-LOCAL**(*v*)
6: &nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;**for** *u* ∈ $N^-(v)$ **do**
7: &nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;**if** *u* is a factor **then**
8: &nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;**if** *u* is not marked **then**
9: &nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;**res** ← **PROCESSREASON-F-LOCAL**(*u*)
10: &nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;**if** *u* is marked as *included* ∨ **res** = **TRUE** **then**
11: &nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;**Mark** *u* as *included*
12: &nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;**else if** *u* is marked as *non-included* ∨ **res** = **FALSE** **then**
13: &nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;**Mark** *u* as *non-included*
14: &nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;**return** **FALSE** ▷ A literal from the reason does not belong to the nogood
15: &nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;**else if** *u* ∉ $NG_{init}$ **then**
16: &nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;**return** **FALSE** ▷ A literal from the reason does not belong to the nogood
17: &nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;**return** **TRUE** ▷ All literals from the reason belong to the nogood

**Algorithm 4** Recursive minimisation of the 1-UIP nogood with biclique factorisation

**Require:** The factorised implication graph, the *trail*, the 1-UIP nogood *NG* and its *UIP* *p*

**Ensure:** Apply recursive minimisation to *NG*

1: **levels** ← {$level(n) | n \in NG$}
2: **minRank**($\ell$) ← $min_{n \in NG|level(n)=\ell}(rank(n))$ ∀$\ell \in levels$
3: $NG_{init} \leftarrow NG$ ▷ Store the information of the initial nogood
4: **for** $n \in NG_{init} \setminus \{p\}$ **do**
5: &nbsp;&nbsp;&nbsp;&nbsp;**if** $ISDOMINATED(n, n)$ **then**
6: &nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;**Remove** $n$ from $NG$
7: **function** $ISDOMINATED(v, n)$
8: &nbsp;&nbsp;&nbsp;&nbsp;**if** $v \in NG_{init} \setminus \{n\} \lor v$ is marked as *dominated* **then** **return** **TRUE**
9: &nbsp;&nbsp;&nbsp;&nbsp;**else if** $v$ is marked as *undominated* **then** **return** **FALSE**
10: &nbsp;&nbsp;&nbsp;&nbsp;**else if** $v$ is a decision ∨ $level(v) \notin levels$ ∨ $rank(v) < minRank(level(v))$ **then**
11: &nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;**Mark** $v$ as *undominated*
12: &nbsp;&nbsp;&nbsp;&nbsp;**return** **FALSE** ▷ The literal *v* is not dominated by $NG_{init}$
13: **else**
14: &nbsp;&nbsp;&nbsp;&nbsp;**for** $u \in N^-(v) : level(u) > 0$ **do**
15: &nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;**if** $\neg ISDOMINATED(u, n)$ **then**
16: &nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;**Mark** $v$ as *undominated*
17: &nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;**return** **FALSE** ▷ The literal *v* is not dominated by $NG_{init}$
18: &nbsp;&nbsp;&nbsp;&nbsp;**Mark** $v$ as *dominated*
19: &nbsp;&nbsp;&nbsp;&nbsp;**return** **TRUE** ▷ The literal *v* is dominated by $NG_{init}$

local [6] and recursive [37] minimisation. The first consists in removing from the nogood all literals whose reason is included in the nogood. The second removes every literal *n* that is dominated by the nogood *NG*, i.e every path from a decision to *n* passes through at least
one literal from $NG\setminus\{n\}$.

We present in Algorithm 3 and Algorithm 4 the local and recursive minimisations adapted to biclique factorisation. Actually, no particular changes are required for recursive minimisation in the presence of factors. Let rank($\ell$) denote the index of a literal $\ell$ in the trail. The smaller the rank, the longer ago the literal was added to the implication graph. For recursive minimisation, the conditions in line 10 related to levels and minRank are optimisations to reduce the size of the explored subgraph [37, 18].

## B Lower-Bound Proofs for ALLDIFFERENT

To establish lower bounds on the worst-case time complexity of generating graph explanations for ALLDIFFERENT, we construct infinite families of constraint satisfaction problems (CSPs) that each contain an ALLDIFFERENT constraint. In these families, the number of variables $r$ and the number of values $d$ for the ALLDIFFERENT constraint can grow independently subject only to the necessary condition $r \le d$, ensuring that all considered instances are non-trivial.

**Proof of the lower bound in Theorem 2.** Let $(G_{k,\ell}^C)_{k,\ell \in \mathbb{N}_{>0}}$ be a family of CSPs defined as follows (see Figure 5-left). Let $k, \ell \in \mathbb{N}_{>0}$, the CSP $G_{k,\ell}^C$ is made of:

- A set $V$ of $k$ values whose minimum is $v_{min}$ and whose maximum is $v_{max}$, and a set $A$ of $k$ integer variables whose domain is $V$;

- A set $W$, disjoint from $V$, of $k+\ell$ values greater than $v_{min}$ and smaller than $v_{max}$, and a set $B$ of $k$ integer variables whose domain is $V \cup W$;

- A constraint ALLDIFFERENT($A \cup B$).

When the GAC propagator for ALLDIFFERENT is called for the first time, the residual graph has two SCCs: one made up of $A \cup V$ and another of $B \cup W \cup \{t\}$. All variable-value pairs in $B \times V$ are pruned, and the explanations are

$$ \bigwedge_{a \in A} (\llbracket a \ge v_{min} \rrbracket \wedge \llbracket a \le v_{max} \rrbracket \wedge \bigwedge_{w \in W} (\llbracket a \ne w \rrbracket) \rightarrow \llbracket b \ne v \rrbracket \quad \forall b, v \in B, V $$

So, a number of $k^2 \times k \times (k+\ell+2)$ arcs are generated in $\Omega(k^3(k+\ell))$ time. Also, the number of variables is $r = 2k$, so $k = \Omega(r)$. And the number of distinct values is $d = 2k+\ell$, so $k+\ell = \Omega(d)$. Therefore, the worst-case time complexity of generating graph explanations is $\Omega(r^3 d)$ for a single propagator call, and then also $\Omega(r^3 d)$ down a branch. ◀

<figure><img src="image_8.png" /><figcaption>■ Figure 5 LEFT: an illustration of the residual graph during initial propagation for the CSP $G_{k,\ell}^C$. RIGHT: an illustration of the residual graph down a branch for the CSP $G_{k,\ell}^B$. The artificial vertex $t$ is not represented because its presence would not change the SCCs.</figcaption></figure>
**Proof of the lower bound in Theorem 4.** Let $k, \ell \in \mathbb{N}_{>0}$, and let $G_{k,\ell}^C$ be the CSP defined previously. A factor for the SCC $A \cup V$ is created and its reason of size $\Omega(k(k+\ell))$ is computed in $\Omega(k(k+\ell))$ time. The number of variables is $r = 2k$, so $k = \Omega(r)$, and the number of values is $d = 2k+\ell$, so $k+\ell = \Omega(d)$. Therefore, the worst-case time complexity of generating factorised graph explanations is $\Omega(rd)$ for a single propagator call. ◀

**Proof of the lower bound in Theorem 6.** Let $(G_{k,\ell}^B)_{k,\ell \in \mathbb{N}_{>0}}$ be a family of CSPs defined as follows (see Figure 5-right). Let $k, \ell \in \mathbb{N}_{>0}$, the CSP $G_{k,\ell}^B$ is made of:

- A set $A = (a_i)_{1 \le i \le k-1}$ of $k-1$ integer variables whose initial domain is $\{0, \dots, k+\ell\}$;

- Two integer variables $x$ and $y$ whose initial domain is $\{0, \dots, k+\ell\}$;

- A constraint `ALLDIFFERENT$(A \cup \{x, y\})$;

- A boolean variable $b$ and a constraint $b \implies z \neq i$ for $k \le i \le k+\ell-1$ and $z \in A \cup \{x, y\}$;

- A set $B = (b_i)_{1 \le i \le k-1}$ of $k-1$ boolean variables and a constraint $b_i \implies z \neq i$ for $1 \le i \le k-1$ and $z \in (A \setminus \{a_i\}) \cup \{x, y\}$.

The search consists in branching first on $b$ and then on the boolean variables in $B$ by increasing order of index, and setting them first to true. No pruning occurs during initial propagation nor after setting $b$ to true. After $b_i$ is set to true, with $1 \le i \le k-1$, the variables $a_j$ for $1 \le j \le i-1$ are already instantiated to $j$, the values $\{k, \dots, k+\ell-1\}$ are present in the domain of no variable, and the current domain of $a_i$ is $\{i, \dots, k-1\} \cup \{0, k+\ell\}$. Also, the variables $\{a_j | i+1 \le j \le k-1\} \cup \{x, y\}$ and the values $\{i+1, \dots, k-1\} \cup \{0, k+\ell\}$ form an SCC. See Figure 5-right.

Thus, $a_i$ is forcibly instantiated to $i$ and the explanation is

$$ \bigwedge_{z \in \{a_j | i+1 \le j \le k-1\} \cup \{x, y\}} (\llbracket z \ge 0 \rrbracket \wedge \llbracket z \le k+\ell \rrbracket \wedge \bigwedge_{v \in \{1, \dots, i\} \cup \{k, \dots, k+\ell-1\}} (\llbracket z \neq v \rrbracket) \to \llbracket a_i = i \rrbracket $$

So, a number of $(k-i+1) \times (2+i+\ell)$ arcs are generated in $\Omega((k-i)(i+\ell))$ time. Because $\sum_{i \in \{1, \dots, k-1\}} (k-i) \times (i+\ell) = \Omega(k^2(k+\ell))$, $\Omega(k^2(k+\ell))$ time is spent generating factorised graph explanations down the branch. Finally, the number of variables for the `ALLDIFFERENT` constraint is $r=k+1$, so $k = \Omega(r)$. And the initial number of distinct values is $d = k+\ell+1$, so $k+\ell = \Omega(d)$. Therefore, the worst-case time complexity of generating factorised graph explanations is $\Omega(r^2 d)$ down a branch. ◀

## C Lower-Bound Proofs for CUMULATIVE

To establish lower bounds on the worst-case time complexity of generating big-step and pointwise explanations for `CUMULATIVE`, we construct infinite families of CSPs that each contain a `CUMULATIVE` constraint. In these families, either the number of tasks $n$, or both $n$ and the size of the time interval $|\Delta|$ can grow independently, depending on the parametrisation of the theoretical bound.

**Proof of the lower bound in Theorem 7.** Let $(BS_k^C)_{k \in \mathbb{N}_{>0}}$ be a family of CSPs defined as follows (see Figure 6-left). Let $k \in \mathbb{N}_{>0}$, the CSP $BS_k^C$ is made of:

- A set $F^L$ of $k$ fixed long tasks starting at time 0, of duration $k$ and height 1;

- A set $F^S = (f_i^S)_{0 \le i < \frac{k}{2}}$ of $\lfloor \frac{k}{2} \rfloor$ fixed short tasks such that $f_i^S$ starts at time $2i$, has duration 1 and height 1;

- A set $U$ of $k$ unfixed tasks starting at time 0 or later, of duration 1 and height 2;

- A constraint `CUMULATIVE$(F^L \cup F^S \cup U, k+1)$.
<figure><img src="image_9.png" /><figcaption>■ **Figure 6** Illustration of the initial profile of $BS_k^C$ (left) and $PW_{k,d}$ (right) for arbitrary $k, d \in \mathbb{N}_{>0}$</figcaption></figure>

For each task $u$ in $U$, one call to the time-table propagator iteratively sets the lower bound of the starting time of $u$ to 1, then to 2, and so on until $k$ because the profile is made of $k$ steps. A big-step explanation of size $\Omega(k)$ is computed for each one of these bound updates. So, the time spent generating big-step explanations is $\Omega(k^3)$. The number of tasks is $n = 2k + \lfloor \frac{k}{2} \rfloor$, so $k = \Omega(n)$. Therefore, the worst-case time complexity of generating big-step explanations is $\Omega(n^3)$ for a single propagator call. ◀

**Proof of the lower bound in Theorem 8.** Let $(BS_{k,d}^B)_{k,d \in \mathbb{N}_{>0}}$ be a family of CSPs defined as follows (see Figure 7). Let $k, d \in \mathbb{N}_{>0}$, the CSP $BS_{k,d}^B$ is made of:

- A set $F$ of $k$ fixed tasks starting at time $d-1$, of duration $d$ and height 1;

- A set $U$ of $k$ unfixed tasks starting between 0 and $2d-1$, of duration $d$ and height 1;

- A task $t$ starting between 0 and $d-1$, of duration $d$ and height 1;

- A constraint CUMULATIVE($F \cup U \cup \{t\}, k+1$);

- A set $B = (b_i)_{i \in \{1, \dots, d-1\}}$ of $d-1$ boolean variables;

- A constraint $b_i \implies s_t \ge i$ for all $i \in \{1, \dots, d-1\}$.

Let us say the search consists in branching first on the boolean variables in increasing index order by setting them first to true. During initial propagation, all the tasks in $F$ have a mandatory part of height 1 between $d-1$ and $2d-1$ while $t$ has a mandatory part of height 1 between $d-1$ and $d$. Therefore, the lower bound of the starting time of each task in $U$ is updated and set to $d-1$. A big-step explanation of size $\Omega(k)$ is generated for each bound update. The fix point for the Time-Table propagator is reached by a single call. Then, the search sets $b_1$ to true and the mandatory part of $t$ is now between $d-1$ and $d+1$. The lower bounds are then updated again and big-step explanations are generated. This process is repeated over the whole branch. A number of $k$ big-step explanations of size $\Omega(k)$ are generated at each node down a branch made of $d-1$ nodes. Thus, the time spent generating big-step explanations is $\Omega(k^2 d)$.

The number of tasks is $n = 2k+1$, so $k = \Omega(n)$. The size of the time interval is $|\Delta| = 3d-1$, so $d = \Omega(|\Delta|)$. Therefore, the worst-case time complexity of generating big-step explanations is $\Omega(n^2 |\Delta|)$ down a branch. ◀

<figure><img src="image_10.png" /><figcaption>■ **Figure 7** Illustration of the evolution down a branch of the profile of $BS_{k,d}^B$ for arbitrary $k, d \in \mathbb{N}_{>0}$</figcaption></figure>
**Proof of the lower bound in Theorem 9.** Let $(PW_{k,d})_{k,d \in \mathbb{N}_{>0}}$ be a family of CSPs defined as follows (see Figure 6-right). Let $k, d \in \mathbb{N}_{>0}$, the CSP $PW_{k,d}$ is made of:

- A set $F$ of $k$ fixed tasks starting at time 0, of duration $d$ and height 1;

- A set $U$ of $k$ unfixed tasks starting between 0 and $d$, of duration 1 and height 1;

- A single constraint CUMULATIVE($F \cup U, k$).

One call of the time-table propagator updates all the lower bounds of the starting times of the tasks in $U$, setting them to $d$. For each task $u$ in $U$, pointwise explanations are generated for all of the $d-1$ timepoints between 0 and $d$ because $u$ has duration 1. Each one of these explanations is of size $\Omega(k)$. So, the time spent generating pointwise explanations is $\Omega(k^2 d)$. The number of tasks is $n=2k$, so $k = \Omega(n)$. The size of the time interval is $|\Delta| = d+1$, so $d = \Omega(|\Delta|)$. Therefore, the worst-case time complexity of generating pointwise explanations is $\Omega(n^2 |\Delta|)$ for a single propagator call, and then also $\Omega(n^2 |\Delta|)$ down a branch. $\quad$

**Proof of the lower bound in Theorem 10.** Let $k \in \mathbb{N}_{>0}$, and let $BS_k^C$ be the CSP defined previously. A factor and its reason are created for each rectangle. The number of rectangles is $\Omega(k)$ and the size of each reason is $\Omega(k)$. So, this takes $\Omega(k^2)$ time. Also, we have $k = \Omega(n)$. Therefore, the worst-case time complexity of generating factorised big-step explanations is $\Omega(n^2)$ for a single propagator call. $\quad$

**Proof of the lower bound in Theorem 11.** Let $k, d \in \mathbb{N}_{>0}$, and let $PW_{k,d}$ be the CSP defined previously. A factor and its reason are created for each timepoint between 0 and $d$, which takes $\Omega(kd)$ time. Also, we have $k = \Omega(n)$ and $d = \Omega(|\Delta|)$. Therefore, the worst-case time complexity of generating factorised pointwise explanations is $\Omega(n|\Delta|)$ for a single propagator call. $\quad$