SMT 与 MILP 用于护士排班问题的比较研究

人员排班对医疗机构护士的护理质量和工作条件具有明确的影响。然而，需求持续存在且约束差异大，使得医疗排班问题尤为具有挑战性。该问题已研究了数十年，仅有少量研究旨在应用满足模理论 (SMT)。SMT 在形式化验证领域近些年获得了热度，推动了 SMT 求解器的发展，这些求解器已显示出优于标准数学编程技术的性能。本文提出了能够建模广泛现实世界排班约束的通用约束公式。然后，将通用约束建模为 SMT 和 MILP 问题，用于比较 Z3 和 Gurobi 两种主流求解器在学术和现实世界灵感排班问题上的表现。实验结果表明，每个求解器在特定类型问题中都有优势；MILP 求解器在问题高度受限或不可行时通常表现更好，而 SMT 求解器在其他情况下表现更佳。在包含更多样化班次和人员的现实世界灵感问题中，SMT 求解器更占优势。此外，实验中注意到 SMT 求解器对通用约束的建模方式更敏感，需要仔细考虑和实验以获得更好的性能。我们得出结论，SMT 方法为人员排班领域的未来研究提供了有前景的方向。