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