This project aims to develop techniques for a variety of important scheduling problems that occur frequently, yet are inadequately addressed by current techniques. The research will be done in the context of a particular application--patient scheduling for medical clinics and it will involve a Michigan clinic that works with patients with traumatic brain injury. This application context has three characteristics that make it challenging. First, it is dynamic, in that events, such as patient appointments, as well as constraints on the times of the events change over time. Second, it involves both hard constraints (e.g., that no appointments can be scheduled earlier than a given time), as well as so-called "soft" constraints that represent preferences over alternative schedules (e.g., that a particular patient prefers afternoon appointments, or that it is better not to have large gaps between the appointments a patient has on a given day). Third, it is interactive: a human being is responsible for specifying events, constraints, and preferences.
To create an effective scheduler, we will extend a well-studied class of constraint-satisfaction systems: Satisfiability Modulo Theory (SMT) solvers. A key goal of this project is to enable SMT solvers to perform optimization efficiently and to develop algorithms for solving sequences of problems in a way that minimizes change across solutions while still producing near-optimal results. The project will also develop interfaces that make it possible for lay users to describe richly expressive constraints and preferences on schedules.
The broader impact of the work includes the potential usefulness of the techniques to key applications including clinic scheduling; the exposure of graduate students to contextual research; and the development of real-world problem sets for undergraduate courses.