negative-weight cycle then the Rcpsp/max instance is infeasible. Otherwise the shortest path from the source v0 to an activity i determines the earliest possible start time for i, i.e. −w(v0 → i) where w(.) is the length of the path and the shortest path from an activity i to the sink vn+1 the latest possible start time for i in any schedule, i.e. tmax + w(i → vn+1). The Bellman-Ford algorithm has a runtime complexity of O(*|V| × |E|*).

These earliest and latest start times can not only used for an initial smaller domain, but also to improve the objective constraints by replacing them with

% Objective constraints
constraint
$$\begin{array}{l}{{\mathrm{\Large~objective~constraints}}}\\ {{\mathrm{straint}}}\\ {{\mathrm{forall~(i~in~V)~(S[i]~+~tail[i]~<=~objective);}}}\end{array}$$
where tail[i] is the "negative" length −w(i → vn+1) of the shortest path from i to vn+1 in the digraph G. Preliminaries experiments confirmed that this modification gave major improvements for solving an instance and generating a first solution, especially on larger instances. Another advantage specific to LCG is that a smaller initial domain also reduces the size of the problem because less Boolean variables are necessary to represent the integer domain in the SAT solver.

## 3.2. Activities In Disjunction

Two activities i and j ∈ V are in *disjunction*, if they cannot be executed at the same time, i.e. their resource requirement for at least one resource k ∈ R is bigger than the available capacity: rik + rjk > Rk. Activities in disjunction can be exploited in order to reduce the search space.

The simplest way to model two activities i and j in disjunction is by two propositional constraints sharing the same Boolean variable Bij .

$$\begin{array}{c}{{B_{i j}\to S_{i}+p_{i}\leq S_{j}}}\\ {{\neg B_{i j}\to S_{j}+p_{j}\leq S_{i}}}\end{array}$$
$\forall i<j$ in disjunction (1) $\forall i<j$ in disjunction (2)
Bij → Si + pi ≤ Sj ∀*i < j* in disjunction (1)
¬Bij → Sj + pj ≤ Si ∀*i < j* in disjunction (2)
If Bij is *true* then i must end before j starts (denoted by i  j), and if Bij is *false* then j  i. The literals Bij and ¬Bij can be directly represented in the SAT solver, consequently Bij represents the relation (structure) between these activities. The propagator of such a propositional constraint can only infer new bounds on left hand side of the implication if the right hand side is false, and on the start times variables if the left hand side is true. For example, the right hand side in the second constraint is false if and only if maxD Si − minD Sj < pj . In this case the literal ¬Bij must be false and therefore i  j.

Adding these redundant constraints to the model allows the propagation solver to more quickly determine information about start time variables. The Zinc model of these constraints is
% Redundant non-overlapping (disjunctive) constraints