Demirovic, E., Musliu, N., & Winter, F. (2019). Modeling and solving staff scheduling with partial weighted maxSAT. Annals of Operations Research, 275(1), 79–99. https://doi.org/10.1007/s10479-017-2693-y
E192-02 - Forschungsbereich Databases and Artificial Intelligence
-
Journal:
Annals of Operations Research
-
ISSN:
0254-5330
-
Date (published):
2019
-
Number of Pages:
21
-
Peer reviewed:
Yes
-
Keywords:
Management Science and Operations Research; General Decision Sciences; Employee scheduling; maxSAT; SAT encodings; Cardinality constraints
-
Abstract:
Employee scheduling is a well known problem that appears in a wide range of different areas including health care, air lines, transportation services, and basically any organization that has to deal with workforces. In this paper we model a collection of challenging staff scheduling instances as a weighted partial Boolean maximum satisfiability (maxSAT) problem. Using our formulation we conduct a comparison of four different cardinality constraint encodings and analyze their applicability on this problem. Additionally, we measure the performance of two leading solvers from the maxSAT evaluation 2015 in a series of benchmark experiments and compare their results to state of the art solutions. In the process we also generate a number of challenging maxSAT instances that are publicly available and can be used as benchmarks for the development and verification of modern SAT solvers.
