1 Introduction and Related Work↩︎

Railway traffic management must react to delays, disrupted rolling stock, or temporary capacity reductions while keeping the resulting plan safe and close to the published timetable. In fixed-route train rescheduling, the dispatcher chooses entry times for resources such as block sections, tracks, and stations. This fixed-route assumption is a modeling choice that simplifies the scheduling search space; however, it limits applicability to minor delay recovery scenarios rather than large-scale disruptions where train rerouting, cancellations, or short-turnings are operationally required. The model contains train-path precedence and disjunctive safety constraints, which makes exact optimization difficult under real-time limits [1]–[3].

MILP formulations are the most common exact modelling tool for train rescheduling. Big-\(M\) formulations keep continuous time variables, but their linear relaxations are often weak. Time-indexed formulations replace temporal disjunctions by binary choices over a discretized horizon and usually give stronger combinatorial structure, but a full discretization can be too large and a coarse discretization can produce modelling errors. Dynamic Discretization Discovery (DDD) addresses this tension by solving restricted time-indexed models and refining only time points that violate the continuous-time constraints [4].

Croella et al. [5] encoded restricted DDD subproblems as weighted partial MaxSAT instances, with hard clauses for feasibility and soft clauses for delay cost. We keep that DDD proof structure and target two CNF bottlenecks that become visible under track and station aggregation. Aggregated resources create large conflict cliques, and pairwise exclusions then create \(\Theta(n^2)\) clauses. Initial lower-bound ladders also ignore path precedence, so early DDD iterations rediscover constraints already implied by each train route.

This paper develops a more structured MaxSAT-DDD encoding. The novelty is not a new DDD algorithm, but the integration of clique-based cardinality encoding and train-path bound propagation into the MaxSAT-DDD refinement loop, together with an empirical study of their behaviour under resource aggregation. The contributions are as follows.

• We encode resource conflicts as time-dependent occupation cliques and use a hybrid AMO encoding. Large cliques use the sequential-counter encoding of Sinz [6].

• We propagate effective earliest times along each train path before the first DDD iteration. This tightening is linear in the total route length and preserves all feasible schedules.

• We compare four MaxSAT variants, two SAT optimization backends, Gurobi and CPLEX MILP models, and a CPLEX CP model. We report feasible incumbents and proven optima separately.

The results show that MaxSAT-DDD is most effective for discrete delay objectives. Commercial Big-\(M\) MILP remains strongest on continuous delay, but MaxSAT-Default improves over the baseline MaxSAT encoding on rounded costs and on hard continuous subsets.

Table 1 classifies the main lines of railway rescheduling research. The surveys in [1], [2], [7] show that modelling choices depend on the operational scope, from microscopic safety constraints to large-network disruption management.

2.7pt

The closest line is logic-based exact optimization. SAT, ASP, and MaxSAT methods exploit the Boolean structure of restricted time-indexed models [16]–[18]. Our work keeps the DDD optimality logic of [5] and improves its generated CNF through sequential-counter resource cliques and precedence propagation.

2 Train Rescheduling Problem Formulation↩︎

Let \(I\) be the set of trains. Each train \(i\in I\) follows a fixed ordered route \(R_i=\langle r^i_1,\ldots,r^i_{|R_i|}\rangle\) through railway resources. The decision variable \(t^{ir}\) is the time at which train \(i\) enters resource \(r\in R_i\). The input provides an earliest local time \(\underline t^{ir}\), a minimum traversal or dwell time \(l_i^r\), and safety separations \(l_{ij}^{rq}\) for pairs of operations that cannot overlap. The planning horizon \(H\) bounds all entry times. Let \(a_i\) be the scheduled arrival time of train \(i\) at its destination \(r_i^{\mathrm{dest}}\), and define \(\delta_i=\max\{0,t^{i r_i^{\mathrm{dest}}}-a_i\}\).

A schedule is feasible when it satisfies the following constraints: \[\begin{align} t^{ir} &\ge \underline t^{ir}, && i\in I,\;r\in R_i, \tag{1}\\ t^{iq} &\ge t^{ir}+l_i^r, && r \prec_i q, \tag{2}\\ t^{jq} &\ge t^{ir}+l_{ij}^{rq} \quad \text{or}\quad t^{ir}\ge t^{jq}+l_{ji}^{qr}, && (r,q)\in\mathcal{D}_{ij}. \tag{3} \end{align}\] Constraint 1 enforces release times, 2 enforces the order of operations on a train path, and 3 enforces resource safety between trains. Separations \(l_{ij}^{rq}\) are computed from signaling rules: under fixed-block signaling, headway limits ensure train \(j\) cannot enter block \(q\) until train \(i\) clears \(r\) plus a safety margin; at stations, they represent route locking/releasing times. Traversal times \(l_i^r\) depend on speed limits and train dynamics. The objective is \(\min \sum_i c_i(\delta_i)\), with three delay-cost functions:

• Step: \(c_i(\delta)=\sum_k w_{ik}\mathbf{1}[\delta>\eta_{ik}]\).

• Round: \(c_i(\delta)=w_i\lceil\delta/180\rceil\), where the 180-minute granularity is inherited from the benchmarks of [5] (representing coarse step-like penalties).

• Cont: \(c_i(\delta)=w_i\delta\).

2.1 Illustrative Conflict-Resolution Example↩︎

Figure 1 shows two fixed-route trains with shared segments \(c\) and \(d\). Train 1 follows \(\langle a,c,d\rangle\) and Train 2 follows \(\langle b,c,d\rangle\), with traversal times of \(3, 5, 4, 3\) minutes on segments \(a,b,c,d\), respectively.

In Fig. 1 (a), the trains overlap on \(c\) and \(d\), violating 3 . Delaying Train 2 by two time units removes both conflicts and creates the rescheduled timetable in Fig. 1 (b).

3 Baseline MaxSAT-DDD Formulation↩︎

DDD stores a time partition \(\Lambda^{ir}\) for each operation \((i,r)\) and solves a restricted interval assignment problem. The selected interval left-endpoints define a lower-bound schedule. Violated path or resource constraints trigger interval refinement. If the decoded schedule is feasible and has the same cost as the restricted model, optimality is certified.

MaxSAT-DDD encodes each restricted model as weighted partial MaxSAT. Hard clauses enforce interval assignment, monotonicity, and discovered incompatibilities. Soft clauses encode delay costs. Ladder literals \(d^{ir}(\tau)\) represent \(t^{ir}\ge\tau\), and baseline resource conflicts are mostly pairwise exclusions over occupation events. For each destination-delay breakpoint \(\tau\), the soft literal \(\neg d^{i r_i^{\mathrm{dest}}}(a_i+\tau)\) carries the marginal cost increase \(c_i(\tau)-c_i(\tau^-)\). Step and rounded objectives have few breakpoints, whereas the continuous objective can create many unit-weight levels.

4 Proposed MaxSAT-DDD Encoding↩︎

4.1 Solver Architecture and Refinement Workflow↩︎

The solver first applies precedence propagation to tighten the initial ladders. The DDD loop then alternates between optimizing the restricted MaxSAT model and adding path, resource, or cost-refinement clauses until feasibility and objective consistency certify optimality.

4.2 Train-Path Precedence Propagation↩︎

The baseline initializes each operation from its local lower bound \(\underline t^{ir}\). For route \(R_i=\langle r^i_1,\ldots,r^i_{|R_i|}\rangle\), we instead compute effective earliest times by \[\begin{align} \underline t^{i r^i_1}_{\mathrm{eff}} &= \underline t^{i r^i_1}, \tag{4}\\ \underline t^{i r^i_{k+1}}_{\mathrm{eff}} &= \max\left\{\underline t^{i r^i_{k+1}}, \underline t^{i r^i_k}_{\mathrm{eff}}+l_i^{r^i_k}\right\}. \tag{5} \end{align}\] This forward pass costs \(O(\sum_i |R_i|)\) and removes no feasible schedule, because every solution satisfying 1 and 2 also satisfies \(t^{ir}\ge\underline t^{ir}_{\mathrm{eff}}\).

4.3 Sequential-Counter Encoding for Resource-Capacity Cliques↩︎

Fix a physical resource \(r\) and a time point \(\tau\). Let \(X_{r,\tau}=\{v_1,\ldots,v_n\}\) be the set of operations that may occupy \(r\) at \(\tau\) under the current DDD discretization. Safety requires at most one of these operations to be active: \[\mathrm{AMO}(x_{v_1},\ldots,x_{v_n}). \label{eq:amo}\tag{6}\] Each indicator \(x_v\) is linked to the ladder literals defining occupation at \(\tau\). Specifically, \(e_v(\tau)\) is defined as the ladder literal \(d^{i_v r_v^{\text{succ}}}(\tau+1)\) representing \(t^{i_v r_v^{\text{succ}}} \ge \tau+1\), while \(\neg d^{i_v r_v}(\tau+1)\) represents \(t^{i_v r_v} \le \tau\). Their conjunction \(\neg d^{i_v r_v}(\tau+1) \wedge d^{i_v r_v^{\text{succ}}}(\tau+1)\) captures that train \(i_v\) has entered resource \(r_v\) by time \(\tau\) but has not yet entered its successor \(r_v^{\text{succ}}\) at \(\tau\), meaning it occupies \(r_v\). The implication \[\mathrm{occ}(v,\tau)\rightarrow x_v\] is encoded by \[x_v \vee \neg e_v(\tau) \vee d^{i_v r_v}(\tau+1). \label{eq:occind}\tag{7}\] For a general disjunctive pair \((r,q)\in\mathcal{D}_{ij}\) with asymmetric separations, the unsafe time windows determine the occupation indicators; the AMO clique is then built only for indicators that are mutually incompatible at the same refined time point. The baseline pairwise AMO encoding adds \(\binom n2\) clauses \(\neg x_{v_a}\vee \neg x_{v_b}\). We replace it by a sequential counter for large cliques. With auxiliary prefix variables \(s_1,\ldots,s_{n-1}\), the clauses are written following Sinz [6] with explicit index ranges and a separate boundary case: \[\begin{align} \neg x_{v_1} \vee s_1, & \label{eq:sc} \\ \neg x_{v_j} \vee s_j, & \qquad (1 < j < n), \notag \\ \neg s_{j-1} \vee s_j, & \qquad (1 < j < n), \notag \\ \neg x_{v_j} \vee \neg s_{j-1}, & \qquad (1 < j < n), \notag \\ \neg x_{v_n} \vee \neg s_{n-1}. & \notag \end{align}\tag{8}\] Pairwise AMO is used when \(n < \theta\) (default \(\theta=6\)). This threshold is justified because \(n=6\) is the theoretical crossing point where the sequential counter encoding yields fewer clauses (\(3n - 4 = 14\)) than the pairwise encoding (\(n(n-1)/2 = 15\)). Since precedence propagation only raises lower bounds implied by 1 –2 and the sequential counter is equisatisfiable with pairwise AMO, this strengthened encoding preserves the exactness of the DDD optimum.

4.4 MaxSAT Optimization Strategy↩︎

MaxSAT-Default combines precedence propagation with the hybrid AMO policy. Algorithm 4 gives the full DDD loop. The SAT backends use the same refinement layer; only the optimization oracle changes.

4.4.1 Solver Configurations for the Comparative Study↩︎

Table 2 lists the evaluated configurations.

5pt

5 Computational Results and Experimental Analysis↩︎

5.1 Benchmark Instances and Infrastructure Abstractions↩︎

The benchmark from [5] models a busy corridor on the Norwegian Bergen Line, with single-track sections and siding tracks. The A-series has 25–30 trains, and the B-series is a smaller sub-corridor. Delays are generated via entry delays at the boundaries. Unlike [5] which only tested pairwise MaxSAT-Base, we evaluate precedence propagation, sequential counters, CP, and tuned MILP. The benchmark has 24 base instances (A1–A12 and B1–B12) under three abstractions:

• original: original block resources;

• track: parallel block sections on short track segments are grouped;

• station: resources inside a station are grouped into larger shared resources.

This gives 72 instances per objective. The hard subset contains trackA1, trackA2, trackA8, trackA11, trackA12, and the corresponding station instances; these are the larger A-series cases where aggregation creates denser resource conflicts.

5.2 Solver Backends, Hardware, and Optimality Criteria↩︎

All runs use a 120-second timeout and a 32 GB memory limit. For real-time dispatching, decisions are typically required within 30–60 seconds; instances solved within 30 seconds are considered operationally tractable. We report single-run times because the solvers (RC2 and Glucose 4.2) run in a fully deterministic mode with fixed seeds, ensuring zero runtime variance. The implementation is in Rust, with RC2, Glucose 4.2, Gurobi 12.0, CPLEX MILP, and CPLEX CP Optimizer under default single-run settings. Experiments use Ubuntu 22.04 and an Intel Core i7-13700K CPU. Average time is computed only over proved-optimal runs, so timeouts are reflected through the Opt., Feas., and gap columns rather than through penalized averages.

We evaluate all methods on 72 instances and three objectives. The main pattern is stable: MaxSAT-DDD is strongest on discrete delay objectives, while continuous delay favours Big-\(M\) MILP.

5.3 Aggregate Performance Across Delay Objectives↩︎

4.5pt

Table 3 shows a clear objective-dependent pattern. MaxSAT-Default matches the stepwise solved count of Gurobi Big-\(M\) while being about 16 times faster on average, and it reduces rounded-cost runtime from 794 ms to 479 ms without changing the solved count. Continuous delay is less favourable to the Boolean objective encoding: Gurobi Big-\(M\) gives the best aggregate time, although MaxSAT-Default still improves over MaxSAT-Base from 59 to 60 proved optima and from 5 181 ms to 4 881 ms.

5.4 Commercial MILP and Constraint-Programming Baselines↩︎

3.6pt

Table 4 separates feasible incumbents from optimality proofs. CP-CPLX finds a schedule for every instance, but gaps of 26–34% limit its value as a certificate baseline. Big-\(M\) MILP gives the strongest proof performance, whereas the time-indexed MILP is solver-sensitive: TI-GRB proves almost all cases, but TI-CPLX proves fewer than half and returns no incumbent outside the proved set. This TI-CPLX behavior (failing to find incumbents on unsolved instances) is a known characteristic of time-indexed MILP models: their huge LP relaxation size at the root node can overwhelm CPLEX’s default MIP heuristics before the timeout, whereas Gurobi’s heuristics are more aggressive in finding early feasible integer solutions.

5.5 Performance on Hard Track and Station Instances↩︎

4.5pt

The hard instances contain 25–30 trains and 500–636 operations. On the stepwise objective, Table 5 shows that both MaxSAT variants solve all hard instances within 250 ms, while PureSAT times out on four dense cases. MaxSAT-Default is fastest on five of the ten instances, including trackA8 and trackA12, so the added propagation and hybrid AMO policy do not harm the easiest discrete objective.

4.5pt

Table 6 shows where the Boolean encoding is most useful. On rounded trackA8 and stnA8, MaxSAT-Default improves over MaxSAT-Base by 41.7% and 40.7%, respectively; it is also more than an order of magnitude faster than Gurobi Big-\(M\) on trackA8. Continuous hard cases show the opposite pattern: Gurobi Big-\(M\) proves the smaller cases quickly, while SAT-based runs often time out or exhaust memory when many distinct cost levels are present.

5.6 Ablation of Sequential-Counter AMO and Precedence Propagation↩︎

4.5pt

Table 7 isolates the two improvements. The stepwise objective changes little, but MaxSAT-Default reduces rounded runtime by about 40% on both track and station abstractions and reduces continuous track runtime by 79.6% on the common-solved subset. Sequential-counter AMO is most visible on large track cliques, while precedence propagation is most useful when continuous-cost ladders create many candidate delay levels. The minor regression of MaxSAT-SC on continuous station instances (\(11\,503 \to 11\,827\) ms) is due to auxiliary variable overhead and VSIDS heuristic disruption on smaller cliques near the threshold. The common-solved subset of hard instances contains all 10 instances for Stepwise, 6 instances (A1, A2, A8) for Rounded (dropping A11–A12), and 2 instances (A1, A2) for Continuous (dropping A8, A11–A12).

3.8pt

Table 8 reports CNF size and DDD iterations. Rounded-cost speedups occur with similar formula sizes, so they should be attributed to the encoding structure and solver search behaviour rather than to size reduction alone. For continuous objectives, precedence propagation reduces the average size from 7 845 variables and 23 130 clauses to 7 382 variables and 21 772 clauses, while DDD iteration counts change only modestly. Specifically, the 79.6% runtime reduction on continuous track instances stems from slightly fewer iterations (\(\bar I = 216 \to 213\)), 7.4% fewer clauses, and faster MaxSAT calls. Precedence propagation prunes the search space early to reduce solver backtracking, while the sequential-counter AMO handles resource conflicts in \(O(n)\) time and clauses instead of \(O(n^2)\), accelerating unit propagation.

5.7 Optimality Gaps for Unsolved SAT and MaxSAT Runs↩︎

4.5pt

Table 9 lists instances unsolved by all SAT/MaxSAT methods. The optimality gap is \((\text{UB} - \text{LB}) / \text{UB} \times 100\%\), where \(\text{UB}\) is the best feasible objective value and \(\text{LB}\) is the proven lower bound. Gaps of 90%+ on continuous track and station instances (e.g., stationA11, trackA12) occur because the initial DDD discretization is very coarse, leaving initial lower bounds close to zero. Refinements raise these bounds slowly, so \(\text{LB} \approx 0\) at timeout. Due to space constraints, UBs are not tabulated, but MaxSAT-Default’s feasible costs are within 5% of Gurobi’s on instances where Gurobi proved optimality, confirming that these gaps are driven by weak lower bounds rather than poor solution quality. MaxSAT-Default and MaxSAT-Base have similar gaps, so the proposed encoding mainly accelerates search rather than strengthening the lower bound. IncSAT can tighten selected gaps through learned-clause reuse, e.g., 31.7% on rounded trackA11, but it is less reliable on continuous cases because memory pressure increases. Overall, MaxSAT-DDD is most attractive for threshold and rounded delay objectives, whereas continuous delay still favours Big-\(M\) MILP and calls for stronger lower bounds.

6 Conclusions and Future Work↩︎

We presented a MaxSAT-DDD approach that combines sequential-counter AMO encoding with train-path precedence propagation. MaxSAT-Default preserves the stepwise performance of the baseline, improves rounded-cost runtime, and helps on hard continuous subsets. While the fixed-route assumption limits the operational scope to minor delay recovery rather than large-scale disruptions, it serves as a necessary foundation for exact methods. Future work should focus on scaling the model to handle train rerouting, passenger connections, and uncertainty under larger disruptions, as well as strengthening continuous-cost lower bounds.

6.0.1 Data and Code Availability↩︎

The complete source code, benchmark datasets, and experimental artefacts used in this study are publicly available at https://github.com/maxsat-tsp/maxsattrainscheduling.

References↩︎