SMT Solvers for Flexible Job-Shop Scheduling Problems: A Computational Analysis

摘要

In this paper we evaluate different formulations for solving the Flexible Job-shop Scheduling Problem (FJSP) to optimality. Heuristic methods resulting in sub-optimal solutions are traditionally used to solve this problem since it is a known NP-hard problem. Since industrial problems often have additional constraints that need to be considered during optimization, the heuristic methods need to be adapted to deal efficiently with the additional constraints. For this reason general-purpose solvers that are often used in industrial applications. There are different approaches to formulate FJSPs as Mixed-Integer Linear Programming problems (MILP) that can be solved using generic MILP-solvers. In recent years, satisfiability solvers, i.e. SAT- and SMT-solvers, have evolved within the formal verification community and shown to be able to efficiently solve large instances of well-known NP-hard problems. In our previous work we have shown that SMT-solvers extended with optimization techniques can be a competitive alternative to commercial MILP-solvers on traditional job-shop scheduling problems. In this work we have adapted three formulations used for formulating FJSPs for MILP solvers into SMT-formulations. The three formulations are used to solve benchmark FJSPs using the open-source Z3 SMT-solver. We show that the a formulation based on the Manne formulation adapted for SMT-formulations for FJSPs is a competitive alternative for solving large-scale FJSPs, and might be considered as a viable alternative for solving industrial problems.