Compact MDDs for Pseudo-Boolean Constraints with At-Most-One Relations in Resource-Constrained Scheduling Problems

1 Introduction

Scheduling problems consist of finding execution times for each of the activities of a project while respecting some constraints. The most frequent involve precedence relations between activities and limitations over the use of shared resources with finite capacity. Usually, the goal is to find a schedule that minimizes the makespan, i.e., the total duration of the project. These problems are NP-hard. Among scheduling problems, the Resource-Constrained Project Scheduling Problem (RCPSP) is a well-studied one which comprises non-preemptive activities and renewable constraints. Many extensions of this problem have been proposed [Brucker et al., 1999]. One of the key points for solving these problems is how the resource constraints are handled.

In this work we use SAT Modulo Theories (SMT) encodings for scheduling problems: we use Integer Difference Logic (IDL) to enforce precedences, and SAT encodings of pseudo-Boolean (PB) constraints to control resources usage.

Interestingly, in some cases the variables of such PB constraints have at-most-one (AMO) relations enforced by other constraints of the global encoding. We show how to take advantage of this fact to simplify the encodings.

The main contribution of this paper is to provide a specific way to use Multi-Decision Diagrams (MDD) to represent PB constraints with AMO relations between their variables, which we call AMO-PB constraints. AMO-PBs represent partial functions which do not include in their domain some assignments which are assumed to be forbidden due to AMO relations. Having a partial domain allows us to build compact MDDs which are translated into small SAT encodings. We show that such encodings are very efficient compared to BDD-based SAT encodings of PB constraints. Our approach can be applied to any problem in which PBs and AMO constraints between their variables appear together, but in this work we focus on scheduling problems. The use of AMO-PBs turns out to be decisive in some problems, where we are able to outperform state-of-the-art exact solvers.

In the problems we consider, there occur several AMO relations that we can exploit to compact PB constraints into AMO-PBs. Interestingly, in the formulation of our problems sometimes we do not need to include any SAT encoding of the AMOs, since these are enforced implicitly. On the one hand, we consider the RCPSP, where AMO relations arise from precedences between activities. On the other hand, we consider two extensions of it: the MultiMode RCPSP (MRCPSP) [Brucker et al., 1999] where each activity can be executed in one of many modes, and the RCPSP with Time-Dependent Resource Capacities and Requests (RCPSP/t) [Hartmann, 2013]. The impact of taking into account AMOs is higher in these extensions, because the variables introduced to deal with modes or with resource requirement variations have additional AMO relations which make AMO-PB encodings much smaller than PB encodings. Our results show a reduction in the size of the encodings of one order of magnitude in terms of Boolean variables.

2 RelatedWork

Many exact approaches have been proposed to tackle the RCPSP and the MRCPSP, based on Integer Linear Programming (ILP) [Zhu et al., 2006; Kon´e et al., 2011], FailureDirected Search (FDS) [Vil´ım et al., 2015] or Lazy Clause Generation (LCG) [Schutt et al., 2013; Szeredi and Schutt,

2016]. SMT has also been shown to be a competitive approach to solve such scheduling problems [Ans´otegui et al., 2011; Bofill et al., 2016]. The latter demonstrated the good performance of PB constraints to encode resource constraints. In [Hartmann, 2015] it was introduced a genetic algorithm to solve the RCPSP/t, but to our knowledge no exact approach for this problem has been published.

Regarding the field of PB constraints, there have been many works on representing them as Binary Decision Diagrams (BDDs) and translating them to SAT encodings [E´en and Sorensson, 2006; Ab´ıo et al., 2012]. In [Ab´ıo et al., 2016] there were presented SAT encodings for the generalized case of MDDs. [Ab´ıo et al., 2015] presented an algorithm to construct MDDs from PB constraints with implication chains. There, it is shown how this approach can be used to capture AMO relations between variables, but unlike our approach, it requires some transformations of the original constraints which introduce many additional clauses and fresh variables.

In [Ab´ıo and Stuckey, 2014] it was provided an algorithm to construct MDDs representing Linear Integer (LI) constraints. MDDs were also used in [Cire and van Hoeve, 2012] in the field of scheduling to model the disjunctive global constraint.

3 MDDs for Pseudo-Boolean Constraints with AMO Relations

Before going into the definition of AMO-PBs, we will introduce the concepts of PB and BDD, and illustrate how BDDs can represent PBs.

Definition 3.1. A pseudo-Boolean (PB) constraint has the form:

where qi and K are integer constants, xi are 0/1 (true/false) variables, and # ∈ {<,≤,=,≥,>}. As usual in the literature and w.l.o.g. we will assume that # is ≤ [E´en and Sorensson, 2006].

Definition 3.2. A Binary Decision Diagram (BDD) is a rooted, directed, acyclic graph which represents a Boolean function. BDDs have two terminal nodes, namely F-terminal and T -terminal. Each non-terminal node has associated a Boolean variable (selector), and has two outgoing edges, representing the true and the false assignment of the selector. Every truth assignment of the variables follows a path from the root to the T -terminal if it satisfies the formula, or to the F-terminal otherwise.

A BDD is called ordered if different variables appear in the same order on all paths from the root. A BDD is said to be reduced if the following two rules have been applied until fix point:

• Merge any isomorphic subgraphs.
• Eliminate any node whose two children are isomorphic.

A Reduced Ordered Binary Decision Diagram (ROBDD) is canonical (unique) for a particular function and variable order.

(RO)BDDs can in particular represent PB constraints [E´en and Sorensson, 2006]. Figure 1a contains the ROBDD representation of the PB constraint C : 2x1+3x2+4x3+5x4 ≤ 7 with the variable order x1 ≺ x2 ≺ x3 ≺ x4. As seen in the picture, a BDD can be organized in different layers, and at each layer it is considered a different selector variable. For instance, in all the nodes of the second layer we choose whether to set x2 to true or to false.

In this work we deal with PB constraints whose variables satisfy AMO relations. For example, consider again the PB constraint C : 2x1 + 3x2 + 4x3 + 5x4 ≤ 7, and assume that AMO(x1, x2) and AMO(x3, x4) hold, i.e., these constraints are already enforced. A possible truth assignment of C would be x1 = true, x2 = true, but we know that such an assignment is already forbidden. Therefore, there is no need to handle this assignment in an encoding of the PB constraint. This motivates the definition of PB constraints with AMO relations as follows.

Definition 3.3. We refer to an integer linear expression q1 · x1 + · · · + qm · xm over 0/1 variables x1, . . . , xm, subject to the fact that at most one xi is true, as an AMO-product. We conveniently express AMO-products as QX, where Q = 〈q1, . . . , qm〉 and X = 〈x1, · · · , xm〉.

Definition 3.4. We refer to an expression of the formQ1X1+ · · · + QnXn ≤ K, where QiXi are AMO-products and K is an integer constant, as a PB constraint with AMO relations (AMO-PB).

Note that an AMO-PB can be seen as a partial function, whose value is undefined if the AMO relation does not hold for some Xi.

AMO-PBs generalize PBs, since the particular case in which each AMO-product contains only one variable is indeed a PB constraint. Now, still assuming that AMO(x1, x2) and AMO(x3, x4) hold, we can redefine C as an AMO-PB C ′ : 〈2, 3〉 · 〈x1, x2〉 + 〈4, 5〉 · 〈x3, x4〉 ≤ 7. This has to be read as: the sum of either 2x1 or 3x2 or non of them, plus 4x3 or 5x4 or none of them, is ≤ 7. Unlike C, C ′ is not defined for assignments such as x1 = true, x2 = true, i.e., the assignments that do not satisfy the AMO relation between the variables of some AMO-product do not belong to the domain of C ′ . The key point of our approach is constructing decision diagram representations of AMO-PBs which do not handle such assignments; this lets us obtain more compact structures than the classical BDD representations of PB constraints. Obviously, it has to be guaranteed that the AMO constraint of each AMO-product is satisfied but, interestingly, it may be the case that these constraints are implied by other constraints, as we will see in Section 4. Now we show how to represent an AMO-PB constraint with an MDD.

Definition 3.5. A Multi-Decision Diagram (MDD) is a generalization of a BDD. It is a rooted, directed, acyclic multigraph which has two terminal nodes, namely F-terminal and T -terminal. Each non-terminal node can have an arbitrary number of outgoing edges, each one corresponding to a different decision. The same notions of ordered and reduced can be applied to MDDs, thus having also ROMDDs.

In their classical definition, MDDs stand for Multi-valued Decision Diagrams and can be seen as a generalization of BDDs which have a multi-valued selector variable in each node instead of a Boolean variable [Srinivasan et al., 1990]. However, and especially in the context of SAT encodings of MDDs, a set of Boolean variables can be used as selectors, each variable representing a different decision.

In our setting, each non-terminal node has associated a list of Boolean selector variables 〈x1, . . . , xm〉, and has an outgoing edge for each variable. Moreover, there is an additional outgoing edge, which we denote as the else edge. Each one of the m+1 outgoing edges corresponds to a different decision, namely assigning to true exactly one of xi, 1 ≤ i ≤ m, or assigning all of them to false, hence choosing the else edge.

AMO-PBs can be represented with such MDDs, where each node handles an AMO-product, and all paths from the root to a terminal node choose (assign to true) at most one of the variables of each AMO-product. Every one of these truth assignments follows a path from the root to the T -terminal if it satisfies the AMO-PB, or to the F-terminal otherwise. Figure 1b contains the ROMDD representation of C ′ with the order 〈x1, x2〉 ≺ 〈x3, x4〉. Unlike BDDs for PB constraints, where each layer considers a single variable, each layer of an ROMDD considers the set of variables of a different AMOproduct. Note the significant size reduction with respect to the ROBDD representation of C in Figure 1a. In particular, we have now just 2 non-terminal nodes instead of the 6 we had originally, and the depth is reduced from 5 to 3.

3.1 The Particular Case of Exactly-One

The particular case where the variables of an AMO-product satisfy an exactly-one (EO) constraint is already supported by AMO-PBs. However, in this case we can further simplify the AMO-product as follows. Consider an AMO-PB Q1X1 + · · · + QnXn ≤ K. Let Xi = 〈x1, . . . , xm〉 such that an EO relation holds on its variables, and Qi = 〈q1, . . . , qm〉. We can simplifyXi intoX′ i = 〈x1, . . . , xj-1, xj+1, . . . , xm〉 andQi intoQ′i = 〈q1-qj, . . . , qj-1-qj, qj+1-qj, . . . , qmqj 〉, for some j, and replace the original AMO-PB by Q1X1+ · · ·+Q′iX′ i +· · ·+QnXn ≤ K-qj . Moreover, by choosing a qj which appears more than once, more than one variable can be removed from the AMO-product.

Example 3.1. Let C : 〈2, 2, 3, 4〉 · 〈x1, x2, x3, x4〉 ≤ 3, and assume that EO(x1, x2, x3, x4) holds. By removing all xj with coefficient qj = 2 in the previously described way, we obtain C ′ : 〈1, 2〉 · 〈x3, x4〉 ≤ 1, and AMO(x3, x4) holds. Note that we can replace C by C ′ because the following holds:

3.2 MDDConstruction

In [Ab´ıo et al., 2012], it was presented an algorithm to construct a ROBDD representing a PB constraint with a given variable ordering, whose running time is polynomial w.r.t. the size of the resulting ROBDD. Now we present a generalization of this algorithm to construct a ROMDD representing an AMO-PB with a given order on the sets of variables of the AMO-products. We highlight the main aspects of this generalized algorithm, and refer the reader to [Ab´ıo et al., 2012] for further details.

Before describing the algorithm, we introduce the idea of interval for AMO-PB constraints.

Definition 3.6. Let C be of the formQ1X1+· · ·+QnXn ≤ K. The interval of C are all integers K′ such that Q1X1 + · · · + QnXn ≤ K′ , interpreted as a Boolean function, is equivalent to C. The set of valid K′ is always an interval that we denote as [β, γ].

For example, given the AMO-PB 〈1, 5, 4〉 · 〈x1, x2, x3〉 + 〈4〉 · 〈x4〉 ≤ 6, its interval is [5, 7], because its truth table is the same for K′ = 5, K′ = 6 and K′ = 7, and different for K′ = 4 and K′ = 8 (taking into account that this AMO-PB is undefined for some assignments). The ROMDD representation of an AMO-PB constraint is the same for all the values of its interval.

At layer i of the global ROMDD, each node is the root of the ROMDD representing the AMO-PB QiXi + · · · + QnXn ≤ K, for some different K at each node. The algorithm ensures that the ROMDD is reduced by maintaining a set Li of tuples ([β, γ],M) for each layer i of the global ROMDD, where [β, γ] is an interval and M its associated ROMDD. We denote L = (L1, . . . ,Ln+1) the list of all Li sets of a ROMDD. By means of this dynamic programming method, the ROMDD representation for a particular interval of an AMO-PB constraint is constructed only once, and reused as many times as needed.

The main procedure is described in Algorithm 1. It receives as input an AMO-PB C : Q1X1 + · · · + QnXn ≤ K, and the ordering used for the ROMDD is X1 ≺ · · · ≺ Xn. It starts by computing, for each layer of the final ROMDD, the interval of the T -terminal ROMDD and the interval of the F-terminal ROMDD. Then, it calls the recursive procedure MDDBuild (Algorithm 2). This inserts and searches ROMDDs in the lists Li while recursively constructing the global ROMDD. More precisely, each call creates (if it was not already constructed and stored in Li) the ROMDD for a given AMO-PB C : QiXi+· · ·+QnXn ≤ K and layer i. To construct this ROMDD, the child for each possible decision

Algorithm 1 Construction of ROMDD algorithm

Require: constraint C : Q1X1 + · · · +QnXn ≤ K Ensure: returnsMthe ROMDD of C for all i such that 1 ≤ i ≤ n + 1 do Li ← {((-∞,-1],F) , ([ ∑ j∈[i,n] max(Qj),∞), T )} end for L ← 〈L1, . . . , Ln+1〉 ([β, γ], M) ← MDDBuild(1, C, L) return M

is recursively constructed, taking into account that choosing xj contributes with qj to the left-hand-side sum of C, and that choosing else has a 0 contribution. If all the children are the same ROMDD, i.e., all the outgoing edges point to the same ROMDD, no new node is created but this unique child is already the representation of C. Otherwise, the root node for the ROMDD representing C is created, and its children are properly linked. Finally, the obtained ROMDD and its corresponding interval are inserted in Li.

Algorithm 2 uses the following functions:

search(K,Li): If there is a tuple (I,M) in Li, such that K ∈ I, it is returned. Otherwise, an empty interval is returned in the first component of the tuple.

insert((I,M),Li): Inserts (I,M) into the set Li.

indexOfMax(Qi): Returns the position of the maximum coefficient in list Qi.

mdd(〈x1, . . . , xm〉, 〈M1, . . . ,Mm〉,Melse): Constructs an MDD with a new node as root, Mj as child for selector variable xj, andMelse as the else child.

3.3 SAT Encodings of MDDs for AMO-PBs

The SAT encoding for MDDs that we use was firstly introduced in [Ab´ıo et al., 2012] for BDDs representing monotonic PB constraints. This encoding is generalized arcconsistent. A generalized version for MDDs can be found in [Ab´ıo et al., 2016]. Many other encodings were presented in the latter, not restricted to monotonic functions, but we have observed that in the resource constraints considered in this paper they generate larger encodings both in number of variables and clauses, and have a worse runtime performance.

In the AMO-PBs that we use in Section 4, all the coefficients are positive, and therefore we adapt the encoding for monotonic MDDs of [Ab´ıo et al., 2016] to take into account the else case. We add a fresh auxiliary Boolean variable v for each node of the MDD. Each non-terminal node of the MDD has as selector variables 〈x1, . . . , xm〉, and v as auxiliary variable. Each selector xi of a node has associated an outgoing edge to a child node with auxiliary variable vi. We assert the following clauses for each non-terminal node:

Moreover, we assert the clauses {vr}, {vT } and {¬vF}, where vr, vT , vF, are the auxiliary variables of the root, the

Algorithm 2 Procedure MDDBuild

Require: integer i ∈ {1, . . . , n+1}, constraint C : QiXi + · · · + QnXn ≤ K and list L Ensure: returns [β, γ] interval of C,Mits ROMDD ([β, γ], M) ← search(K, Li) if [β, γ] ̸= ∅ then return ([β, γ],M) else 〈x1, . . . , xm〉 ← Xi 〈q1, . . . , qm〉 ← Qi α ← indexOfMax(Qi) for all j such that 1 ≤ j ≤ m do C ′ ← Qi+1Xi+1 + · · · + QnXn ≤ K - qj ([βj , γj ], Mj ) ← MDDBuild(i + 1, C ′ , L) end for C ′ ← Qi+1Xi+1 + · · · + QnXn ≤ K ([βelse, γelse], Melse) ← MDDBuild(i + 1, C ′ , L) if [βα, γα] = [βelse, γelse] then M ← Mα [β, γ] ← [βα + qα, γα] elseM← mdd(〈x1, . . . , xm〉, 〈M1, . . . ,Mm〉,Melse) [β, γ] ← [βelse, γelse] ∩ ⋂ j∈[1,m][βj + qj , γj + qj ] end if insert(([β, γ], M), Li) return ([β, γ],M) end if

T -terminal and the F-terminal nodes respectively. Note that a node can have more than one selector pointing to the same child, and if it happens with the else child, there is no need to add the clauses corresponding to selector variables pointing to the else child. We remark that this encoding does not enforce AMO constraints on the variables of the AMO-products, but we have constructed the AMO-PBs assuming that such constraints hold. For the soundness of the whole encoding of a problem, these constraints must be already enforced either implicitly, as shown in Section 4, or explicitly.

4 Application to Scheduling Problems

The Resource-Constrained Project Scheduling Problem (RCPSP) consists of finding a start time for each activity (a schedule) in a project while respecting precedence and resource usage constraints. The schedule must minimize the total duration of the project (makespan). It is defined by a tuple (V, p, E, R, B, b) where:

• V = {A0,A1, . . . ,An,An+1} is a set of activities. Activities A0 and An+1 are dummy activities representing, by convention, the start and the end of the schedule, respectively. They don't consume resources and have duration 0.
• p is a vector of naturals, where pi is the duration of Ai.
• E is a set of pairs of activities representing precedence relations. Concretely, (Ai,Aj) ∈ E iff the execution of activity Ai must precede that of activity Aj, i.e., activity Aj must start after activity Ai has finished. We

assume that we are given a precedence activity-on-node graph G(V,E) that contains no cycles, since otherwise the precedence relation is inconsistent.

• R = {R1, . . . , Rv} is a set of renewable resources.
• B ∈ Nv is a vector of naturals, where Bk is the available amount of each resource Rk.
• b is a matrix of naturals corresponding to the resource demands of activities, and bi,k represents the amount of resource Rk that activity Ai is using per time step during its execution.

A schedule is a vector of naturals S = (S0, S1, . . . , Sn, Sn+1) where Si denotes the start time of activity Ai.

It is common in the literature to compute the transitive closure E∗ of E, which contains a pair of activities (Ai,Aj) iff there is a path from Ai to Aj in the precedence graph. We will denote G∗ = (A, E∗ ) as the extended precedence graph.

In ([Bofill et al., 2016]) it is proposed an SMT encoding for the MRCPSP which models the precedences as IDL expressions, and enforces the resource constraints with BDD encodings of PB constraints. The overall idea of the encoding is to capture, for each activity Ai ∈ V , and for each discrete time instant t ∈ TW(Ai), whether Ai is running at time t. Here TW(Ai) is the range of time instants in which Ai can be running according to some preprocessed information [Artigues et al., 2007]. In the current work we use the precedence graph to infer earliest start times and latest close times. Then, the encoding enforces the resource constraints at all time instants t ∈ [0,H], where H is a large enough time horizon to ensure the feasibility of the project. The following equations are a subset of this encoding properly adapted for the case of RCPSP. We do not reproduce the whole encoding, but the principal equations involved in the contributions of this paper.

Si are integer variables denoting the start time of activity Ai, and xi,t are Boolean variables which are true iff Ai is running at time t. Constraints (1) enforce the precedence relations, Constraints (2) define xi,t, and PB Constraints (3) ensure that the capacity of Rk is not surpassed at time t.

4.1 Implicit AMO fromPrecedences

A precedence (Ai,Aj) ∈ E introduces an incompatibility between these two activities, i.e., they can never be running at the same time. It is also the case for any pair of activities connected by a path in the precedence graph. For this reason, for a given time instant t there is a mutual exclusion between any pair of variables (xi,t, xj,t) such that (Ai,Aj) ∈ E∗ . This means that all the variables xi,t of activities in a path are pairwise mutually exclusive, or in other words, they satisfy the AMO relation. Note that there are no clauses explicitly enforcing the AMO over variables xi,t in a path, but it is guaranteed by Equations (1) and (2).

What we will do is to compute a path cover P = 〈P1, ..., Pl〉 in G∗ , i.e., Pi = 〈Ai1 , . . . ,Aik 〉 is a path in G∗ and every activity belongs to one and only one path.

For every path Pi ∈ P we will have an AMO-product in an AMO-PB constraint, and thus a layer in the resulting ROMDD. For this reason we are interested in finding a minimum path cover, which can be done in polynomial time in directed acyclic graphs [Fulkerson, 1956]. Note the importance of computing the minimum path cover in G∗ instead of G. Figure 2 depicts a precedence graph of a project with 7 activities. For the sake of simplicity, the picture does not contain all the additional extended precedences but only (A2,A5) ∈ E∗ . Thanks to this extended edge, we can find P = 〈〈A1, A3, A4〉, 〈A0, A2, A5, A6〉〉 which only has 2 paths. Otherwise, using the non-extended precedence graph a minimum path cover would contain 3 paths.

4.2 AMO-PB for Resource Constraints

Now we show how to use minimum path covers on G∗ to reformulate the resource constraints (3) as AMO-PB constraints. For some time instant t:

1. Compute G∗ (t) the subgraph from G∗ that contains all the nodes of the activities Ai such that t ∈ TW(Ai), i.e., G∗ (t) = (V (t),E∗ (t)), where V (t) = {Ai |Ai ∈ V, t ∈ TW(Ai)}, and E∗ (t) = {(Ai,Aj) | (Ai,Aj) ∈ E∗ , Ai ∈ V (t), Aj ∈ V (t)}.
2. Compute a minimum path cover P(t) = 〈P1, ..., Pl〉 of G∗ (t).
3. Formulate theAMO-PBconstraint by defining anAMOproduct for each Pi ∈ P(t)

The first two steps remain the same for many generalizations of the RCPSP, and in particular for the ones considered in this paper. The implementation of the third step for each particular problem is described below.

RCPSP

We substitute PB constraints (3) for the following AMO-PB constraints:

Where Q(Pi, k) is the list of coefficients:

And X(Pi, k, t) is the list of Boolean variables:

Note the AMO constraint among the variables of the AMOproducts is implicitly enforced by the precedences in the paths. This also happens in MRCPSP and RCPSP/t.

MRCPSP

The Multi-Mode Resource-Constrained Project Scheduling Problem (MRCPSP) introduces different execution modes for the activities. The durations and the demands of the activities depend on their execution mode. In addition to the start times, solutions have also to assign a single execution mode to each activity.

We denote the number of possible execution modes of Ai as Mi. For an activity Ai, running in mode o ∈ [1,Mi], its demand over resource Rk is bi,k,o, and its duration is pi,o. As done in [Bofill et al., 2016], we add the Boolean variables mi,o which are true iff Ai runs in mode o. It has to be ensured that each activity runs in exactly one mode. We encode this constraint (5) with the classical quadratic encoding. The dependence of the durations and the demands on the execution modes slightly modifies the precedence constraints (6), and requires the substitution xi,t for xi,t,o (7), now meaning that Ai is running at time t in execution mode o:

We update Constraints (4) by redefining Q and X:

Moreover, in this problem there can be non-renewable resources, whose demanded capacity is not recovered after the demanding activity ends its execution. Letting {Rv+1, . . . , Rw} be the non-renewable resources, the AMOPB constraint which guarantees that their capacity is not exceeded is the following:

Having:

Since variables mi,o maintain an EO relation for a fixed Ai (5), we apply the reduction explained in Section 3.1 to Constraints (8). In order to preserve the monotonicity required in the SAT encoding that we use for the MDDs, we take the minimum qj in each AMO-product. Thanks to this, we can remove at least one variable from each AMO-product. This turns out to be very significant in the benchmark instances considered in Section 5, which contain activities with 3 execution modes, and hence the number of variables in AMO-PB constraints is reduced at least to 2/3.

Note that the AMO constraint among the variables of AMO-products is preserved both in renewable and nonrenewable resource constraints. This follows from Constraints (5) and (7).

An interesting property of using AMO-PBs in MRCPSP is that the inclusion of multiple execution modes for the activities in the resource constraints do not yield an increase of the depth of the MDDs with respect to the single-mode case, because all the variables of possible modes of a particular activity are included in a same AMO-product (and hence handled in the same MDD layer). The BDD representation of resource PB constraints in [Bofill et al., 2016] multiplies the depth of the BDDs by the number of modes of the activities.

RCPSP/t

In this generalization of the RCPSP, the resources' capacities can be different at each time instant, and the requirements of an activity can be different at each time instant of its execution. Now we denote the capacity of resource Rk at time t as Bk,t, and the demand of activity Ai at its e-th execution time instant as bi,k,e. In order to encode this problem, we redefine variables xi,t to have a different meaning than in RCPSP. Now xi,t is true iff activity Ai starts at time t:

Where TW ′ (Ai) is the range of time instants at which Ai can start. Note that TW ′ (Ai) ⊆ TW(Ai). Now we can redefine the resource constraints (4) as:

Having:

The main idea of Constraints (10) is that an activity can only be running at time t because it has started at some time t - e for e ∈ [0, pj). Note that the AMO relation among all the variables xi,t of a given Ai is guaranteed by the domain of Si and Constraints (9), i.e., an activity has only one start time.

5 Experiments

We have run our experiments on a 8GB Intel R© Xeon R© E31220v2 machine at 3.10 GHz. In all experiments we use Yices 2.4.2 [Dutertre and de Moura, 2006] as the core SMT solver. We have also implemented the optimization procedure described in [Bofill et al., 2016]. We have tested our proposal on benchmark datasets of different hardness available in PSPLib [Kolisch and Sprecher, 1997] and MMLIB [Van Peteghem and Vanhoucke, 2014]. 1

First of all we compare the time performance of our system (APB in short) with the best known exact methods for these problems. Namely, for RCPSP and MRCPSP we consider Failure-Directed Search (FDS) [Vil´ım et al., 2015], Lazy Clause Generation (LCG) [Schutt et al., 2013; Szeredi and Schutt, 2016], and SMT with PB constraints (PB) [Bofill et al., 2016]. We have been able to run all the solvers in the described environment except LCG for the RCPSP, for which we have considered results from [Schutt et al., 2013]. To the best of our knowledge there is no exact approach to tackle RCPSP/t. In order to evaluate the impact of using AMO-PB constraints we have also codified this problem by transforming AMO-PBs into PBs in the obvious way (i.e., splitting all AMO-products into single variable products). These results are given in Table 1.

In the MRCPSP, APB is able to solve to optimality within the timeout many more instances than the other approaches, especially for MMLIB50 (M50 in the table), which is the hardest set of instances. Both in MRCPSP and RCPSP/t there is a significant speedup using AMO-PB constraints w.r.t. using PB constraints. One possible cause for this can be found in Table 2. It contains, for PB and APB, the average size of the encoding of a dataset in terms of number of Boolean variables and number of clauses. We consider the hardest set of each problem, i.e., MMLIB50 for MRCPSP and j120 for RCPSP/t. It can be seen that the reduction is an order of magnitude for the number of Boolean variables and halving for the number of clauses.

1 Our solvers and detailed results can be downloaded at http://imae.udg.edu/recerca/LAP

Regarding RCPSP, we have tested our system with sets j30, j60, j90 and j120 from PSPLib. We do not include detailed results for lack of space, but we have observed that APB average runtimes are very similar with the ones of FDS and LCG, and the number of unsolved instances is equal or smaller in all cases. Overall, we certify the optimality of 6 new instances and decrease the upper bound of 2 instances for the MMLIB50 dataset with respect to the best reported results until now [Bofill et al., 2016; Geiger, 2013]. Finally, as mentioned earlier, to our knowledge no previous results of exact methods have been published for the RCPSP/t datasets, but they have been tackled with heuristic methods in [Hartmann, 2013] and [Hartmann, 2015]. We have certified the optimality, or infeasibility for the time horizon specified, of 5090 instances, and improved the upper bound of 1763 instances with respect to the heuristic methods.

6 Conclusions

In this work we have shown that the codification into SAT of PB constraints which have AMO relations among their variables can be enhanced by using MDD representations. Although our technique can be used in any problem with such kind of constraints, we have shown that in the particular case of scheduling problems it performs very well. This suggests that the presented approach could be successfully used in other domains. In addition, we have presented SMT encodings for scheduling problems which have shown to provide very good performance, and that can be handled by any offthe-shelf SMT solver.

Acknowledgments

Work supported by grants TIN2015-66293-R (MINECO/FEDER, UE), MPCUdG2016/055 (UdG), and Ayudas para Contratos Predoctorales 2016 (grant number BES-2016076867, funded by MINECO and co-funded by FSE). We thank the authors of [Vil´ım et al., 2015; Szeredi and Schutt, 2016] for sharing with us the FDS and LCG solvers, and the author of [Hartmann, 2013; 2015] for sharing the heuristics results for the RCPSP/t. We are also grateful to Dr. Alan Frisch for his helpful comments.