Sat solves factory scheduling problems with better optimal results
Solving Distributed Flexible Job Shop Scheduling Problem Using SAT
Logic in Computer Science
Summary
Scheduling jobs across factories and machines is a complex problem where the goal is to finish all work as quickly as possible. The authors developed a method using a computer logic system called SAT to find the best schedules exactly. Their approach improves known solutions for many standard test problems and proves the solutions are optimal. This method competes well against other advanced techniques and can help improve scheduling decisions in multiple factories.
What this means in practice
- •For manufacturing schedulers: Generate optimal job schedules over multiple factories and machines, reducing total production time with guaranteed best solutions.
- •For industrial automation engineers: Integrate the SAT-based scheduling method to improve factory resource allocation and operation sequencing for complex manufacturing systems.
Authors
Phuong Dang Anh, Duc Nguyen Kim Trung, To Van Khanh
Abstract
The Distributed Flexible Job Shop Scheduling Problem (DFJSP) requires the joint determination of factory assignment, machine selection, and operation sequencing to minimize the makespan. This paper presents an exact SAT-based approach built on an efficient SAT formulation that exploits problem structure through propagation, symmetry breaking, and incremental SAT solving to effectively address these coupled decisions. The proposed method is evaluated on 76 standard benchmark instances from the Fattahi, Brandimarte, and rdata datasets under two- and three-factory configurations. Together with previously established results, the new SAT optimality certificates bring the total number of proven-optimal instances to 72 out of 76, including three newly certified instances; for two of these instances, SAT also improves the previous best-known makespans. Across the benchmark configurations, SAT achieves the best results on four of the five configurations and remains competitive with strong exact approaches such as CP and LBBD1_CPIL, as well as existing metaheuristic methods. These results demonstrate that the proposed SAT framework is an effective exact approach for the DFJSP, combining strong solution quality with rigorous optimality certification and offering a complementary exact method for future DFJSP studies and evaluations on additional benchmark instances.