A Comparative Study of SMT and MILP for the Nurse Rostering Problem

要約

医療従事者のケアの質と労働条件に対する人員のスケジューリングの影響は、徹底的に文書化されています。
ただし、常に存在する需要と制約の大きな変動により、ヘルスケアのスケジューリングは特に困難になります。
この問題は数十年にわたって研究されており、限られた研究は満足度モジュロ理論（SMT）を適用することを目的としています。
SMTは、過去数十年で正式な検証コミュニティ内で勢いを増しており、標準的な数学プログラミング技術よりも優れていることが示されているSMTソルバーの進歩につながりました。
この作業では、幅広い現実世界のスケジューリング制約をモデル化できる一般的な制約定式化を提案します。
次に、一般的な制約はSMTおよびMILPの問題として策定され、学術的および実世界にインスパイアされた名簿の問題について、それぞれの最先端のソルバーであるZ3とGurobiを比較するために使用されます。
実験結果は、各ソルバーが特定の種類の問題にどのように優れているかを示しています。
MILPソルバーは通常、問題が高度に制約または実行不可能である場合にパフォーマンスが向上しますが、SMTソルバーはそうでない場合はパフォーマンスが向上します。
より多様なシフトと人員のセットを含む現実世界に触発された問題では、SMTソルバーが優れています。
さらに、実験中に、SMTソルバーは一般的な制約の策定方法により敏感であり、パフォーマンスを向上させるために慎重な検討と実験が必要であることが注目されました。
SMTベースの方法は、人事スケジューリングの領域内で将来の研究のための有望な手段を提示すると結論付けています。

要約(オリジナル)

The effects of personnel scheduling on the quality of care and working conditions for healthcare personnel have been thoroughly documented. However, the ever-present demand and large variation of constraints make healthcare scheduling 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 last decades, leading to the advancement of SMT solvers that have been shown to outperform standard mathematical programming techniques. In this work, we propose generic constraint formulations that can model a wide range of real-world scheduling constraints. Then, the generic constraints are formulated as SMT and MILP problems and used to compare the respective state-of-the-art solvers, 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 highly constrained or infeasible, while the SMT solver performs better otherwise. On real-world inspired problems containing a more varied set of shifts and personnel, the SMT solver excels. Additionally, it was noted during experimentation that the SMT solver was more sensitive to the way the generic constraints were formulated, requiring careful consideration and experimentation to achieve better performance. We conclude that SMT-based methods present a promising avenue for future research within the domain of personnel scheduling.

arxiv情報

提供元, 利用サービス

arxiv.jp, Google