arXiv:2505.10328v1 人员调度类型: 新 摘要：人员调度对医疗服务质量和工作人员工作条件的影响已经被充分记录。然而，不断增长的需求和广泛存在的约束变化使得医疗人员调度变得尤为挑战。这个问题已经研究了几十年，但很少有关于如何将适应性逻辑谓词演算（Satisfiability Modulo Theories, SMT）应用于该领域的研究。在过去的几十年里，SMT 在形式验证社区中取得了很大进展，导致了性能优于标准数学规划方法的 SMT 求解器的发展。 在本文中，我们提出了通用的约束表达式，可以 modeling 各种实际的调度约束。然后，这些通用约束被表述为 SMT 和混合整数线性规划（MILP）问题，并用于在学术问题和基于现实世界的排班问题上比较最新的 SMT 求解器 Z3 和 MILP 求解器 Gurobi。实验结果展示了每种求解器在特定类型问题上的优势；当问题高度受限或不可行时，MILP 求解器表现更优，而 SMT 求解器在其他情况下表现更好。在包含更广泛轮班和人员的选择的实际问题中，SMT 求解器表现出色。此外，在实验中发现，SMT 求解器对通用约束的表述方式更为敏感，需要仔细考虑和实验以获得更好的性能。我们得出结论，基于 SMT 的方法为医疗人员调度领域未来的研究提供了一个有前景的途径。