An Efficient MaxSAT-DDD Approach for Train Rescheduling via Precedence Propagation and Hybrid AMO Encodings

Technical Summary: An Efficient MaxSAT-DDD Approach for Train Rescheduling

Problem Formulation
The paper addresses the fixed-route train rescheduling problem (TRP), where the goal is to repair disturbed timetables while enforcing train-path precedence, resource capacity constraints, and minimizing delay objectives. The problem assumes fixed routes for trains, simplifying the search space but limiting applicability to minor delay recovery scenarios rather than large-scale disruptions requiring rerouting. The model incorporates:

• Precedence Constraints: Ensuring the order of operations along a train's path.
• Resource Safety: Disjunctive constraints preventing trains from occupying the same resource (block section, track, or station) simultaneously.
• Delay Objectives: Three cost functions are evaluated: Stepwise (penalties for exceeding specific thresholds), Rounded (penalties based on 180-minute granularity), and Continuous (linear delay cost).

The authors utilize Dynamic Discretization Discovery (DDD) to avoid the computational intractability of full time discretization. Instead, DDD solves restricted time-indexed models and iteratively refines only the time points necessary to certify feasibility and optimality.

Methodology
The core contribution is a strengthened MaxSAT-DDD encoding that integrates two specific improvements into the refinement loop:

1. Hybrid AMO (At-Most-One) Encodings for Resource Conflicts:

   • Resource conflicts are modeled as time-dependent occupation cliques.
   • The authors replace standard pairwise exclusions (which generate $\Theta(n^2)$ clauses) with a hybrid approach. For small cliques ($n < 6$), pairwise clauses are retained. For larger cliques, they employ Sinz's sequential-counter encoding, which reduces the clause count to linear complexity ($O(n)$).
   • This encoding links indicator variables to "ladder literals" that define whether a train occupies a resource at a specific time point.

2. Train-Path Precedence Propagation:

   • Before the first DDD iteration, the solver performs a forward pass to compute effective earliest times ($t^{eff}$) for each operation along a train's route.
   • This propagation tightens the initial lower-bound ladders by enforcing that the start time of an operation must be at least the end time of the preceding operation plus traversal time.
   • This preprocessing step is linear in the total route length and preserves all feasible schedules while pruning the search space early.

Solver Architecture
The proposed solver, MaxSAT-Default, combines these two improvements. It operates within a DDD loop that alternates between:

1. Solving a restricted weighted partial MaxSAT instance (hard clauses for feasibility, soft clauses for delay costs).
2. Decoding the solution to check for violations.
3. Refining time intervals and adding new path/resource/cost clauses if violations or objective inconsistencies are found.
   The study compares this against a baseline MaxSAT encoding, incremental and non-incremental SAT backends (RC2, Glucose 4.2), and commercial solvers (Gurobi, CPLEX) using Big-M MILP, Time-Indexed (TI) MILP, and Constraint Programming (CP) formulations.

Key Contributions

• Encoding Efficiency: The integration of sequential-counter AMO encoding for large resource cliques significantly reduces the CNF size and improves unit propagation speed compared to pairwise encodings.
• Search Space Pruning: Precedence propagation tightens initial bounds, reducing the number of DDD iterations and solver backtracking, particularly for continuous delay objectives.
• Empirical Evaluation: A comprehensive evaluation on 72 instances across three delay objectives, comparing four MaxSAT variants against state-of-the-art MILP and CP baselines.

Experimental Results
The experiments were conducted on a benchmark derived from the Norwegian Bergen Line, featuring 25–30 trains and varying levels of resource aggregation (original, track, station).

• Stepwise Objectives: MaxSAT-Default solved all 72 instances with an average runtime of 23 ms, matching the solved count of Gurobi's Big-M MILP but being approximately 16 times faster on average.
• Rounded Objectives: MaxSAT-Default reduced the average runtime from 794 ms (baseline) to 479 ms without changing the number of solved instances. On hard continuous track instances, the ablation study showed up to a 79.6% runtime reduction on the common-solved subset.
• Continuous Objectives: While Big-M MILP (Gurobi) remained the strongest baseline for continuous delays, MaxSAT-Default still improved upon the baseline MaxSAT encoding, solving 60 instances compared to 59, with reduced runtimes.
• Hard Instances: On dense, aggregated instances (e.g., trackA8, stationA8), MaxSAT-Default consistently outperformed the baseline and often outperformed TI-MILP and CP approaches, which frequently timed out or exhausted memory.

Significance and Claims
The paper claims that the proposed MaxSAT-DDD approach is highly effective for discrete delay objectives (stepwise and rounded), offering a significant speedup over baseline MaxSAT and competitive performance against commercial MILP solvers. The authors note that while the fixed-route assumption limits the scope to minor delay recovery, the work provides a necessary foundation for exact methods in this domain.

The study modestly concludes that for continuous delay objectives, Big-M MILP remains superior, and the MaxSAT approach is most valuable for accelerating the search on hard subsets rather than strengthening lower bounds. The primary value of the proposed encoding lies in its ability to handle resource aggregation efficiently and reduce the computational overhead of the DDD refinement loop. Future work is identified as scaling the model to handle rerouting and strengthening lower bounds for continuous costs.