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.

The Conflict-Free Electric Vehicle Routing Problem (CF-EVRP) is an extension of the Vehicle Routing Problem (VRP), a combinatorial optimization problem of designing routes for vehicles to visit customers such that a cost function, typically the number of vehicles or the total travelled distance, is minimized. The problem finds many logistics applications, particularly for highly automated logistic systems for material handling. The CF-EVRP involves constraints such as time windows on the delivery to the customers, limited operating range of the vehicles, and limited capacity on the number of vehicles that a road segment can accommodate at the same time. In this paper, the compositional algorithm ComSat for solving the CF-EVRP is presented. The algorithm iterates through the sub-problems until a globally feasible solution is found. The proposed algorithm is implemented using an optimizing SMT-solver and is evaluated against an implementation of a previously presented monolithic model. The soundness and completeness of the algorithm are proven, and it is benchmarked on a set of generated problems and found to be able to solve problems of industrial size.Note to Practitioners—The need to define and solve the CF-EVRP relates to an industrial application where a fleet of autonomous robots navigates in a heterogeneous environment, shared with humans and other vehicles and obstacles. To allow for a low-level trajectory controller to handle dynamic obstacles, like humans and fork-lifts, the CF-EVRP includes capacity constraints on the road segments. This increases the problem complexity, and thus requires to trade off optimality for feasability; this so to get solutions in reasonable time with respect to how long ahead the jobs to schedule are known. The overall problem is to find feasible solutions that satisfy all constraints while avoiding travelling unnecessarily long routes, and at the same time meet the stipulated time-windows to deliver material just-in-time. The compositional algorithm (ComSat) presented in this work is based on the idea to break down the overall scheduling problem into sub-problems that are easier to solve, and then to build a schedule based on the solutions of the sub-problems. ComSat is designed to work well for industrial scenarios where there are good reasons to believe that feasible solutions do exist. This seems a reasonable assumption as in an industrial setting a sufficient number of mobile robots can typically be assumed to be available.

Bin packing and bin covering are important optimization problems in many industrial fields, such as packaging, recycling, and food processing. The problem concerns a set of items, each with its own value, that are to be sorted into bins in such a way that the total value of each bin, as measured by the sum of its item values, is not above (for packing) or below (for covering) a given target value. The optimization problem concerns minimizing, for bin packing, or maximizing, for bin covering, the number of bins. This is a combinatorial NP-hard problem, for which true optimal solutions can only be calculated in specific cases, such as when restricted to a small number of items. To get around this problem, many suboptimal approaches exist. This article describes the formulations of the bin packing and covering problems that allow finding the true optimum, for instance, counting hundreds of items using general-purpose MILP-solvers. Also presented are suboptimal solutions that come within less than 10% of the optimum while taking significantly less time to calculate, even ten to 100 times faster, depending on the required accuracy.