Personnel Scheduling as Satisfiability Modulo Theories

Personnel Scheduling as Satisfiability Modulo Theories

Christoph Erkinger, Nysret Musliu

Proceedings of the Twenty-Sixth International Joint Conference on Artificial Intelligence
Main track. Pages 614-621. https://doi.org/10.24963/ijcai.2017/86

Rotating workforce scheduling (RWS) is an important real-life personnel rostering problem that appears in a large number of different business areas. In this paper, we propose a new exact approach to RWS that exploits the recent advances on Satisfiability Modulo Theories (SMT). While solving can be automated by using a number of so-called SMT-solvers, the most challenging task is to find an efficient formulation of the problem in first-order logic. We propose two new modeling techniques for RWS that encode the problem using formulas over different background theories. The first encoding provides an elegant approach based on linear integer arithmetic. Furthermore, we developed a new formulation based on bitvectors in order to achieve a more compact representation of the constraints and a reduced number of variables. These two modeling approaches were experimentally evaluated on benchmark instances from literature using different state-of-the-art SMT-solvers. Compared to other exact methods, the results of this approach showed an important improvement in the number of found solutions.
Keywords:
Constraints and Satisfiability: Constraint Satisfaction
Constraints and Satisfiability: Modeling/Formulation
Planning and Scheduling: Scheduling
Constraints and Satisfiability: Constraints and Satisfiability