Charles Explorer logo
🇬🇧

Benders Decomposition in SMT for Rescheduling of Hierarchical Workflows

Publication at Faculty of Mathematics and Physics |
2017

Abstract

Real-life scheduling has to face many difficulties such as dynamic manufacturing environments with failing resources and urgent orders arriving during the schedule execution. Complete rescheduling, considering only the original objective function, in response to unexpected events occurring on the shop floor may yield schedules that are prohibitively different from the original schedule, which may lead to extra costs due to impacts on other planned activities.

Our novel approach in the area of predictive-reactive scheduling is to allow for substitution of jobs which cannot be executed with a set of alternative jobs. Hence, this paper describes the model of hierarchical work-flows suitable for dealing with unforeseen events using the possibility of alternative processes and proposes a new approach, based on the Satisability Modulo Theories (SMT) formalism, to recover an ongoing schedule from a resource failure.

The experimental results show that the SMT approach using Benders decomposition is orders of magnitude faster than a Constraint Programming approach.