Workforce scheduling is a classical optimization problem. Improved schedules can be better both for the workers and for the business, but are often surprisingly hard to find. One common variant of scheduling is called Rotating Workforce Scheduling (shortened as RWS), and is sometimes called cyclic scheduling. In RWS, a weekly schedule is created for a group of workers covering the projected needs. Each worker will rotate through the schedule, working all different weeks.

Solving RWS is a challenging problem, both for manual and automatic approaches. This post will describe developing a reasonably realistic variant of finding an RWS schedule using MiniZinc. Starting with the basic structure and then adding more and more typical requirements to get realistic schedules.

In Solving LinkedIn Queens using MiniZinc I wrote about how to solve the LinkedIn Queens problem using MiniZinc, and showed a single example. In Solving LinkedIn Queens with Haskell I saw that there is a large set of instances available, so it's time to benchmark the different MiniZinc solvers.

The benchmarks test several different features, so first it's worth going deeper into what MiniZinc actually is and how it works. In addition, we will talk about how to benchmark solvers and what the different values mean.

Hillel Wayne wrote about solving the LinkedIn Queens problem with SMT in his Computer Things newsletter. This was in turn inspired by Ryan Berger's post Using SAT to Get the World Record on LinkedIn's Queens that solves the same problem using a SAT solver.

Not to be outdone, this post describes how to use MiniZinc to solve the problem in what I think is a more readable and natural expression of the model than either SAT or SMT. As always, YMMV and what is natural and clear to one person is opaque and weird to someone else.