Abstract
The effects of personnel scheduling on the quality of care and workingconditions for healthcare personnel have been thoroughly documented. However,the ever-present demand and large variation of constraints make healthcarescheduling 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 lastdecades, leading to the advancement of SMT solvers that have been shown tooutperform standard mathematical programming techniques. In this work, wepropose generic constraint formulations that can model a wide range ofreal-world scheduling constraints. Then, the generic constraints are formulatedas SMT and MILP problems and used to compare the respective state-of-the-artsolvers, 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 highlyconstrained or infeasible, while the SMT solver performs better otherwise. Onreal-world inspired problems containing a more varied set of shifts andpersonnel, the SMT solver excels. Additionally, it was noted duringexperimentation that the SMT solver was more sensitive to the way the genericconstraints were formulated, requiring careful consideration andexperimentation to achieve better performance. We conclude that SMT-basedmethods present a promising avenue for future research within the domain ofpersonnel scheduling.