[Back]

F. Winter, N. Musliu, E. Demirovic, P. Stuckey:
"Solution-Based Phase Saving and MaxSAT for Employee Scheduling: A Computational Study";
Talk: 12th International Conference on the Practice and Theory of Automated Timetabling, Wien; 2018-08-28 - 2018-08-31; in: "12th International Conference on the Practice and Theory of Automated Timetabling", (2018), ISBN: 978-0-9929984-2-4; 453 - 457.

Employee scheduling is a well-known problem that appears in a wide-range of areas including healthcare, airlines, transportation services, and other workforce­related institutions. This problem arises whenever there is a need for effective management and distribution of workforce over periods of time. The task is to schedule the working times of employees while respecting the requirements defined by the given institution and labour laws. Finding the ideal workforce roster, however, is not an easy task: even a basic variant of employee schedul­ing was proved to be NP-hard [8]. In this paper, we study the applicability of solution-based phase saving, an existing but not widely-used technique [l], within the linear maxSAT algorithm [17] for employee scheduling. Following the line of work by [14], we model employee scheduling as a propositional Boolean formula, experimenting with four different cardinality constraint en­codings, and use a maximum Boolean satisfiability (maxSAT) solver to pro­vide solutions. Our results demonstrate that our approach outperforms previ­ous MaxSAT approaches. Furthermore, we show that MaxSAT solvers can be used to achieve competitive results for many instances when compared with existing metaheuristic techniques.

Employee scheduling is a well-known problem that appears in a wide-range of areas including healthcare, airlines, transportation services, and other workforce­related institutions. This problem arises whenever there is a need for effective management and distribution of workforce over periods of time. The task is to schedule the working times of employees while respecting the requirements defined by the given institution and labour laws. Finding the ideal workforce roster, however, is not an easy task: even a basic variant of employee schedul­ing was proved to be NP-hard [8]. In this paper, we study the applicability of solution-based phase saving, an existing but not widely-used technique [l], within the linear maxSAT algorithm [17] for employee scheduling. Following the line of work by [14], we model employee scheduling as a propositional Boolean formula, experimenting with four different cardinality constraint en­codings, and use a maximum Boolean satisfiability (maxSAT) solver to pro­vide solutions. Our results demonstrate that our approach outperforms previ­ous MaxSAT approaches. Furthermore, we show that MaxSAT solvers can be used to achieve competitive results for many instances when compared with existing metaheuristic techniques.

Solution-Based Phase; Saving; MaxSAT; Employee; Scheduling; Computational; Study

Project Head Nysret Musliu:
ARTIOS