基于SAT求解分布式柔性作业车间调度问题
Solving Distributed Flexible Job Shop Scheduling Problem Using SAT
AI总结：
本文提出一种基于SAT的精确方法求解分布式柔性作业车间调度问题，在76个基准实例中使72个实例达到最优，部分实例改进了最佳完工时间，是有效的互补精确方法。
摘要：
分布式柔性作业车间调度问题（DFJSP）需要联合确定工厂分配、机器选择和工序排序，以最小化总完工时间（makespan）。本文提出一种基于SAT的精确方法，该方法构建于高效的SAT公式之上，通过传播、对称性破缺和增量SAT求解利用问题结构，有效解决这些耦合决策。在Fattahi、Brandimarte和rdata数据集的76个标准基准实例上，针对两工厂和三工厂配置对所提方法进行评估。结合先前已有的结果，新的SAT最优性证明使76个实例中已证明最优的实例总数达到72个，其中包括3个新验证的实例；对于其中2个实例，SAT还改进了先前已知的最佳完工时间。在基准配置中，SAT在5种配置中的4种上取得最佳结果，并且与CP、LBBD1_CPIL等强大的精确方法以及现有元启发式方法相比仍具有竞争力。这些结果表明，所提SAT框架是DFJSP的有效精确方法，兼具优异的解质量与严格的最优性证明，为未来DFJSP研究及额外基准实例评估提供了互补的精确方法。
英文摘要：
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.
机构、总结、中文摘要均由AI分析而来，可能存在错误，请以论文正文为准。
