Personnel Scheduling as Satisfiability Modulo Theories

1 Introduction

For companies and organizations in a broad range of business areas, it is necessary to provide availability 24 hours a day and 7 days a week. While some companies need their machines up and running all the time in order to fit the production demand, other organizations like hospitals or police stations need their staff to be working day and night to ensure proper health-care or the citizens' safety.

In this paper the particular problem of interest is Rotating Workforce Scheduling (RWS), which is a constraint satisfaction problem (CSP). This problem addresses designing a schedule where a certain number of shifts are assigned to work days over a specific planning period, typically one week. The work schedule is designed for each employee by considering the necessary temporal requirements and other constraints. Furthermore, in rotating workforce scheduling all employees work the same schedule in a rotating sequence starting at different offsets.

Over the years different approaches to this problem have been introduced in the literature. Early methods were based on exhaustive enumeration [Butler, 1978] and Integer Linear Programming [Laporte et al., 1980]. A network flow model was developed in [Balakrishnan and Wong, 1990] to solve the problem. In [Laporte, 1999] a relaxation of the constraints was proposed that allows the creation of efficient rotating schedules by hand. The use of an algebraic computational approach has been proposed in [Falc´on et al., 2016]. Heuristic techniques were successfully used to create rotating schedules in [Musliu, 2005; 2006]. Methods based on constraint programming techniques were applied in [Laporte and Pesant, 2004; Musliu et al., 2002; Triska and Musliu, 2011]. Although these exact approaches provide a solution for many instances, solving large problems is still a challenge for them. Therefore, it is intriguing to find other exact methods that may provide better results.

SMT-solving offers the expressive power of first-order theories combined with the good performance of state-of-the-art SAT-solvers. As a consequence, researchers have gained interest in using SMT for solving constraint satisfaction problems. In [Bofill et al., 2010] it is stated that SMT-Solvers are well suited for solving CSPs and a tool is presented for translating instances of the MiniZinc constraint modeling language into the SMT-LIB standard. SMT-solvers have been used to solve different constraint optimization problems [Ans´otegui et al., 2011], [Nieuwenhuis and Oliveras, 2006], [Ans´otegui et al., 2013]. In [Ans´otegui et al., 2013] a SMT based approach was presented for the Nurse Rosterin Problem (NRP), which is related to our problem. However, NRP differs from our problem as it does not take into consideration the cyclicity of the schedule.

In this paper we investigate how the RWS problem can be encoded in first-order formulas over certain background theories. By formulating the problem in the theory of quantifierfree linear integer arithmetic, many instances could be solved. However, this approach reached its limits when applied to problems with a large number of employees. To overcome this issue we developed a second new encoding using the theory of fixed-size bitvectors. By means of machine arithmetic we were able to achieve a very compact representation of the constraints and a reduced number of variables. We experimentally evaluated the two modeling approaches on benchmark instances from literature using various SMTsolvers. The proposed approach outperforms other existing exact approaches by solving more instances, which could not been solved yet by complete methods.

2 RotatingWorkforce Scheduling

Rotating Workforce Scheduling addresses the problem of shift assignment and day-off scheduling in the specific case of cyclic schedules. The formal definition of the problem and its instances is based on the definition from [Musliu et al., 2002]:

Instance:

• n: Number of employees.
• A: Set of m shifts (activities): a0, a1, ..., am-1, where a0 represents the special "day-off" shift.
• w: Length of the schedule. Typically the value of w is set to 7 (one week). The total length of a planning period is n × w for one employee, because of the cyclicity of the schedule.
• Cyclicity: The required schedule is considered to be cyclic, that is, each employee works the schedule for the complete planning period starting at a specific week. For example in the second week the first employee will take the schedule of the second employee, the second employee will take the schedule of the third employee, and so one the last employee will take the schedule of the first employee.
• R: Temporal requirements matrix, an (m-1)×w-matrix (because the day-off shift a0 is excluded) where each element ri,j of matrix R defines the required number of employees for the corresponding shift (i) on that day of the week (j).
• Prohibited shift sequences: Certain shift sequences must be prevented from being assigned to the employees.
• MINw and MAXw: Minimal and maximal possible length of work blocks. A work block consists of consecutive days on which an employee is working without having a day-off.
• Maximum and minimum length of periods of consecutive shifts: Vectors MAXSm, MINSm, where each element shows the maximum respectively minimum permitted length of periods of consecutive shifts.

Problem: Find a cyclic schedule (assignment of shifts to employees) that satisfies the requirement matrix, and all other constraints.

3 Modeling the RotatingWorkforce Scheduling problem

In this paper we propose two encodings that use functions and predicates from different background theories. The first formulation is based on linear integer arithmetic, whereas the second formulation expresses RWS with fixed-size bitvectors and bit-level operations.

3.1 Linear Integer Arithmetic

For the first modeling approach the theory of linear arithmetic over the integer numbers is used. The first step is to define a set of variables to represent the workforce schedule. Therefore, we define one variable for each day of the planning period, i.e. n ×w variables. Next, we have to specify the type of these variables. In order to simplify the constraint formulations we will use different integer numbers for the shifts, hence the type of our variables will be the Integers.

Let a schedule S be defined as a n×w matrix of variables, where n is the number of employees and w the number of work days.

Furthermore, we map every shift a0, a1, . . . , am-1 of A (see Section 2) to an integer number. Therefore, we define a function: f : A → N s.t. for all ai ∈ A \ {a0} : f(ai) = f (ai-1) ∗ n + 1 and f (a0) = 0 (explained below).

Every variable xi,j of schedule S is now assigned exactly one of our calculated integer values: ∀xi,j ∈ S : xi,j ∈ A′ and A′ = {f(ak) : ∀ak ∈ A (0 ≤ k ≤ m- 1)}

We will now focus on formulation of the constraints using linear integer arithmetic with equalities.

Temporal requirements The main reason why we use the function f to map every shift character ai to a natural number is that it allows us to specify the temporal requirement constraints by means of basic linear integer arithmetic. Thus, we can formally define the temporal requirements T(j) for a specific day j of the week as follows:

We can now formulate the temporal requirement constraints as an equation that always has to hold:

Since we defined the calculation f(ai) as the arithmetic operation f(ai-1)∗n+1, it is ensured that the required value for T(j) can only be obtained if the correct amount of staff is assigned to the corresponding shifts.

Shift Block Length To address the block length issue, we have to think of our schedule as a one dimensional sequence of work days instead of the matrix we defined before. This ensures that the last day of each week is adjacent to the first day of the next week. Additionally, we must not forget that in a cyclic schedule the last day of the last week is also adjacent to the first day of the first week. With that in mind we define the block length constraints by considering every variable to be the first in a new block. The neighbors of each of these possibly block-starting variables are then constrained: The block-starting variable itself has a certain shift value, then all following variables of the same block are restricted to the according shift value. For the following definitions we address every variable xi,j by its absolute position in the one dimensional representation of the schedule. Therefore, we omit the second index j as i will range from 1 to n × w.

Minimum Shift Block Length: For every xi, if xi = aj (where aj defines the shift to be constrained) and xi-1 ̸= aj, then xi+1 = aj ∧xi+2 = aj ∧ . . . ∧xi+min-1 = aj . We note that we have to avoid the cases when the subindex of x is out of bounds.

Maximum Shift Block Length: For every xi, if xi = aj ∧ xi-1 ̸= aj ∧xi+1 = aj ∧xi+2 = aj ∧ . . . ∧xi+max-1 = aj , then xi+max ̸= aj .

Note that the formulation of the shift block constraint must also be applied to the day-off shift a0 to restrict the minimum and maximum number of consecutive days off. We can describe the constraints for the work block length very similarly to those for the shift blocks. The only difference is that we do not care about the shifts the block consists of, unless they are assigned the special "day-off" shift a0. Due to this similarity and space limitation the formal definition for work block length is not given in this paper (this definition can be found in [Erkinger, 2013]).

Illegal Shift Sequences Safety concerns and legal reasons make it necessary to forbid certain shift sequences from being assigned to the employees. This means that if on a day xi an employee works in shift aj, the employee is not allowed to work in shift ak the day after. For every xi it has to hold that if xi = aj, then xi+1 ̸= ak (k ̸= j), iff aj → ak is forbidden. This assertion can be easily adapted to restrict illegal sequences of three shifts.

3.2 Bitvector Theory

The formulation of the problem in bitvector theory is more complex than the formulation using linear integer arithmetic. By definition a bitvector in the SMT context may be of arbitrary length. Therefore we propose using bitvectors that are the size of the complete schedule for the problem. Thereby each bit of a bitvector represents one day in the schedule. With that in mind, we use one bitvector per shift and one extra bitvector to represent the days-off. We will call the bitvector of a shift a shiftvector. A shift is assigned to a specific work day iff the according bit in the shiftvector is set to 1.

A schedule S is represented by m bitvectors shift0, shift1, ...shiftm-1, where shift0 represents the day-off shift. Each bitvector shifti (0 ≤ i ≤ m- 1) is of size n × w where n represents the number of employees and w the number of work days.

The subsequent sections discuss the constraints of rotating workforce scheduling using the bitvector encoding.

Shift Assignment The shift (including day-off) assignment constraint ensures that exactly one shift is assigned to each day of the schedule. This is accomplished in two steps: we have to make sure that there can be no more than one shift per day and employee and that there must be at least one shift assignment per day and employee.

For the first part of the constraint we use the bitwise AND operation. We have to apply this operation to every combination of two shiftvectors and assert that the result of the combination is a bitvector of the same length as the original vectors containing only zero-bits (0).

The example above shows a violation of this constraint because on two days both shift1 and shift2 have the according bits set to 1 meaning the employee would be assigned both shifts on these days.

To ensure correctness we also have to rule out that no shift is assigned to a specific day. Recall that this also includes the day-off shift (shift0). The second assertion addresses this issue by using the bitwise OR operation. If the result of the bitwise OR applied to all shiftvectors is equal to the bitvector containing only 1-bits, then at least one shift is assigned to each work day.

Temporal requirements Instead of only regarding the structure of our shiftvectors as having the length of the whole schedule (n × w), we have to think about the schedule as a multidimensional array, consisting of n arrays with size w in order to restrict the number of employees assigned to each shift on a specific day. Note that a shiftvector is read from right to left, meaning that the first week of the schedule starts with the least significant bit.

Because of the cyclicity of the schedule, every week also stands for the current shift schedule of one employee. Hence, every column of our multidimensional array represents the shift plan for all employees on that day of the week. In the formulated constraint the number of 1-bits in each column must be equal to the number of employees that should be assigned to the corresponding shift on that day. Therefore, we first have to create a temporary bitvector by extracting the correlating bits of the original shiftvector and concatenating them to a new bitvector that represents that day.

· · ·

The SMT-LIB input language provides an extract operation to select certain bits within a bitvector. These bits can be concatenated with the help of the concat operator.

In the next step we count all bits in the bitvector that are set to 1. To accomplish that, we calculate the Hamming Weight of our vector. In the following a short definition of the Hamming Weight is given:

"The Hamming distance d(u, v) between two words u and v, of the same length, is equal to the number of symbol places in which the words differ from one another. If u and v are of finite length n then their Hamming distance is finite since d(u, v) ≤ n."[Daintith et al., 2004]. Introduced by Richard Hamming in [Hamming, 1950], the Hamming distance is used in telecommunication for error detection and error correction. The Hamming Weight is simply defined as the Hamming distance of a word u and the zero-word. Hence, it represents the number of symbols which are different from the zero-symbol.

The original algorithm to calculate the Hamming Weight has a runtime that depends on the length of the input word, because it checks if every single symbol of the word differs from the zero-symbol. This approach is not ideal for our use, as it cannot be formulated in a declarative way and therefore is not suitable for us in the constraint formulation.

A better way to calculate the Hamming Weight is provided by the algorithm developed by Peter Wegner in 1960 [Wegner, 1960], which is based on the fact that if the bitwise AND operation is applied to a binary number N and N-1, then the resulting number has one 1-bit less than the original number N. In other words, the least significant 1-bit is eliminated.

input : A bitvector v output: The Hamming weight of bitvector v 1 while v ̸= 0 do 2 weight = weight + 1; 3 v = v & (v- 1); 4 end 5 return weight

Wegner's method offers the advantage that it can be formulated declaratively using recursion, because the number of iterations (recursive calls) is equal to the number of set bits in the input vector. Formally the number of selected bits n in a bitvector v can be calculated by the recursive application of v = v & (v - 1) until v = 0.

To use this method in our encoding we define a helper function (bitcount) that takes a bitvector v as input and returns the result of the operation v = v & (v - 1).

To make sure that a certain bitvector has exactly n bits that are set to 1, we define one assertion which guarantees that after n-1 applications of the bitcount function the bitvector is not equal to 0 and another assertion that ensures the vector is equal to 0 after n calls of the bitcount function. These assertions are defined for the previously created bitvectors of each work day.

MaximumShift Block Length Shift blocks are a sequence of 1-bits in a shiftvector. The length of this sequence needs to be constrained to prevent an employee from working an illegal number of consecutive work days of the same shift. To accomplish that, we need to count the consecutive 1-bits of a shiftvector.

We can find two consecutive bits in a bit vector v, by shifting the vector one bit to the right v >> 1 and combine it with the original vector using the AND operation v & (v >> 1). Then the bit vi is set to 1 iff vi+1 is set to 1 in the original vector. Hence, with every application of this operation the left most bit of a block is replaced by a 0.

To find n consecutive bits we can expand our equation to this generalized one:

(8)

Thus, we can use this kind of algorithm to restrict the maximum length (max) of a shift block, since the vector has to be equal to 0 after at most max iterations of v′ = v′ & (v >> i) with 1 ≤ i ≤ max, v being the original shiftvector and v′ being the resulting modified shiftvector v (see Example 8 for a maximum of 3).

Another problem we have yet to deal with is that of cyclicity. As we are designing a rotating schedule, the least and the most significant bit (lsb/msb) of each shiftvector are adjacent, which is important for the shift block constraints. To incorporate that, we simply concatenate every shiftvector with itself so that the lsb and the msb become adjacent in the middle of the new vector. Afterwards, we apply the consecutive bitcount method to this double-size bitvector.

Minimum Shift Block Length The next step is to ensure the minimum length of a shift block. This constraint is more difficult to formulate declaratively than the maximum shift block constraint. If we tried the same approach as for the maximum shift block length by applying the consecutive bitcount algorithm min times in order to assert that the vector equals to 0, this would clearly be wrong. As min only represents the minimum block length, longer sequences of consecutive bits are still allowed to exist. Hence, the resulting shiftvector not necessarily equals to 0.

The method we propose to ensure the minimum shift block length consists of three steps:

1. Delete illegal blocks: Apply min - 1 iterations of the consecutive bit count method to the shiftvector, where min is the minimum block length. After min - 1 applications at least one 1-bit of each legal block is still present, while all blocks of illegal size have been replaced by 0-bits.

1. Restore blocks: By iteratively shifting the vector from (1) to the left min - 1 times and applying the OR operation to the shifted vector and the one from the previous iteration, the length of all blocks is restored (except the already deleted illegal blocks).
2. Verify: In the last step we have to compare the bitvector from (2) with the original shiftvector. These two vectors are equal iff the original vector did not contain any illegal blocks in the first place, because otherwise they would have been deleted in step (1).

input : A bitvector v

input : The minimum block length min

output: A Boolean indicating that the min block length holds for v or not

1 v2 = v 2 for i = 1 to min-1 do 3 v2 = v2 & (v2 >> 1) 4 end 5 for i = 1 to min-1 do 6 v2 = v2 | (v2 << 1) 7 end 8 return v == v2

For better illustration of how the algorithm works, consider the following example. Take a shiftvector shift1 and check if the minimal block length min = 3 holds for all shift blocks of this vector.

We will start by applying the consecutive bitcount method min - 1 times:

(11)

The example above shows that with every iteration of the consecutive bitcount method, the left most bit of every 1block is replaced by a zero. Hence, after min - 1 = 2 iterations at least one set bit of each legal block has not been replaced, whereas the illegal blocks - blocks with a length less than min - have vanished completely.

As a next step we will restore the original shiftvector by shifting the vector back to the left min-1 times and applying the bitwise OR operation to every iteration (see 12). This will ensure that every 1-bit of a legal block that has been replaced by the consecutive bitcount method is being restored, while the blocks with illegal length are not.

The resulting vector is now compared to the original shift vector. The constraint is successfully fulfilled iff the two vectors are equal.

So far we have left out the fact that our algorithm does not consider the cyclicity of the schedule, meaning that the first and the last bit of a shiftvector are adjacent. To overcome this issue, we have to refine our algorithm in a way that incorporates rotating schedules. Suppose we have the following shift vector:

If we constrain the minimal block length to 3, the shiftvector will be legal, because we have two blocks of length 3, one being in the middle of the vector and one that consists of the first and the last two bits of the vector. Before we can make use of our algorithm, we therefore have to concatenate this split block, since otherwise the algorithm would falsely classify two blocks as illegal, one each at the beginning and the end of the vector. Thus, by moving the illegal block at the end in front of the most significant bit, we merge these blocks together and solve this issue.

We start out by creating a vector that only contains the last 1-block of the original shiftvector.

(15)

Example 15 shows how the vector can be modified, so that only the least significant 1-block is present. We could now concatenate this vector with the original shift vector in order to merge the split block. However, there is still a problem. Although we have concatenated the two vectors and thus considered the split block as a legal block, we still have two bits at the end of the vector, that form an illegal block. Therefore, before concatenating the two vectors, we apply the XOR operation to them and then concatenate the vector from 15 with the resulting vector of that operation.

The obtained vector represents the correct non-cyclic shiftvector. The minimum shift block length algorithm (Algorithm 2) applied to this vector will indicate whether the shiftvector contains only legal blocks or not.

Work Block Length: The work block constraints are very similar to the shift block constraints. The only difference is that a work block is a sequence of consecutive days where an employee has to work regardless of what shift he/she is assigned to.

We could get a vector encompassing all the work blocks by simply applying the bitwise OR on all shiftvectors, except the special "day-off" vector. Another way to obtain that vector is to negate the "day-off" vector, i.e. replace every 0 by 1 and every 1 by 0. The 1-bits in the resulting vector then represent all work-days, whereas the 0s stand for the days off. The easiest way to negate a bitvector is to use the NOT operation

.

We now use the same constraint formulations as for the shift block length on this new vector to restrict the length of consecutive work days.

Illegal shift constellations Certain shift constellations are considered illegal, because every employee needs a fixed amount of resting time between two workdays. Therefore, it is not allowed for example, to work the day-shift after working the night-shift.

These constellations can be forbidden with the help of bit rotation of a shiftvector. Considering the example above, to prevent the shift constellation Night →Day we have to rotate the shiftvector of the night shift N by 1 to the right. We can now AND this vector with the shiftvector of the day shift D and check if they have no bits in common that are set to 1. Subsequently, for any position i, Di ̸= Ni has to hold. Hence, the resulting bitvector must be 0.

The example also illustrates why it is important to use bit rotation instead of a logical shift right operation. If we had shifted the night shift vector to the right, we would have missed the fact that the least and most significant bit of each vector are adjacent.

The problem definition also allows illegal shift sequences of length 3 to be specified. The algorithm for detecting such illegal sequences is still very similar, except that we have to take three shiftvectors into consideration. A more detailed explanation can be found in [Erkinger, 2013].

4 Experimental Results

In this section we investigate the performance of our two modeling approaches on 20 benchmark instances described in [Musliu, 2005; 2006]. 1 The first three problems have been used in most rotating workforce scheduling papers given in the introduction and other 17 instances were derived from real life problems of different business areas. The collection contains small, middle-size and very large instances. The number of employees (or groups) for the largest instance is 163. As the number of shifts for this problem is 4 (including day-off), the search space for this problem is 4163∗7 .

1 http://www.dbai.tuwien.ac.at/staff/musliu/benchmarks/workforceScheduling.zip

We applied five state-of-the-art SMT-solvers (Z3 version 4.3.1 [de Moura and Bjørner, 2008], MathSAT5 version 5.2.5 (gmp 5.0.5, clang/LLVM 3.1, 64-bit) [Cimatti et al., 2013], CVC4 version 1.0 (compiled with GCC version 4.2.1) [Barrett et al., 2011], Yices version 2.1.0 [Dutertre and de Moura, 2006] and Boolector version 1.5.115 [Brummayer and Biere, 2009]). The solving process was performed on an Apple MacBook Pro with the following hardware details: 2.0 GHz quad-core Intel Core i7 (Sandy-Bridge) and 8 GB DDR3 RAM. The timeout for each solver and instance was set to 1000 seconds.

A comparison of the different solvers with respect to the number of found solutions for the the linear arithmetic (LIA) encoding shows that Z3 is able to solve the most benchmark instances (Z3 finds a solution for 15 instances). All five solvers achieve a higher solution rate with the bitvector approach than with the linear arithmetic method. MathSAT and Boolector were even able to solve 18 instances, which is three instances more than the best solver (Z3) of the LIA approach. A detailed evaluation including the exact runtimes can be found in [Erkinger, 2013].

Next, we compare the fastest performing SMT-solvers of each modeling approach to each other in order to evaluate whether one encoding is superior for solving the rotating workforce scheduling problem (Figure 1). The best performing solver of the linear arithmetic approach was Z3, whereas MathSAT provides the best results for the bitvector encoding. We can conclude from Figure 1 that the bitvector approach outperforms the linear arithmetic method on all instances and achieves significantly faster solving times. This seems to confirm the initial assumption that modeling the problem with bitvectors has a positive impact on the solvers' runtime.

5 Comparison to other Approaches

In order to evaluate whether the approach of solving the rotating workforce scheduling problem with SMT-solvers is competitive, we have to compare the results to other solving techniques from literature. First, we compare the results of MathSAT to two other approaches ([Balakrishnan and Wong, 1990] and [Laporte and Pesant, 2004]) that have been tested on three existing instances from literature. Table 1 provides the solving times for both of these approaches and MathSAT. Although the results cannot be compared directly due to different hardware specifications, it can be observed that MathSAT solves these three instances in a short span of time and thus is competitive with the two approaches.

We now compare the number of solutions and the runtimes to those of the First Class Scheduler (FCS) proposed by [Musliu et al., 2002], the min-conflicts heuristic with tabusearch algorithm (MC-T) of [Musliu, 2006] and the exact method developed by [Triska and Musliu, 2011] that uses constraint programming. MC-T solves all 20 instances, however, it is a heuristic technique and should therefore not be directly compared to the exact methods. It is more suitable to compare the SMT-technique to FCS [Musliu et al., 2002] and the constraint programming approach CP-Rota [Triska and Musliu, 2011], as these two are also exact methods.

In comparison to the First Class Scheduler, the SMT approach solves 5 instances more than FCS. While MathSAT can find a solution to the instances 9,12,13,17,19 and 20, FCS did not finish within 1000s on these instances. On the other hand, FCS is able to solve instance 7 which is not the case for any of the tested SMT-solvers in this paper.

Comparing the constraint programming approach CP-Rota to the results of MathSAT shows that CP-Rota solves 13 out of 20 instances, meaning five less than the SMT-solver. Although MathSAT is able to find a model for the instances 10, 11, 12, 18, 19 and 20, CP-Rota finds a solution for instance 7 in return. It is indeed surprising that the other exact methods were not only able to solve instance 7, but to do so in a short time. We could not find an explanation why SMT-solvers fail to find a solution for this instance, especially as they share many similarities with constraint programming techniques. Nevertheless, MathSAT has the highest solution rate of all exact methods considered in this paper.

Although these results indicate the superiority of SMTsolving over other exact methods, this conclusion should be taken with caution since the runtimes of these techniques were not measured on the same hardware and are therefore not directly comparable. We now have a look at the detailed solving times given in Table 2.

The runtimes show that the two approaches from literature achieve good results on a number of instances. This indicates that FCS and CP-Rota might achieve better results on a faster hardware and thus even outperform the MathSAT solver. However, the SMT approach is particularly fast on most instances (9, 10, 11, 12, 17, 18) that could not be solved by FCS or CP-Rota.

In conclusion, the encoding in SMT is an efficient approach to rotating workforce scheduling, which provides promising results when compared to other exact methods.

6 Conclusion

In this paper we proposed a new approach for solving the rotating workforce scheduling problem. By formulating rotating workforce scheduling as an SMT problem, we were able to use state-of-the-art solving tools (SMT-solvers) for the generation of cyclic workforce schedules. With the help of different background theories we developed two modeling approaches for the problem. Although encoding the problem with bitvectors and bit-level operations was a challenging task due to the complexity of the constraints, the assumption of the approach's superiority was indeed confirmed by the comparison of the experimental runtime results of the two modeling techniques. The competitiveness of solving the problem with SMT-solvers was verified by the comparison to other exact methods from literature. The results show that SMT-solving is a well performing alternative to these approaches, because it outperformed the other exact approaches on many instances and is able to provide a solution in a reasonable time frame for some instances where the other methods fail to do so.

Acknowledgments

The work was supported by the Austrian Science Fund (FWF): P24814-N23.