Conflict Analysis Based on Cutting-Planes for Constraint Programming

A constraint satisfaction problem (CSP) is a triple $(𝒳,𝒟,𝒞)$, where:

• $\mathrm{■}$

  $x\in 𝒳$ is a decision variable,

• $\mathrm{■}$

  $𝒟(x)\in 𝒟$ with $x\in 𝒳$ is the domain of $x$, i.e. the set of values $x$ can be assigned to,

• $\mathrm{■}$

  and $C\in 𝒞$ is a constraint: a predicate over the variables that is either satisfied or violated.

We use range notation when the domain is a uninterrupted sequence of integers: $[l,u]=\left\{i\right|l\le i\le u\}$.

An assignment is a total function $\theta$ that maps every variable $x\in 𝒳$ to a set $V\subseteq 𝒟(x)$. If $|\theta (x_i)|>1$, i.e. there is more than one possible value for $x_i$, then the assignment is referred to as a partial assignment. Otherwise, the assignment is called total. In this paper, unless we explicitly use the term “partial assignment”, we refer to a total assignment. We abuse notation to say that $\theta (x)=v$ with $v\in \mathbb{Z}$ to mean that $\theta (x)=\left\{x\right\}$. If the assignment $\theta$ satisfies all the constraints in $𝒞$, then $\theta$ is called a solution. In this paper, we restrict ourselves to integer decision variables, i.e. $\forall x\in 𝒳:𝒟(x)\subset \mathbb{Z}$, and we assume the domains are finite.

Constraint Programming (CP) is a paradigm for solving CSPs. CP solvers combine inference and search to find solutions to a CSP. The inference prunes the domain based on the constraints in the problem, and once no more inference can be done, the search splits the problem into subproblems to be solved independently. A conflict happens when there exists a variable $x\in 𝒳$ such that $𝒟(x)=\mathrm{\varnothing }$.

In a CP solver, constraints are enforced by propagators. A propagator is a function $p:𝒟\mapsto 𝒟$ that takes the domain and removes values that do not exist in a solution. This means that $p(𝒟)⊑𝒟$, where ${𝒟}_1⊑{𝒟}_2$ denotes that ${𝒟}_1$ is stronger than ${𝒟}_2$, i.e. for every $x\in 𝒳$ it is the case that ${𝒟}_1(x)\subseteq {𝒟}_2(x)$. We highlight two types of constraints and their propagators.

• $\mathrm{■}$

  A clause, which is a disjunction of Boolean variables. It has the form $l_1\vee \mathrm{\cdots }\vee l_n$, where every $l_i$ has a Boolean domain $𝒟(l_i)=\{0,1\}$. This constraint requires at least one $l_i$ to be $1$. The propagator for a clause waits until $n-1$ variables are fixed to $0$, and then sets the final variable to $1$.

• $\mathrm{■}$

  A linear inequality (also referred to as linear constraint in this paper) has the form ${\displaystyle \sum w_i{x}_i}\le c$, where $w_i\in \mathbb{Z}$ and $c\in \mathbb{Z}$ are constants, and $x_i\in 𝒳$ are decision variables. The propagator for this constraint performs bound propagation [5], as shown in 1.

  Example 1.

  Let $x,y$ be integer decision variables with domains $𝒟(x)=[1,5]$ and $𝒟(y)=[0,2]$. The propagator for the constraint $x+2y\ge 7$ can remove the values $1$ and $2$ from $𝒟(x)$ and the value $0$ from $𝒟(y)$, because there are no solutions where $x=2$ or $y=0$.

An Integer Linear Program (ILP) is a CSP in which all constraints are linear inequalities. Given two linear constraints $A:a_1{x}_1+\mathrm{\cdots }+a_n{x}_n\le a_0$ and $B:b_1{x}_1+\mathrm{\cdots }+b_n{x}_n\le b_0$, their linear combination results in a new linear constraint $C:c_1{x}_1+\mathrm{\dots }{c}_n{x}_n\le c_0$ with $c_i=\alpha a_i+\beta b_i$ that is implied by $A\wedge B$. In the case where $c_i=0$, we say that $x_i$ has been eliminated. Note that we can always pick an $\alpha$ and $\beta$ such that $c_i=0$ when , i.e., when the coefficients of the variable to be eliminated $x_i$ have opposite signs in $A$ and $B$.

The combination rule can be used by solvers like IntSat [27], which are inspired by Conflict-Driven Clause Learning (CDCL) [22]. IntSat keeps a trail of bounds in the form $⟨x\diamond v⟩$, with $\diamond \in \{\le ,\ge \}$, that iteratively tighten the domain of the variables.

1 presents the pseudo-code for the conflict analysis procedure. Just like propositional CDCL, the trail gets traversed backwards. For every entry, it is checked whether reason constraint $RC$ can be combined with the conflicting constraint $CC$ to eliminate propagated variable $V$ (lines 5 and 6). This elimination is feasible only if $V\in CC$ and the signs of the coefficients of $V$ in $CC$ and $RC$ are opposite. If these conditions are met, the reason constraint $RC$ is combined with the conflicting constraint $CC$ (line 7). This process is repeated until the resulting constraint $CC$ can propagate at an earlier decision level (asserting), or the previous decision is reached.

A notable difference with propositional CDCL, is that 1 may fail to derive a linear constraint that is asserting at a prior decision level. In such cases, the solver resorts to performing resolution on bounds as a fallback strategy, similar to LCG conflict analysis (see next section), which is the clausal counterpart of linear combinations.

The reason for the inability to construct an asserting linear constraint is the rounding problem, which is illustrated by 2 (adapted from [27, Example 3.1]). As a consequence, linear conflict analysis can generate implied constraints that are not conflicting under the current partial assignment, even though the constraint that identified the conflict initially was conflicting with this assignment.

A CDCL-inspired ILP solver has to deal with the situation from 2 in some way. In Section 3 we highlight different approaches taken by various solvers.

Lazy Clause Generation [28, 38] (LCG) is an approach to solving CSPs within the CP paradigm. It combines the domain propagation capabilities of CP solvers with the clause learning capabilities of SAT solvers.

There are two main parts to the integration. The first is the representation of the decision variables in a propositional formula. This is done by creating Boolean variables that map to unary constraints of the following form: $⟨x\diamond v⟩$, where $x\in 𝒳$, $\diamond \in \{\le ,\ge ,\ne ,=\}$, and $v\in \mathbb{Z}$. Such a unary constraint is called an atomic constraint. Every domain reduction in an LCG solver can be expressed by setting one or more atomic constraints to true.

The second part of the integration allows propagations done by propagators to be used during conflict analysis. Every propagation is explained by an implication ${\displaystyle \bigwedge l_i}⟹p$, where $l_i$ and $p$ are atomic constraints.

These explanations can be treated as clauses to integrate into the CDCL procedure, allowing the solver to learn clauses based on propagations done by propagators.

The conflict analysis algorithm employed by LLG closely resembles the one presented in 1, with several key modifications introduced in this section. The most notable distinction is that constraints are no longer exclusively linear. While the conflicting constraint $CC$ and the reason constraint $RC$ were previously guaranteed to be linear, conflicts and propagations must now be explained linearly for them to participate in conflict analysis. Unlike IntSat, there is no guarantee that $CC$ or $RC$ can actually be explained linearly, as certain linear explanations for propagations and conflicts may either be impractical or too expensive to create.

For example, we consciously do not convert clauses to linear inequalities, even though that is possible. Any clause $l_1\vee \mathrm{\cdots }\vee l_n$ with $l_i$ being atomic constraints can be turned into the linear inequality $l_1+\mathrm{\cdots }+l_n\ge 1$. However, contrary to many other LCG solvers, our implementation does not create 0-1 variables for atomic constraints in clauses. I.e., a clause is a set of atomic constraints rather than a set of Boolean variables. This means that converting the clause to a linear constraint would require creating auxiliary variables for all atomic constraints $l_i$. As will become clearer in Subsection 4.3, creating auxiliary variables is not cheap, and we would need a lot of them. Future work can explore an implementation where this is feasible.

Subsection 4.4 presents a few linear explanations, and Appendix A gives the complete list of constraints and explanations we implemented. Given that, our conflict analysis differs from IntSat (as displayed in 1) in the following areas:

1. 1.

   First, rather than directly retrieving the currently conflicting constraint from $𝒞$ (line 1), we attempt to derive a linear explanation for the conflict. Either the conflict is explicitly identified by a propagator and described as a linear inequality, in which case $CC$ is set to that linear inequality. Alternatively, the domain of a variable $x$ became empty. In that case, the linear inequality $Ax\le b$ explaining the last propagation on $x$ is conflicting, so it is used as the conflicting constraint.

   If we cannot express the conflict with a linear constraint, then we proceed to the resolution fallback (line 14). A common example when this happens is when the conflicting constraint is a clause.

2. 2.

   Similarly, instead of getting $RC$ directly from the trail (line 4), $RC$ becomes the linear explanation of the propagation. We also introduce an additional check: the combination step cannot proceed if we cannot create a linear explanation to assign to $RC$.

3. 3.

   Finally, if we fail to learn an asserting linear constraint, we fall back to resolution just as IntSat does (line 14). The difference here is that IntSat does not remember clauses because it does not have a clausal propagator, so it just propagates the learned clause once and forgets about it. In our CP solver, we have a clausal propagator, so we remember the clause. Effectively, if we cannot learn an asserting linear inequality, the conflict analysis operates as a standard LCG conflict analysis does.

A fundamental aspect of LLG is constructing linear inequality explanations for propagations. This section elaborates on several key aspects of constructing these explanations.

The auxiliary variables associated with conditional explanations cannot be constructed before starting the search procedure, as it is unknown which auxiliary variables will be necessary. Thus, they must be introduced and propagated during the search. A key challenge is maintaining a consistent solver state at decision levels where these variables did not exist yet.

We have formulated linear explanations for several arithmetic constraints and the element global constraint. This section provides a detailed exposition of some of these explanations. A comprehensive overview of all explanations is presented in Appendix A. These explanations can closely resemble a lazy decomposition, where linear inequalities are added to the model lazily. However, when we refer to inequalities as explanations, we explicitly mean that we do not add the inequalities to the model.

The instances we used to evaluate our LLG implementation are drawn from the MiniZinc Challenges 2008-2024 [36, 34] and the MiniZinc Benchmarks¹¹1https://github.com/MiniZinc/minizinc-benchmarks. Models with unbounded or floating-point domains were excluded, as well as models without a specified search heuristic. Instances from the MiniZinc challenge which are not solved by at least one finite-domain solver are also excluded. For every model with more than 10 instances, we sampled 10 instances randomly.

Each instance is decomposed into the following constraints: multiplication ($a\times b=c$), truncating division ($a/b=c$), absolute value ($a=|b|$), maximum ($max(A)=b$), not equals ($Ax\ne b$), linear less-than-or-equal-to ($Ax\le b$), reified ($p\to constraint$), element ($A[idx]=b$) and clauses. The explanations for these constraints are given in Appendix A.

This results in a dataset of 952 instances based on 223 unique models. These instances result in roughly $\mathbf{50.5}𝐌$ linear inequalities, $\mathbf{18.4}𝐌$ reified constraints, $\mathbf{3.7}𝐌$ not-equals constraints, $\mathbf{1.3}𝐌$ multiplication constraints, $\mathrm{𝟔𝟓𝟒}𝐤$ element constraints, $\mathrm{𝟒𝟏𝟕}𝐤$ maximum constraints, only $\mathbf{4.5}𝐤$ absolute and only $\mathbf{1.4}𝐤$ division constraints.

All experiments were conducted on the DelftBlue [10] compute cluster. Each run used a single thread of an Intel Xeon E5-6248R 24C 3.0GHz and had access to 8GB of memory. The time limit was set to 1 hour per instance.

The first experiment shows how LLG impacts the number of conflicts encountered compared to the LCG baseline. We can break down the instances into three categories:

1. 1.

   There are 328 instances that timed out or ran out of memory for LLG. This is compared to 289 in the LCG solver. That is an increase, however, the instances for which this happens are different between the two solvers. I.e., the LLG solver times out or errors on different instances than the LCG solver. In many of these instances, the LLG solver does learn linear constraints, but their impact is not big enough to prevent a time-out.

2. 2.

   Then, there are 181 instances that are solved by the LLG solver, but not a single linear inequality was learned. In these instances, even though LLG has the overhead of cutting-planes reasoning, that overhead did not prevent the solver from terminating within the time-out.

3. 3.

   The final 443 instances are solved within the time limit, and at least one linear inequality is learned. Figure 1 aggregates the ratio of the number of conflicts for LLG relative to LCG. The lower half of the distribution exhibits significant reductions, with a decrease in conflicts of up to 60% for a quarter of the instances, even increasing to over 90% when looking at the top 10% of instances. Then, the Q2 to Q3 quartile indicates that in roughly a quarter of the completed instances, the number of conflicts is reduced only slightly. For these instances, LLG learns very few linear constraints, or learns linear constraints that propagate similar bounds as learned clauses. Lastly, the upper 75% to 90% percentile range highlights cases where the number of conflicts increases marginally. This is due to some learned constraints being weaker compared to the clauses that would have been learned by the LCG solver.

These numbers show that, with the current state of LLG, not all instances benefit from its linear conflict analysis. However, when a linear inequality is derived, it has the potential to massively reduce the number of conflicts. We initially assumed that the top-performing instances would be derived from a limited subset of models that fit LLG especially well. However, upon examining the instances exhibiting at least a 50% reduction in conflicts, we identify 117 instances originating from 52 models ($117/52\approx \mathbf{2.3}$ instances per model). In comparison, a total of 574 instances from 171 models successfully complete for both LCG and LLG ($547/165\approx \mathbf{3.3}$ instances per model): the top-performing instances are even more varied than the full dataset. Consequently, our assumption was wrong; particular models are not more suitable for LLG than others.

The distribution of constraints across these instances also seems highly variable. The successful instances exhibit a slightly higher percentage of linear inequality constraints, though the difference is within only a few percent.

Lastly, although the implementation of the LLG solver can be improved on many fronts, we observe that for the top 25% of instances – each achieving at least a 60% reduction in conflicts – runtime performance already surpasses our baseline LCG, owing to the significant decrease in conflicts of LLG. Specifically, for this subset of instances (excluding those with execution times below 5 seconds), the median runtime improvement is 75%.

The motivation for LLG is based on the proposition that linear constraints may provide stronger reasoning than clauses. With this experiment, we show that the theoretical benefit translates to practice. For the 443 completed instances with at least one learned inequality, we examine whether the learned inequality indeed propagates more often than the clause that would have been learned in its place.

The results indicate that when a linear constraint is learned, it replicates over 91% of the propagations that the fallback clause would have produced. In contrast, only 37% of the propagations triggered by learned linear constraints would have been replicated by the clause. This confirms that, in nearly all cases, the linear constraint is at least as strong as the fallback clause. This further suggests that neither conflict analysis method strictly dominates the other, yet learned linear constraints tend to be more general in practice.

We also observe that in a normal LLG execution, the majority of learned clauses do not propagate more than once. In contrast, the median number of propagations per learned learned inequality is 90. This demonstrates that when an inequality can be learned, it generally has a much greater impact on the search compared to a learned clause.

This experiment aims to illustrate the success rate of LLG analyses as the search progresses, and to identify reasons for failed analyses. Recall that a successful LLG analysis results in learning a linear constraint, whereas a failed analysis reverts to LCG for reasons such as a violated conflicting invariant. Here, it is relevant to compare successful instances with less successful instances. We divide the 624 instances that the LLG solver could finish into three subsets: all instances (Figure 2(a)), those with at least a 50% reduction in conflicts (Figure 2(b)), and those with at least a 75% reduction in conflicts (Figure 2(c)).

Firstly, Figure 2(a) demonstrates a declining trend in successful analyses over time, accompanied by an increase in conflicts and explanations that cannot be expressed linearly. This trend persists when results are categorized by the number of conflicts (comparing small and large instances) and by problem type (satisfaction versus optimization). The only correlation we can observe is the one between a decreasing LLG success rate and an increase in failed LLG analyses attributed to encountered clauses. Approximately 38% of LLG failures can be attributed to these factors. The remaining 62% consist of failures that occur at a relatively constant rate throughout the search, including invariant violations ($\approx 50\%$), combinations that fully cancel out ($\approx 6\%$), overflows ($\approx 3\%$), and cases where a decision is reached before identifying an asserting constraint ($\approx 3\%$).

In contrast, Figures 2(b) and 2(c) exhibit some differences compared to the full dataset. Initially, conflict analysis is highly successful – significantly more so than for the full dataset. However, as the search progresses, analysis performance declines sharply. For these instances, we can see that the number of analysis failures due to invariant violations increases substantially throughout the search. Figures 2(a) through 2(c) all illustrate that LLG conflict analysis succeeds in only a relatively small fraction of instances. This experiment demonstrates that even a relatively small number of learned linear constraints can significantly decrease the number of conflicts encountered.

Given the decreasing frequency of conflict analyses leading to newly learned linear constraints, it is worth exploring whether a similar pattern is observed in the propagation of learned constraints. Figure 2(d) plots the density function (area under the curve equals 1) of all propagations triggered by learned constraints, presented for the same three subsets of instances. The results indicate that, despite the decline in newly learned linear constraints, propagations of learned constraints increase over time. This indicates that, as the search progresses, previously learned linear constraints continue to propagate consistently.

In addition to comparing LLG with LCG, it is also valuable to evaluate Pumpkin’s decomposition as described in Section 5.1 against a decomposition consisting only of linear inequalities. This evaluation shows that using CP propagators – even though not all its linear explanations are equally successful – is still beneficial over a fully linear model. For this experiment, all instances from the test set were reformulated into a fully linear model using the MiniZinc Linear Library [4]. Among the 952 instances in the test set, 938 could be transformed into a linear model within a 300-second timeout. The 14 instances that could not be converted likely experienced excessive model growth when represented fully linearly.

For the 938 successfully converted instances, Figure 3(a) presents the ratio of conflicts between the linear decomposition (baseline) and LLG. The results indicate a substantial reduction in conflicts when using LLG. Specifically, at least 25% of the instances exhibit a conflict reduction of 50% or more. Furthermore, the first and second quartiles (Q1 to Q2) of the boxplot show a notable decline in conflicts, ranging from 50% to 8%. The second to third quartiles (Q2 to Q3) display a mix of reductions, from an 8% reduction to an increase of 20%. The remaining instances exhibit a slightly larger increase in conflicts.

These increases in conflicts can be attributed to two primary factors. Firstly, the preprocessing optimizations performed by the linear decomposition can result in the generation of smaller linear problem instances compared to those produced by Pumpkin’s decomposition. Secondly, some of Pumpkin’s propagators perform propagations that cannot be easily linearly explained, such as set or alldifferent propagations, whereas the linear decomposition provides alternative propagations that can be linearly explained more effectively. Nevertheless, LLG continues to exhibit a significant performance advantage over the linear decomposition.

Subsection 5.4 shows that as more clauses are encountered in the conflict analysis, the success-rate of the the linear conflict analysis drops. Therefore, we investigate the consequences of only propagating a learned clause once, without storing it in the constraint database. The results, presented in Figure 3(b), indicate that omitting clause storage leads to a significant increase in conflicts. This observation underscores that even though encountering clauses likely results in learning fewer linear inequalities, the effectiveness of LLG relies heavily on the ability to store and propagate learned clauses.

We note the clear parallel between this experiment and the standard behavior of IntSat [27]. However, two key distinctions differentiating the two approaches prevent an accurate comparison. First, IntSat operates solely on fully linear models, which inherently provide better linear explanations for propagations than a CP model can, increasing the success rate of IntSat’s conflict analysis. Second, IntSat tries to transform learned clauses into linear inequalities when at most one bound of the clause is non-binary. Within our CP problems, such conversions are rarely feasible due to the predominant use of integer variables. This limitation might change if the CP models were reformulated as linear programs.