Modeling and solving staff scheduling with partial weighted maxSAT
将员工排班问题建模为加权部分布尔最大可满足性问题，比较四种基数约束编码，并用两个求解器在基准测试中对比性能，生成公开的挑战性实例供后续研究。
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.