Keywords

1 Introduction

Nogood recording is a learning technique that has been applied to the Constraint Satisfaction Problem (CSP) in the 90’s [2, 4, 14]. A classical nogood is defined as a partial instantiation that cannot be extended into a solution. Such nogoods have been cleverly exploited to manage explanations [5, 7] of values that are deleted during search (when running constraint propagation). They have also been generalized [8] by incorporating both assigned variables (positive decisions) and refuted values (negative decisions). More recently, the practical interest of nogood recording has been revisited in the context of lazy clause generation [3].

Nogoods can also be effective in the context of a backtrack search algorithm that regularly triggers restarts. Indeed, just before restarting, a set of nogoods can be easily identified [10] on the rightmost branch of the search tree, which stands for the part of search space that has been explored during the last run. By recording these so-called nld-nogoods, we obtain the guarantee of never exploring the same subtrees, further making the approach complete. This restart-based learning mechanism has been extended to take into account symmetry breaking [11, 13] and the increasing nature of nld-nogoods [12], called increasing-nogoods for this reason.

In this paper, we propose several mechanisms to combine increasing-nogoods, allowing us to increase their filtering capacity. By dynamically analyzing relevant subsets of increasing-nogoods, especially from equivalence forms between decisions, we show that the search space can be more efficiently pruned. More specifically, we introduce three inference rules for deeper reasoning with increasing-nogoods.

2 Preliminaries

A constraint network P is a pair \(\mathcal {(X,C)}\), where \(\mathcal {X}\) is a finite set of variables and \(\mathcal {C}\) a finite set of constraints. Each variable \(x \in \mathcal {X}\) has a domain, denoted by dom(x), which is the finite set of values a that can be assigned to x. Each constraint \(c \in \mathcal {C}\) involves an ordered set of variables, called the scope of c and denoted by scp(c). A constraint c is semantically defined by a relation, denoted by rel(c), which is the set of tuples allowed by (variables of) c. Let \(X \subseteq \mathcal {X}\) be a subset of variables, an instantiation I of X maps each variable \(x \in X\) to a value in dom(x); we note \(I[x]=a\) and \(vars(I)=X\). An instantiation I is complete iff \(vars(I)=\mathcal {X}\), partial otherwise. A solution of P is a complete instantiation satisfying all constraints of P.

A nogood is an instantiation that cannot be extended to any solution. The benefit of recording nogoods is to avoid some form of thrashing, i.e. exploring the same unsatisfiable subtrees several times. There are two classical methods to identify and store nogoods: during search or at restarts. In this paper, we consider a complete backtrack search algorithm with binary branching and nogood recording from restarts [9]. Decisions taken during search are either positive (i.e., variable assignments such as \(x=a\)) or negative (i.e., value refutations such as \(x \ne a\)). A decision \(\updelta \) is checked to be positive or negative by simply writing \(pos(\updelta )\) and \(neg(\updelta )\), respectively. The variable involved in a decision \(\updelta \) is denoted by \(var(\updelta )\), whereas the value involved in a decision \(\updelta \) is denoted by \(val(\updelta )\). Binary branching means that at each search node a left branch labeled with a positive decision \(x=a\) is developed first, and a right branch labeled with a negative decision \(x \ne a\) is developed next. A decision \(\updelta \) is satisfied (resp., falsified) iff it holds (resp., does not hold) whatever is the value chosen in the current domain of \(var(\updelta )\). A decision that is not satisfied (resp., falsified) is said to be unsatisfied (resp., unfalsified).

3 Increasing Nogoods

So-called nld-nogoods [9] (negative last decision nogoods) can be extracted at each restart of a backtrack search algorithm. Let us assume that the sequence of labels all along the rightmost branch of a current search tree being developed is \(\Sigma = \langle \updelta _{1}, \ldots , \updelta _{m} \rangle \), where each decision of \(\Sigma \) is either a positive or a negative decision. It is known that for any i such that \(1 \le i \le m\) and \(neg(\updelta _i)\), the set \(\{ \updelta _j : 1 \le j < i \wedge pos(\updelta _j)\} \cup \{\lnot \updelta _{i}\}\) is a reduced nld-nogood. Note that it only contains positive decisions (and so, is a standard nogood). From now on, for simplicity reasons, we simply call them nld-nogoods.

Fig. 1.
figure 1

The search tree at the end of a run.

Example 1

Let us consider the search tree depicted in Fig. 1, where the rightmost branch of the tree is \(\Sigma = \{\updelta _{1} , \lnot \updelta _{2} , \lnot \updelta _{6} , \updelta _{8} , \lnot \updelta _{9} , \lnot \updelta _{11} \}\). The following (reduced) nld-nogoods can be extracted: \(\{\updelta _{1} , \updelta _{2}\}\), \(\{\updelta _{1} , \updelta _{6}\}\), \(\{\updelta _{1} , \updelta _{8} , \updelta _{9}\}\) and \(\{\updelta _{1} , \updelta _{8} , \updelta _{11} \}\).

As we can observe, there are some similarities between these nld-nogoods: they are said to be increasing [12, 13]. An increasing-nogood compactly represents the full set of nld-nogoods that can be extracted from a branch. To obtain an increasing-nogood from a set of nld-nogoods, we have first to consider each nld-nogood under its directed form.

Example 2

Considering again the search tree in Fig. 1, let us assume the decisions of the last branch represent: \(\Sigma = \langle x_{2} = 1,\ x_{3} \ne 0,\ x_{4} \ne 1,\ x_{5} = 2,\ x_{1} \ne 1,\ x_{6} \ne 2 \rangle \). The four nld-nogoods \(ng_0\), \(ng_1\), \(ng_2\) and \(ng_3\) are given below under their logical forms (middle) and directed forms (right):

In [12], the authors have shown that the set of directed nld-nogoods extracted from a branch are necessarily increasing, meaning that \(\mathtt {LHS}(ng_{i}) \subseteq \mathtt {LHS}(ng_{i+1})\) where LHS designates the left hand side of the implication. This is illustrated on our example by:

In practical terms, it means that it suffices to record the branch exactly as it is instead of extracting nld-nogoods independently. Another important observation is that each increasing-nogood can be viewed as a constraint, together with a filtering algorithm enforcing GAC (Generalized Arc Consistency). Interestingly enough, if \(\langle ng_{1}, \ \cdots , ng_{t} \rangle \) is a sequence of increasing nld-nogoods, and if \(LHS(ng_{i})\) contains two unsatisfied decisions then any nogood \(ng_{j}\) with \(j \ge i\) is necessarily GAC because the LHS of larger nogoods subsume the LHS of smaller ones.

Technically, two indices \(\upalpha \) and \(\upbeta \) can be used to watch the two leftmost unsatisfied positive decisions in the sequence of an increasing-nogood. These two watched decisions as well as all the negative decisions that may occur between them are under surveillance, as \(\updelta _1\), \(\lnot \updelta _2\) and \(\updelta _3\) in the following illustration:

For the sake of simplicity, we consider that for any increasing-nogood \(\Sigma \), the decisions in \(\Sigma \) that are watched by the alpha and beta indices can be respectively accessed by using \(\upalpha (\Sigma )\) and \(\upbeta (\Sigma )\). On our illustration, \(\upalpha (\Sigma )\) and \(\upbeta (\Sigma )\) are respectively \(\updelta _1\) and \(\updelta _3\).

The filtering algorithm (called IncNG) associated with an increasing-nogood (constraint) is triggered in three cases:

  1. 1.

    a watched negative decision is falsified: \(\upalpha (\Sigma )\) must be forced to be falsified, and consequently all nogoods within the constraint are satisfied;

  2. 2.

    \(\upalpha (\Sigma )\) is satisfied: all negative decisions between \(\upalpha \) and \(\upbeta \) must be satisfied and we search for the next unsatisfied positive decision;

  3. 3.

    \(\upbeta (\Sigma )\) is satisfied: we need to find the next unsatisfied positive decision.

4 Reasoning with Increasing Nogoods

When considered as constraints, it is quite natural that nld-nogoods and increasing-nogoods are solicited independently for filtering tasks. However, we show that it is possible to exploit the similarities that exist (rather frequently) between such nogoods. More specifically, we introduce in this section three rules for reasoning deeper with increasing-nogoods.

4.1 Reasoning with Watched Negative Decisions

By checking for each variable x and each increasing-nogood \(\Sigma \) that there exists a value in dom(x) which is not involved in a negative decision for x between \(\upalpha (\Sigma )\) and \(\upbeta (\Sigma )\), we have the guarantee of not missing some inferences from a simple reasoning on watched negative decisions.

Example 3

Consider the following increasing-nogood: \(\Sigma = \langle x_{2} = 1, x_{3} \not = 2, x_{3} \not = 4, x_{5} = 3 \rangle \). Assume that we have \(\upalpha (\Sigma )\) and \(\upbeta (\Sigma )\) being indices for \(x_{2} = 1\) and \(x_{5} = 3\), and all variables with the same domain \(\{1, 2, 3, 4\}\). If \(x_{2}\) is assigned to the value 1, then the values 2 and 4 can be removed from \(dom(x_{3})\). Of course, a conflict occurs if \(dom(x_{3})\) only contains these two values. However, this conflict could have been avoided (anticipated) by removing the value 1 from \(dom(x_{2})\) as soon as \(dom(x_{3})\) is reduced to \(\{2,4\}\). \(\square \)

First, we introduce a function \(\mathtt {diffValues}(\Sigma , x_i)\) that returns for a given increasing-nogood \(\Sigma \), the set of values present in a negative decision of \(\Sigma \) involving \(x_i\) and situated between \(\upalpha (\Sigma )\) and \(\upbeta (\Sigma )\). We also introduce a function \(\mathtt {diffVars}(\Sigma )\) that returns the set of variables involved in a negative decision of \(\Sigma \) situated between \(\upalpha (\Sigma )\) and \(\upbeta (\Sigma )\). For example, for \(\Sigma = \langle x_{2} = 1, x_{3} \not = 2, x_{3} \not = 4, x_{5} = 3 \rangle \) with \(\upalpha (\Sigma )\) being \(x_{2} =1\) and \(\upbeta (\Sigma )\) being \(x_{5}=3\), we have \(\mathtt {diffVars}(\Sigma ) = \{ x_{3} \}\) and \(\mathtt {diffValues}(\Sigma , x_{3}) = \{ 2, 4 \}\). Algorithm 1 implements this way of reasoning, i.e. performs an inference by refuting the value involved in \(\upalpha (\Sigma )\), each time a conflict can be anticipated as discussed above. Even if increasing-nogoods are still reviewed independently (in turn), the filtering capability of the algorithm proposed in [12] is clearly improved if this simple procedure is systematically called. The worst-case time complexity of Algorithm 1 is \(\mathcal {O}(nd)\) where n is the number of variables and d is the size of the largest domain. Indeed, we can precompute sets \(\mathtt {diffVars}(\Sigma )\) and \(\mathtt {diffValues}(\Sigma , x)\) by scanning the decisions in \(\Sigma \) whose size is O(nd). With these precomputed sets, executing lines 1–2 is also in O(nd).

figure a

4.2 Combining Increasing Nogoods of Similar \(\upalpha \)

In this section, we extend the principle presented above to sets of increasing-nogoods. For this purpose, we partition the set of increasing-nogoods according to the decisions indexed by \(\upalpha \): two increasing-nogoods \(\Sigma _i\) and \(\Sigma _j\) are in the same group iff \(\upalpha (\Sigma _i)\) is the same decision as \(\upalpha (\Sigma _j)\). Of course, it is therefore necessary to update the partition each time one \(\upalpha \) is modified (i.e., when filtering and backtracking). Despite that, reasoning about groups of increasing-nogoods allows us to improve the filtering capacity of the increasing-nogoods, and turns out to encompass the previous case.

Example 4

Let us consider the three following increasing-nogoods:

and let us assume that all variables have the same domain \(\{0,1,2,3\}\). On this example, we can observe that \(x_{2} = 1\) is the common \(\upalpha \) to this group of three increasing-nogoods. By looking at the negative decisions following these three occurrences of \(\upalpha \) (the precise values of \(\upbeta \) are not relevant for our illustration), we can collect \(\{0,1,2\}\) as values involved in watched negative decisions for \(x_3\) (they are necessarily put before \(\upbeta \) which is not represented here). This means that if \(x_{2}\) is assigned the value 1 then the only remaining value in \(dom(x_{3})\) will be 3. On the other hand, if at a certain moment, the domain of \(x_3\) does not contain anymore the value 3, it is absolutely necessary to prevent \(x_{2}\) from being assigned the value 1. \(\square \)

figure b

Algorithm 2 is a generalization of Algorithm 1, by considering groups of increasing-nogoods instead of increasing-nogoods individually. Algorithm 2 has a worst-case time complexity in \(\mathcal {O}(nd + g)\) where g is the sum of the size of the increasing-nogoods in \(\Sigma \)s (we have \(g = \sum _{\Sigma \in \Sigma s} |\Sigma |\)). Indeed, precomputing sets \(\bigcup _{\Sigma \in \Sigma s} \mathtt {diffVars(\Sigma )}\) and \(\bigcup _{\Sigma \in \Sigma s} \mathtt {diffValues}(\Sigma ,x)\) can be performed in O(g) by scanning every decision in the increasing-nogoods of \(\Sigma \)s. With these precomputed sets, executing lines 1–2 is in O(nd).

4.3 Combining Increasing Nogoods Using Pivots

We call pivot a variable x such that for any value \(a \in dom(x)\) there exists an increasing-nogood \(\Sigma \) such that \(\upalpha (\Sigma )\) is the positive decision \(x = a\); in that case, we say that \(\Sigma \) is a support of pivot x for a. Interestingly, once a pivot variable x is identified, it is possible to infer negative decisions that are shared by all supports of x. This is the principle of the algorithm we present after an illustration.

Example 5

Let us consider the following three increasing-nogoods:

and let us assume that all variables have the same domain \(\{0,1,2\}\). On this example, we can see that \(x_2\) is a pivot since all its possible values are involved in \(\upalpha \) of different increasing-nogoods. As \(x_{3} \ne 1\) is a negative decision that is watched in the three increasing-nogoods, we can deduce that \(x_{3}\) must always be different from 1. \(\square \)

Algorithm 3 implements the use of pivot variables for making additional inferences. Line 1 only iterates over the variables that are involved in some \(\upalpha \) (i.e., \(\upalpha \) of some increasing-nogoods). Line 2 tests if the variable x is indeed a pivot. Line 3 iterates over the decisions that are shared by all supports of x. Each such decision must be forced to be satisfied. Note that an optimization consists in only checking that a decision is shared by some subsets of supports of x, the subsets with exactly one support of x for each value. Algorithm 3 has a worst-case time complexity in \(\mathcal {O}(n^2dp)\) where p is the number of increasing-nogoods.

figure c
Fig. 2.
figure 2

Pairwise comparison (CPU time in seconds) of IncNG and IncNG+. Results obtained on the 3,744 instances used as benchmarks. The timeout to solve an instance is set to 900 s.

Table 1. Average results on 15 series of instances (timeout set to 900 s).

5 Experiments

We have conducted an experimentation on a computer Intel Xeon X5550 clocked at 2,67 GHz and equipped with 8 GB of RAM. Our initial benchmark was composed of all instances that were used during XCSP 2.1 solver competitions. We discarded the series of instances that were either too easy to solve (less than 1 s) or too hard to solve (more than 900 s) when employing MAC without nogood recording; this yielded a set composed of 3,744 instances. For our experiments, we have used the solver rclCSP introduced in [6]. The variable ordering heuristic is dom/wdeg [1] and the restart policy corresponds to a geometric series of first term 10 and common ratio 1.1. Given the complexity of Algorithm 3 and because Algorithm 1 is generalized by Algorithm 2, we chose to conduct our experiments with only Algorithm 2 (combining increasing-nogoods of similar \(\upalpha \)). For our comparison, we tested three methods: NRR (nogood recording from restarts as proposed in [12]), IncNG (managing increasing-nogoods as proposed in [10]) and IncNG+ (combining increasing-nogoods, our approach as introduced in Sect. 4.2). Figure 2 displays the overall results that we have obtained. The scatter plot shows that our approach (IncNG+) has usually a small overhead (when it turns out to be not very effective), and interestingly makes search a little bit more robust (see the dots on the right vertical line that corresponds to unsolved instances by IncNG). Table 1 shows a detailed comparison between the three methods on some series. The table contains the following information: the name of the series, the number of instances in the series (#inst) and for the three tested approaches, the number of solved instances (#sols) and the PAR10 score that is the average of the runtimes while considering 10 times the timeout (900) for unsolved instances. In general, our approach (IncNG+) solves at least as many instances as IncNG and sometimes more (see, for example, super-jobShop). When IncNG and IncNG+ both solve the same number of instances, we usually notice a slight loss for our approach due to the management of the partitions of the increasing-nogoods (for example, see frb45-21). But interestingly, there are series where this processing time is compensated by a better pruning of the search tree, with a substantial time saving as outcome (rand-2-50-23). Moreover, we observe that, in general, the more difficult the instance is, the more competitive our approach is, as illustrated by the QWH-20 and QWH-25 series which admit increasing sizes and complexities.

6 Conclusion

In this paper, we have introduced three general rules allowing us to reason with (groups of) increasing-nogoods. We have shown experimentally the practical interest of the second rule (which generalizes the first one): when it is effective, i.e., when inferences can be performed by reasoning on groups of increasing-nogoods, it saves computation time, and when it is not effective, the overhead is rather limited. We believe that some improvements are still possible, especially on the exploitation of pivot variables.