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

Technische Samenvatting: Een Efficiënte MaxSAT-DDD Aanpak voor Treinherplanning

Probleemformulering
Het artikel behandelt het probleem van de herplanning van treinen met vaste routes (fixed-route train rescheduling, TRP), waarbij het doel is om verstoorde dienstregelingen te herstellen terwijl de volgorde van operaties langs een treinpad, de capaciteit van middelen en de vertragingsdoelstellingen worden gehandhaafd. Het probleem gaat uit van vaste routes voor treinen, wat de zoekruimte vereenvoudigt maar de toepasbaarheid beperkt tot scenario's met kleine vertragingen in plaats van grootschalige verstoringen die herroutering vereisen. Het model bevat:

• Precedentiebeperkingen: Het waarborgen van de volgorde van operaties langs het pad van een trein.
• Veiligheid van middelen: Disjunctieve beperkingen die voorkomen dat treinen gelijktijdig hetzelfde middel (bloksectie, spoor of station) bezetten.
• Vertragingsdoelstellingen: Drie kostenfuncties worden geëvalueerd: Stapgewijs (boetes bij het overschrijden van specifieke drempels), Afgerond (boetes op basis van 180-minuten granulariteit) en Continu (lineaire vertragingskosten).

De auteurs maken gebruik van Dynamic Discretization Discovery (DDD) om de computationele onhandelbaarheid van volledige tijdsdiscretisatie te vermijden. In plaats daarvan lost DDD beperkte tijd-geïndexeerde modellen op en verfijnt iteratief alleen de noodzakelijke tijdspunten om haalbaarheid en optimaliteit te certificeren.

Methodologie
De kernbijdrage is een versterkte MaxSAT-DDD codering die twee specifieke verbeteringen integreert in de verfijningslus:

1. Hybride AMO (At-Most-One) Coderingen voor Middelenconflicten:

   • Middelenconflicten worden gemodelleerd als tijd-afhankelijke bezettingscliques.
   • De auteurs vervangen standaard paarwijze uitsluitingen (die $\Theta(n^2)$ clausules genereren) door een hybride aanpak. Voor kleine cliques ($n < 6$) blijven de paarwijze clausules behouden. Voor grotere cliques gebruiken ze de Sinz's sequential-counter codering, wat het aantal clausules reduceert tot lineaire complexiteit ($O(n)$).
   • Deze codering koppelt indicatorvariabelen aan "ladder-literalen" die definiëren of een trein een middel op een specifiek tijdstip bezet.

2. Propagatie van Trein-Pad Precedentie:

   • Voordat de eerste DDD-iteratie plaatsvindt, voert de solver een forward pass uit om de effectieve vroegste tijden ($t^{eff}$) voor elke operatie langs de route van een trein te berekenen.
   • Deze propagatie verstrakt de initiële ondergrens-ladders door af te dwingen dat de starttijd van een operatie ten minste de eindtijd van de voorgaande operatie plus de reistijd moet zijn.
   • Deze preprocessing stap is lineair in de totale routelengte en behoudt alle haalbare schema's terwijl de zoekruimte vroegtijdig wordt afgesneden.

Solver Architectuur
De voorgestelde solver, MaxSAT-Default, combineert deze twee verbeteringen. Het opereert binnen een DDD-lus die afwisselt tussen:

1. Het oplossen van een beperkte gewogen partiële MaxSAT-instantie (harde clausules voor haalbaarheid, zachte clausules voor vertragingskosten).
2. Het decoderen van de oplossing om schendingen te controleren.
3. Het verfijnen van tijdsintervallen en het toevoegen van nieuwe pad-/middelen-/kostenclausules indien er schendingen of inconsistenties in de doelstelling worden gevonden.
   De studie vergelijkt dit met een baseline MaxSAT-codering, incrementele en niet-incrementele SAT-backends (RC2, Glucose 4.2), en commerciële solvers (Gurobi, CPLEX) met behulp van Big-M MILP, Time-Indexed (TI) MILP en Constraint Programming (CP) formuleringen.

Belangrijkste Bijdragen

• Coderingsefficiëntie: De integratie van de sequential-counter AMO-codering voor grote middelencliques vermindert de CNF-grootte aanzienlijk en verbetert de snelheid van unit propagation vergeleken met paarwijze coderingen.
• Afsnijding van de Zoekruimte: Precedentiepropagatie verstrakt de initiële grenzen, wat het aantal DDD-iteraties en het terugzoeken (backtracking) van de solver vermindert, met name voor continue vertragingsdoelstellingen.
• Empirische Evaluatie: Een uitgebreide evaluatie op 72 instanties over drie vertragingsdoelstellingen, waarbij vier MaxSAT-varianten worden vergeleken met state-of-the-art MILP en CP baselines.

Experimentele Resultaten
De experimenten werden uitgevoerd op een benchmark afgeleid van de Noorse Bergenlijn, met 25–30 treinen en variërende niveaus van middelenaggregatie (origineel, spoor, station).

• Stapgewijze Doelstellingen: MaxSAT-Default loste alle 72 instanties op met een gemiddelde runtime van 23 ms, wat overeenkomt met het aantal opgeloste instanties van Gurobi's Big-M MILP, maar ongeveer 16 keer sneller is op gemiddelde basis.
• Afgeronde Doelstellingen: MaxSAT-Default reduceerde de gemiddelde runtime van 794 ms (baseline) naar 479 ms zonder het aantal opgeloste instanties te veranderen. Bij harde continue spoor-instanties liet de ablatie-studie een runtime-reductie van maar liefst 79,6% zien op de gemeenschappelijk opgeloste subset.
• Continue Doelstellingen: Hoewel Big-M MILP (Gurobi) de sterkste baseline bleef voor continue vertragingen, verbeterde MaxSAT-Default nog steeds de baseline MaxSAT-codering, waarbij 60 instanties werden opgelost tegenover 59, met gereduceerde runtimes.
• Hardere Instanties: Op dichte, geaggregeerde instanties (bijv. trackA8, stationA8), presteerde MaxSAT-Default consequent beter dan de baseline en presteerde vaak beter dan TI-MILP en CP-benaderingen, die vaak de tijd overschreden of het geheugen uitputten.

Betekenis en Claims
Het artikel beweert dat de voorgestelde MaxSAT-DDD aanpak zeer effectief is voor discrete vertragingsdoelstellingen (stapgewijs en afgerond), waarbij een aanzienlijke versnelling wordt geboden ten opzichte van de baseline MaxSAT en een concurrerende prestatie levert tegenover commerciële MILP-solvers. De auteurs merken op dat hoewel de vaste-route aanname de reikwijdte beperkt tot minder zware herplanning van vertragingen, het werk een noodzakelijke basis vormt voor exacte methoden in dit domein.

De studie concludeert bescheiden dat voor continue vertragingsdoelstellingen, Big-M MILP superieur blijft, en dat de MaxSAT-aanpak het meest waardevol is voor het versnellen van de zoektocht op harde subsets in plaats van het versterken van de ondergrenzen. De primaire waarde van de voorgestelde codering ligt in het vermogen om middelenaggregatie efficiënt af te handelen en de computationele overhead van de DDD-verfijningslus te verminderen. Toekomstig werk wordt geïdentificeerd als het schalen van het model om herroutering te kunnen afhanden en het versterken van de ondergrenzen voor continue kosten.