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.

Multi-agent Path Finding (MAPF) is the problem of planning collision-free movements of agents so that they get from where they are to where they need to be. Commonly, agents are located on a graph and can traverse edges. This problem has many variations and has been studied for decades. Two such variations are the continuous-time and the lifelong MAPF problems. In the former, edges have non-unit lengths and volumetric agents can traverse them at any real-valued time. In the latter, agents must attend to a continuous stream of incoming tasks. Much work has been devoted to designing solution methods within these two areas. To our knowledge, however, the combined problem of continuous-time lifelong MAPF has yet to be addressed.This work addresses continuous-time lifelong MAPF with volumetric agents by presenting the fast and sub-optimal Continuous-time Prioritized Lifelong Planner (CPLP). CPLP continuously assigns agents to tasks and computes plans using a combination of two path planners; one based on CCBS and the other based on SIPP. Experimental results with up to 800 agents on graphs with up to 12000 vertices demonstrate practical performance, where maximum planning times fall within the available time budget. Additionally, CPLP ensures collision-free movement even when failing to meet this budget. Therefore, the robustness of CPLP highlights its potential for real-world applications.

Increased demand for healthcare services is placing a significant strain on hospitals. Prolonged waiting times for patients are becoming commonplace, while healthcare staff are subjected to unsustainable workloads. Finding ways to increase patient flow through hospital departments is one crucial step toward efficient healthcare services.In this work, a modelling framework is proposed to model patient flow though a healthcare department. Patient progression and resource allocation is simulated, offering insights into expected outcomes, bottlenecks, and other inefficiencies.A discrete-event model of a hospital department is formulated and proposed to be used together with Monte Carlo simulations. Patient treatment is represented by a series of processes, each consisting of smaller tasks. Medical staff members are represented as resources with specific qualifications that decide what tasks they may execute. Resources are allocated dynamically to model department-specific procedures, therefore increasing the flexibility of the proposed framework and opening up modelling possibilities to different healthcare departments.A real-world healthcare department is modelled and simulated using historic data and expert knowledge. In this way, the modelling flexibility of the framework is shown. Comparisons between simulation results and actual outcomes highlight the importance of establishing high-quality quantitative data collection in healthcare departments at an early stage to provide a stable foundation for operational modelling research. With accurate process times and resource usage data, the proposed framework has the potential to serve as an important support function, and ultimately contribute to a more sustainable and efficient healthcare.