An Efficient MaxSAT-DDD Approach for Train Rescheduling via Precedence Propagation and Hybrid AMO Encodings
2026-06-15 • Logic in Computer Science
Logic in Computer Science
AI summaryⓘ
The authors worked on fixing train schedules when there are disruptions, making sure trains keep the right order, resources are used properly, and delays are minimized. They improved a method called Dynamic Discretization Discovery (DDD) by better handling resource conflicts and starting with earliest possible times for trains. They tested their improvements on multiple scenarios and found their approach runs much faster than older methods. Overall, their changes made solving complex rescheduling problems quicker and more efficient.
Train reschedulingDynamic Discretization Discovery (DDD)MaxSATResource capacityTimetable optimizationDelay objectivesEncodingSequential counterMILPConstraint programming (CP)
Authors
Tuyen Van Kieu, Tan Huu Nguyen, Khanh Van To
Abstract
Train rescheduling repairs disturbed timetables while enforcing train-path precedence, resource capacity, and delay objectives. Dynamic Discretization Discovery (DDD) avoids full time discretization by refining only time points needed to certify feasibility and optimality. We strengthen a recent MaxSAT-DDD model through two encoding changes. First, resource conflicts are encoded as time-dependent at-most-one cliques, using pairwise clauses for small cliques and a sequential counter for large cliques. Second, earliest feasible times are propagated along train paths before the first DDD iteration. We evaluate four MaxSAT variants, two SAT optimization backends, Gurobi/CPLEX MILP models, and CPLEX CP on 72 instances and three delay objectives. MaxSAT-DDD solves all stepwise instances in about 23 ms on average. MaxSAT-Default reduces rounded-cost runtime from 794 to 479 ms, and the ablation study reports up to 79.6\% runtime reduction on the common-solved subset of hard continuous track instances.