activity j must start after the end of i, i.e. dij equals to the duration of i. In contrast to Rcpsp/max the decision variant of Rcpsp is polynomial solvable, but not its optimization variant which is NP-hard (Blazewicz et al. [7]). The reason for this is the absence of maximal time lags, i.e. here activity executions can always be delayed until to a point in time where enough resource units are available without breaking any precedence constraints. That is not possible for Rcpsp/max.

The best exact methods for Rcpsp to our knowledge are our own [26, 27] and Horbach [17]. Both use advanced SAT technology in order to take advantage of its nogood learning facilities. Our methods [26, 27] are a generic approach based on the Lazy Clause Generation (LCG) [24] using the G12 Constraint Programming Platform [32]. Lazy clause generation is a hybrid of a finite domain and a Boolean satisfiability solver.

Our approaches model the cumulative resource constraint either by decomposing into smaller primitive constraints, or by the creating a global cumulative propagator. The global propagation approach performs better as the size of the problem grows. In contrast to our methods Horbach's approach is a hand-tailored for Rcpsp, but similarly a hybrid with SAT solving. He uses a linear programming solver to determine activity schedules and hybridize with the SAT solver. Overall our global approach [27] is superior to Horbach's approach on Rcpsp.

In this paper we apply the same generic lazy clause generation approach to the more general problem of Rcpsp/max. Because the problems are more difficult than pure RCPSP we need to modify our approach in particular to prove feasibility/infeasibility We show that the approach to solving Rcpsp/max performs better than published methods so far, especially for improving a solution, once a solution is found, and proving optimality. We state the limitations of our current model and how to overcome them.

We compare out approach to the best known approaches to Rcpsp/max on several benchmark suites accessible via the PSPLib [1].

The paper is organized as follows. In Section 2 we give an introduction to lazy clause generation. In Section 3 we present our basic model for Rcpsp/max and discuss some improvements to it. In Section 4 we discuss the various branch-and-bound procedures that we use to search for optimal solutions. In Section 5 we compare our algorithm to the best approaches we are aware of on 3 challenging benchmark suites. Finally in Section 6 we conclude.

## 2. Preliminaries

In this section we explain lazy clause generation by first introducing finite domain propagation and DPLL based SAT solving, and then explaining the hybrid approach. We discuss how the hybrid explains conflicts and briefly discuss how a cumulative propagator is extended to explain its propagations.

## 2.1. Finite Domain Propagation

Finite domain propagation (see e.g. [25]) is a powerful approach to tackling combinatorial problems. A finite domain problem (C,D) consists of a set of constraints C over a set