An Efficient MaxSAT-DDD Approach for Train Rescheduling via Precedence Propagation and Hybrid AMO Encodings (opens in new tab)

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 s...