본 논문은 의료 인력 스케줄링 문제에 Satisfiability Modulo Theories (SMT) 기반 접근법을 제안합니다. 기존 연구에서 의료 인력 스케줄링의 어려움과 제약 조건의 다양성을 다룬 바 있지만, SMT를 적용한 연구는 제한적이었습니다. 본 연구는 다양한 현실 세계 제약 조건을 모델링할 수 있는 일반적인 제약 조건 공식을 제시하고, 이를 SMT와 MILP 문제로 공식화하여 최첨단 솔버인 Z3와 Gurobi를 비교 분석합니다. 실험 결과, MILP 솔버는 제약 조건이 많거나 불가능한 문제에서 더 나은 성능을 보였고, SMT 솔버는 그렇지 않은 경우 더 나은 성능을 보였습니다. 특히 다양한 교대 근무와 인력을 포함하는 현실 세계 문제에서는 SMT 솔버가 우수한 성능을 나타냈습니다. 하지만 SMT 솔버는 제약 조건 공식화에 민감하여 성능 향상을 위해 신중한 고려와 실험이 필요하다는 점을 발견했습니다. 결론적으로 SMT 기반 방법은 의료 인력 스케줄링 분야의 미래 연구에 유망한 방향을 제시합니다.
