constraint forall (i, j in V where i < j) (
if exists(res in R)(r[i, res] + r[j, res] > rcap[res]) then
% Activity i must be run before or after j let {var bool: b} in (
(b -> S[i] + p[i] <= S[j])
/\ (not(b) -> S[j] + p[j] <= S[i])
)
else true endif
);
The detection which activity runs before the other can be further improved by considering the domains of the start times, and the minimal distances in the activity-onnode-network (see e.g. Dorndorf et al. [11]).

## 4. The Branch-And-Bound Algorithm

Our branch-and-bound algorithms are based on deterministic and conflict- driven branching strategies. We use them solely or in combination as a hybrid where at first the deterministic and then the conflict-driven branching is chosen (cf. Schutt et al. [26]). After each branch all constraints are propagated until a fixpoint is reached or the inconsistency for the partial schedule or the instance is proven. In the first case a new node is explored and in the second case an unexplored branch is chosen if one exists or backtracking is performed.

## 4.1. Deterministic Branching

The deterministic branching strategy selects an unfixed start time variable Si with the smallest possible start time minD Si. If there is a tie between several variables then the variable with the biggest size, i.e. maxD Si − minD Si, is chosen. If there is still a tie then the variable with the lowest index i is selected. The binary branching is as follows:
left branch Si ≤ minD Si, and right branch Si > minD Si. We denote this branching strategy by Mslf.

This branching creates a time-oriented branch-and-bound algorithm similar to Dorndorf et al. [11], but it is simpler and does not involves any dominance rule. Hence, it is weaker than their algorithm.

## 4.2. Conflict-Driven Branching

The conflict-driven branching is a binary branching over literals in the SAT solver. In the left branch the literal is set to *true* and in the right branch to *false*. As described in Sec. 2.3.1 on page 9 the Boolean variables in the SAT solver represent values in the integer domain of a variable x (e.g. ¬Jx ≤ 3K (Jx ≤ 10K)) or a disjunction between activities. Hence, it creates a branch-and-bound algorithm that can be considered as a mixture of time oriented and conflict-set oriented.