Disjunctive Scheduling in Tempo

The Satisfiability problem is to decide if there exists an assignment of a set $𝒜$ of atoms such that a propositional logic formula $\phi$ evaluates to true, that is, whether there exists a solution to: $\exists 𝒜.\phi$. We shall use the symbol $a\in 𝒜$ to denote both the Boolean variable and the positive literal standing for this variable being true, while $\neg a$ is the negative literal, standing for this variable being false. It is often assumed that the formula $\phi$ is in Conjunctive Normal Form (CNF). A CNF is a conjunction of clauses, i.e., a disjunction of literals.

Conflict-driven Clause Learning (CDCL) solvers [34] make branching decisions as other tree search algorithms, by adding an arbitrary new true literal to the formula. However, when encountering a failure, instead of undoing the most recent decision, a conflict clause, or nogood, is generated and added to the clause set. Let $ℱ$ be the list, in chronological order, of literals currently true in some branch of the search tree, let $rk(l)$ be the rank of literal $l$ in $ℱ$ and let the explanation $(reason(l)⟹l)$ for $l$ be the clause that unit-propagated $l$ (and we call $reason(l)$ the reason for $l$). Conflict analysis usually computes a conflict clause with a unique implication point (UIP) whose rank is higher than or equal to that of the last decision. Let a conflict set $c$ be a conjunction of literals that entails unsatisfiability of the formula $\phi$, i.e., such that $\phi \wedge c\vDash \perp$. The conflict set is initialized as the negation of the clause that triggered the failure. Then the literal $l\in c$ with maximum rank $rk(l)$ is removed from $c$ and replaced by its reason $reason(l)$ until exactly one literal in $c$ has a rank superior or equal to that of the most recent decision (this literal is the first UIP, i.e., 1-UIP). This process is called conflict-driven clause resolution.²²2We define it using conflict sets because it is more intuitive and convenient, however, those are indeed resolution steps when adopting the clausal view. Then, every branching decision whose rank is higher than the highest rank of any literal in $c$ but the 1-UIP is undone, the conflict clause $\neg c$ is added to the formula, and unit-propagation infers the negation of the 1-UIP literal.

Hybrid CP-SAT solvers work on the same principle, with two key differences. Firstly, there is a mapping between Boolean literals and restriction events on the domains of numeric (often integer) variables. For instance, a literal $a_{i,v}$ may stand for the assignment event $x_i=v$ and $\neg a_{i,v}$ to the removal event $x_i\ne v$. Secondly, arbitrary constraint propagation algorithms can be used as well as clauses to infer new true literals. In order to use conflict analysis as described above, general constraints must be able to produce explanation clauses. Given a literal $l$ inferred by some constraint propagation algorithm in a search state defined by the set of true literals $ℱ$, an explanation clause is a clause $c$ entailed by the model and such that unit-propagation on $ℱ\wedge c$ produces the true literal $l$. The name Lazy Clause Generation comes from the fact that explanation clauses are generated during search rather than proactively as an encoding. However, this should not be confused with another type of laziness: explanation clauses can be generated during constraint propagation, or in a true “lazy” way, only when we want to replace a literal in the conflict set with its reason. In Tempo the two options are used, depending on the constraint.

Satisfiability Modulo Theories (SMT) solvers decide the satisfiability of formula of the form $\exists 𝒳.\phi$ with $\phi$ a propositional logic formula whose atoms have a semantic in an underlying theory. Difference Logic is a fragment of linear arithmetics where atoms stand for binary difference constraints of the form $[[x-y\le k]]$ with $x,y\in 𝒳$ and $k$ a constant.

The duality between shortest path and systems of difference constraints is well know [4]. A conjunction of difference logic constraints $ℰ$ can be mapped to a temporal network, i.e., a directed graph $G_{ℰ}$ with one vertex per numeric variable, and a labeled edge $y\stackrel{𝑘}{\to }x$ for every difference constraint $[[x-y\le k]]\in ℰ$. The system $ℰ$ is satisfiable if and only if $G_{ℰ}$ does not contain any negative cycle, and the difference constraint $[[x-y\le k]]$ is entailed by $ℰ$ if and only if the length $d_{ℰ}(y,x)$ of the shortest path from $y$ to $x$ in $G_{ℰ}$ is less than or equal to $k$. For this reason, we shall refer to difference constraints as edge in this paper.

Given the set of edges $𝒜$ that appear in a formula, and given a subset $ℰ\subseteq 𝒜$ of true edges (edge literals assigned to “true”), a difference logic reasoner is expected to decide if $ℰ$ is consistent. If so, it should produce the set ${ℰ}^{\prime }\subseteq (𝒜\setminus ℰ)$ of edges entailed by $ℰ$, along with their explanations. If not, it should produce an explanation for the inconsistency. It is possible to compute all the entailed edges in polynomial time, by computing all-pair shortest paths in the graph $G_{ℰ}$ with e.g., the Floyd-Warshall algorithm. State-of-the-art implementations do not compute the full transitive closure. Instead, when a new true edge is added to the system, only the edges that appear in the formula and have become entailed by the system are computed. This computation can be done incrementally, by maintaining a potential function and using Dijkstra’s algorithm, after relabeling the edges in the same way as in Johnson’s algorithm [13, 16].

The problem of scheduling tasks under resource constraints has been an extremely successful domain for constraint programming. We are given a set of tasks $ℐ$, where $i\in ℐ$ is defined by an interval of time of possibly variable length $p_i$; where $s_i$ denotes the start time of task $i$; and where $e_i$ is its end time. Tasks can be subject to precedence constraints, set between their start or end times. They can also be subject to resource constraints. In this paper we consider only disjunctive constraints, stating that two tasks using the same resource may not overlap. Difference logic captures well these problems since precedence constraints are edges and the NoOverlap constraint (also referred to as disjunctive or unary resource) is defined a 2-CNF whose atoms are edges:

Moreover, this formulation should make it clear that if all difference logic atoms are assigned a truth value, and if the resulting difference system is consistent, then the problem is satisfiable. Indeed, all constraints (precedences and resources) are defined exclusively using difference logic atoms. Therefore, if we maintain the consistency of the difference logic system, there is no need to branch on start times, end times or durations in the search tree. In this paper we only consider problems where the objective function to minimize is the maximum of all the end times (i.e., the makespan), although several other objectives are of interest.

There are two primitive types of variables in the solver: Boolean and numeric variables. The domain of a numeric variable is defined by its lower and upper bounds. Bound literals are constraints of the form $[[\pm x\le k]]$. We use signed variables so that bound literals are all in the canonical form of difference logic constraints ($[[x\ge k]]$ is written $[[-x\le -k]]$), and so that a smaller right-hand side always corresponds to a tighter literal. We say that $[[\pm x\le k]]$ is active if it was created (e.g. by constraint propagation) at a decision level lower than or equal to the current one in the same branch. In other words, a literal $[[\pm x\le k]]$ can be true without being active, if there is an active literal $[[\pm x\le k^{\prime }]]$ with . For every signed variable, the list of active literals maintained in decreasing order of their right-hand sides. For instance, if the lower bound of a numeric variable $x$ changes (to take the value $k$) because of constraint $c$, the literal $[[-x\le -k]]$ is inserted at the end of the list for $-x$ and its explanation is $c$. Some solvers [26, 17] support lazy bound literal generation. A possible implementation is essentially equivalent to adding new Boolean variables during search with a bound semantic attached to it. This means that the corresponding Boolean variable must live as long as a clause involves such a literal. More generally, adding such literals during search is easy, however, making sure that the number of literals does not grow too large is difficult. Therefore, in Tempo, much like in Aries, the literal $[[\pm x\le k]]$ is not linked to any Boolean variable. It is created when the domain of variable $x$ changes accordingly, and no longer exists when backtracking over that decision level in the search tree. However, this incurs a cost when accessing the informations attached to such a literal. For instance if one wants to access the explanation for $[[\pm x\le k]]$, one must search for the highest value of $k^{\prime }\le k$ such that the literal $[[\pm x\le k^{\prime }]]$ is currently active. Since $[[\pm x\le k^{\prime }]]$ entails $[[\pm x\le k]]$, its explanation is also valid³³3Note that $[[\pm x\le k]]$ cannot be in the explanation of $[[\pm x\le k^{\prime }]]$ because it would entail that a literal $[[\pm x\le k^{\prime \prime }]]$ with is active but that would contradict $k^{\prime }$ is the highest such value.. Similarly, if the literal $[[\pm x\le k]]$ is inferred e.g., by constraint propagation, unit-propagation algorithm would access the list of clauses that watch it in constant time. This is impossible if we do not allocate any memory for literals that are not active. Our implementation of the watched literals data structure is discussed in Section 4.3.

As in SAT Modulo Theories solvers, Boolean variables may be given a semantic in difference logic, i.e., each literal of a Boolean variable $a$ can be associated to an edge: $a⟹[[x-y\le k]]$. The negative literal $\neg a$ can stand for the negation of the edge (). However, we allow for the positive and negative literals of the same variable to be associated to any edges, or no edge at all. This is useful to represent a binary disjuncts with a single variable, e.g.:

The binary disjunct in Eq. 2, stating that tasks $i$ and $j$ do not overlap can be represented with a single variable $a_{i,j}$ with $a_{i,j}⟹[[e_i-s_j\le 0]]$ and $\neg a_{i,j}⟹[[e_j-s_i\le 0]]$. This is also useful for optional tasks, where we might want that a Boolean variable implies an edge, but its negation leaves the numeric variable free.

The difference logic system in implemented in Tempo uses a reversible directed graph $G_{ℰ}$. When the literal $[[x-y\le k]]$ is set to true, the edge is directly added to the difference logic system, modeled by the arc $y\stackrel{𝑘}{\to }x$ in $G_{ℰ}$. Our implementation differs from the method described by Cotton and Maler [13] in the following ways: Firstly, as explained by Feydy et al., in typical constraint problems, many more bounds literals are propagated than edge literals, and hence it is important to have a dedicated procedure for each type [16]. Moreover, since bounds literals are generated lazily, they do not necessarily appear in the formula prior to search. We use the common approach to have a distinguished vertex standing for the constant $0$ in the temporal network. This vertex is connected to every other numeric variable, however implicitly. That is, if $[[x\le k]]$ is the tightest true upper bound literal for variable $x$, then everything works as if the arc $0\stackrel{𝑘}{\to }x$ was in the graph, i.e., the difference constraint $[[x-0\le k]]$, and similarly, $[[-x\le -k]]$ indicates the arc $x\stackrel{-k}{\to }0$. Those arcs are not actually added to avoid having several arcs between the same vertices. Therefore, given the set of edges $𝒜$ that appear in the constraint program and a subset $ℰ\subseteq 𝒜$ of true edges, for each new edge $[[x-y\le k]]$, the reasoner achieves three tasks: decide consistency; compute the set $ℬ$ of bounds literals entailed by $ℰ\cup \{[[x-y\le k]]\}$; and compute a set ${ℰ}^{\prime }\subseteq (𝒜\setminus (ℰ\cup \{[[x-y\le k]]\}))$ of entailed (non-bound) edges.

As in [16], given a new arc $y\stackrel{𝑘}{\to }x$, the first two tasks are done via two calls to a shortest path algorithm. Let $d(0,x)$ be the length of the shortest path from the origin ($0$) to $x$, and $d(x,0)$ be the length of the shortest path to the origin from $x$ in $G_{ℰ}$. The bound literals $[[-x\le -d(x,0)]]$ and $[[x\le d(0,x)]]$ are entailed by $ℰ$. In other words, all the upper (resp. lower) bound updates can be done by computing all the shortest paths from (resp. to) $0$ in $G_{ℰ}$. Since a shortest path can have changed only if it goes through the arc $y\stackrel{𝑘}{\to }x$ this can be done by one call from $x$ and another from $y$ in the converse graph. Notice that the shortest path algorithm can be stopped early when reaching a vertex whose shortest path from (resp. to) $0$ has not changed. Our approach has a worse time complexity than those described in [13, 16] because we use a version of Dijkstra with a simple FIFO queue but where the same vertex can enter the queue more than once. The worst-case time complexity of this algorithm is the same as Bellman-Ford. However, as opposed to Dijkstra’s algorithm, it can work directly on graphs with negative arcs and is efficient in practice when the new edge does not entail many bound updates. If the shortest path from the origin to $x$ is updated to a strictly lower value (say $k$) and $y$ is its predecessor on the path, via the arc $y\stackrel{k^{\prime }}{\to }x$, then the literal $[[x\le k]]$ is inferred, and its explanation is:

Moreover, there is a negative cycle if and only if the shortest path from $0$ to $y$ is updated in the first call, and the explanation is the set of edges in the negative cycle.

Finally, the main difference with respect to [13, 16] concerns the third task: we do not infer all the edges entailed by the current set of true edges. Indeed this requires to either store all the shortest paths and hence quadratic space, or to run the shortest paths algorithms as explained above, but without the early stop condition. Even though the worst-case time complexity is the same, it makes a significant difference on dense precedence networks. In our experiments this turned out to be too costly, and instead we compute only a subset of entailed edges. The rule to infer that the edge $[[x-y\le k]]$ is false corresponds to the standard propagation rule for binary disjunctions in existing scheduling models. Within the difference logic system implemented in Tempo, the rule is as follows:

Indeed the following difference logic sentence is unsatisfiable

since it can be reduced to .

For every edge $[[x-y\le k]]$ in the difference logic system, there is a propagator that watches the lower bound literals of the numeric variable $x$ and the upper bound literals of the $y$, and triggers exactly as shown in Eq. 4 to produce the literal . The explanation can be:

We use a slightly improved explanation. Assume that the most recent bound literal is $[[0-x\le d(x,0)]]$. Then the explanation for $\neg l\iff \neg [[x-y\le k]]$ is:

Since we only need and this explanation is therefore more general.

Since bound literals are generated lazily, we cannot have constant-time access to all data structures storing information on literals. Bound literals are simply stored in order, with one list for upper bounds and another list for lower bounds. Therefore, the current lower and upper bound of a given numeric variable can be accessed in constant time. However, accessing the explanation for a given literal $[[x\le k]]$ requires to traverse the list of upper bounds literals for the variable $x$. This could be done by binary search, however, since conflict analysis usually does not explore literals beyond the current decision level, we chose to use a linear search starting from the most recent bound instead. Since conflict analysis is not as time consuming as constraint propagation, this is not a very important issue.

On the other hand, unit-propagation represents a significant proportion of the total runtime, and the watched-literal data-structure [35] must be adapted. In the standard method, we have a list of watcher clauses for every literal, containing every clause that watches it (every clause watches two of its literals). We use the standard implementation when the watched literal is Boolean. Instead, for bound literals, we have an array indexed by signed numeric variables, i.e., ${𝒲}_x$ is the watch-list for the upper bound of $x$ and ${𝒲}_{-x}$ is the watch-list for its lower bound (see example in Figure 1). This array maps each signed variable to a list ${𝒲}_{\pm x}$ containing pairs $(k,W_{[[\pm x\le k]]})$ where $k$ is a numeric value and $W_{[[\pm x\le k]]}$ is the list of clauses currently watching the literal $[[\pm x\le k]]$. Those pairs are ordered by increasing value of $k$. When a literal $[[x\le k^{\prime }]]$ (resp. $[[-x\le -k^{\prime }]]$) becomes true, we scan the list ${𝒲}_{-x}$ (resp. ${𝒲}_x$). When encountering a pair $(k,W_{[[\pm x\le k]]})$ with $k+k^{\prime }\ge 0$ we know that the clauses in $W_{[[\pm x\le k]]}$ and in all the list after $W_{[[\pm x\le k]]}$ do not need to be unit propagated since they watch a literal weaker than $[[\pm x\le k^{\prime }]]$, and hence no more propagation can occur.

However, the list ${𝒲}_{\pm x}$ must be maintained sorted. Therefore, the additional cost of this data structure comes when moving a clause from a watch list to another watch list. That is, suppose that the literal $[[\pm x\le k]]$ watched by clause $c$ is falsified. If the clause $c$ contains an unwatched, unassigned literal (say $[[y\le k^{\prime }]]$) then $c$ must be removed from $W_{[[\pm x\le k]]}$, which can be done in constant time, and added to the list $W_{[[y\le k^{\prime }]]}$. This can also be done in constant time, however, finding the list $W_{[[y\le k^{\prime }]]}$ within ${𝒲}_y$ takes a time linear in the size of ${𝒲}_y$. In other words, the insertion cost will increase linearly with the number of different bound literals currently watched for the same numeric variable.

We do not use the strongest possible consistency in the difference logic reasoner since computing the full transitive closure can be very costly. However, within the scope of a NoOverlap constraint on $ℐ$, we can compute the transitive closure on the $|ℐ|(|ℐ|-1)/2$ edge variables. The transitivity propagation rule is straightforward, and self-explained:

We use a reversible graph data structure for efficient access to the list of current successors and predecessors of a task. When an edge $[[e_i-s_j\le 0]]$ becomes true we add the edge $[[e_i-s_k\le 0]]$ for each successor $k$ of $j$, and $[[e_k-s_j\le 0]]$ for each predecessor $k$ of $i$.

The graph of precedences between tasks sharing the same resource can be leveraged to infer further propagation. This has been described in the more general context of cumulative resources [27], however, we focus here on the simple case of a disjunctive resources and use an algorithm described in Vilím’s Ph.D. thesis [52]. Suppose that we have a task $j$ and a set of tasks $\mathrm{\Omega }$ all requiring the same resource, and such that for each $i\in \mathrm{\Omega }$, $[[e_j-s_i\le 0]]$ is true. Then, although neither the precedences nor the NoOverlap relation can conclude, the tasks in $\mathrm{\Omega }$ cannot overlap because of the disjunctive resource, and hence we have:

There is as many non-dominated sets $\mathrm{\Omega }$ to consider than successors of $j$. Indeed, for any $\mathrm{\Omega }$ let $i\in \mathrm{\Omega }$ be the task with highest $lc{t}_i$. The set ${\mathrm{\Omega }}^{\prime }$ containing every successor of $j$ whose latest completion time is lower than or equal than $lc{t}_i$ is such that $p_{\mathrm{\Omega }}^{}{}_{}{}^{\prime }\ge p_{\mathrm{\Omega }}$ and $lc{t}_{{\mathrm{\Omega }}^{\prime }}=lc{t}_{\mathrm{\Omega }}$.

Alg. 1 is not identical, but essentially equivalent to Vilím’s. It first sorts the tasks by increasing latest completion time. Now, consider a literal created for task $j$ at Line 1. Task $i$ is a successor of $j$ and each successor whose latest completion time is less than $lc{t}_i$ has been explored earlier (because of the ordering). Therefore, $\mathrm{\Delta }[j]$ contains the sum of their durations. Alg. 1 runs in time linear in the number of true edges. It is sound because it applies the rule in Eq. 17, which is sound, and it is complete because we established that it goes through all the potentially non-dominated application of the rule.

We ran every method on every instance with 10 distinct random seeds. Every run was stopped after 30 minutes of user time. We then grouped the instances into two categories “Easy” and “Hard”, where the former corresponds to instances solved to optimality by all five solvers in every run, and the latter contains all the remaining instances.

The second part of Table 3 gives the result on an ablation study on some aspects of Tempo:

• $\mathrm{■}$

  Tempo${\setminus }_{\text{prec}}$ stands for Tempo without the precedence reasoning described in Section 6.

• $\mathrm{■}$

  Tempo${\setminus }_{\text{edge-finding}}$ stands for Tempo without the Edge-Finding rule described in Section 5.

• $\mathrm{■}$

  Tempo${\setminus }_{\text{weakening}}$ stands for Tempo without the numeric literal weakening rule described in Section 7, but with standard clause minimization instead.

The first observation is that the transitivity and temporal graph reasoning does not pay off. It helps on open-shop and with respect to the best objective on job-shop, but actually degrades the performances on job-shop with time lags and decreases the number of optimality proofs on job-shop. The Edge-Finding rule, however, is clearly useful on job-shop and open-shop, although it also degrades the performance on job-shop with time lags. The bound literal weakening rule has a small but consistently positive impact throughout, however.

Those results are consistent with the comparison between Tempo and Aries: resource constraint propagation has a significant positive impact on standard job-shop, but a negative impact on job-shop with time lags. We believe that in the latter, the temporal graph part is more important and comparatively less propagation comes from resource constraints. This is supported by the results on individual data sets shown in Table 1: Aries is better on la_0, la_0,5 and la_1 where the lags constraints are the strongest, while Tempo is better on la_3 and la_10 which are much closer to standard job-shop.