A Comparative Study of SMT and MILP for the Nurse Rostering Problem

TL;DR

This paper compares SMT and MILP approaches for nurse rostering, showing that SMT performs better on diverse, real-world inspired problems, while MILP excels in highly constrained scenarios, highlighting the potential of SMT in healthcare scheduling.

Contribution

The study introduces generic constraint formulations for scheduling and compares SMT and MILP solvers, demonstrating the strengths of SMT in varied, real-world nurse rostering problems.

Findings

SMT outperforms MILP on real-world inspired scheduling problems.

MILP performs better on highly constrained or infeasible problems.

SMT solver's performance is sensitive to constraint formulation.

Abstract

The effects of personnel scheduling on the quality of care and working conditions for healthcare personnel have been thoroughly documented. However, the ever-present demand and large variation of constraints make healthcare scheduling particularly challenging. This problem has been studied for decades, with limited research aimed at applying Satisfiability Modulo Theories (SMT). SMT has gained momentum within the formal verification community in the last decades, leading to the advancement of SMT solvers that have been shown to outperform standard mathematical programming techniques. In this work, we propose generic constraint formulations that can model a wide range of real-world scheduling constraints. Then, the generic constraints are formulated as SMT and MILP problems and used to compare the respective state-of-the-art solvers, Z3 and Gurobi, on academic and real-world inspired rostering problems. Experimental results show how each solver excels for certain types of problems; the MILP solver generally performs better when the problem is highly constrained or infeasible, while the SMT solver performs better otherwise. On real-world inspired problems containing a more varied set of shifts and personnel, the SMT solver excels. Additionally, it was noted during experimentation that the SMT solver was more sensitive to the way the generic constraints were formulated, requiring careful consideration and experimentation to achieve better performance. We conclude that SMT-based methods present a promising avenue for future research within the domain of personnel scheduling.