Document Open Access Logo

Why Start Over: Incremental MaxSMT for Operational Railway Scheduling

Authors Thomas Dubach , Florian Flükiger-Fuchs , Bernardo Martin-Iradi

PDF

File

Thumbnail PDF
PDF
OASIcs.ATMOS.2026.4.pdf
  • Filesize: 1.65 MB
  • 19 pages

Document Identifiers

Subject Classification

ACM Subject Classification
  • Theory of computation → Constraint and logic programming
  • Applied computing → Transportation
  • Theory of computation → Integer programming
Keywords
  • MaxSAT
  • operational railway timetabling
  • incremental solving

Metrics

Abstract

Railway timetables are planned periodically, but operational planners continuously need to deviate from this base: extra trains are added, or infrastructure changes are made, requiring local updates to the existing schedule. We study this process as a sequential extra train scheduling problem, in which requests arrive one at a time and must be routed and timed against the existing timetable while minimising deviation from it. Commonly, each admitted train is fixed before the next request arrives, and all accumulated solver knowledge is discarded between calls.
We propose an incremental MaxSAT framework over Integer Difference Logic (MaxSMT) that retains accumulated solver state across successive extra-train additions, rather than solving from scratch after each request. We evaluate the approach on the Rhätische Bahn network using different solving strategies and compare against a MIP baseline. Retained solver state substantially reduces solve time for successive additions, increasingly so as more extra trains are admitted, and is an order of magnitude faster than MIP given the same setup. Beyond solving time, we show that jointly re-optimising over all admitted extra trains yields better cumulative objective values, and that our approach achieves this while prioritising adjustments in the timetable region affected by the new request.

Cite As Get BibTex

Thomas Dubach, Florian Flükiger-Fuchs, and Bernardo Martin-Iradi. Why Start Over: Incremental MaxSMT for Operational Railway Scheduling. In 26th Symposium on Algorithmic Approaches for Transportation Modelling, Optimization, and Systems (ATMOS 2026). Open Access Series in Informatics (OASIcs), Volume 147, pp. 4:1-4:19, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2026) https://doi.org/10.4230/OASIcs.ATMOS.2026.4

Author Details

Thomas Dubach
  • IVT Transport Systems Group, ETH Zurich, Switzerland
Florian Flükiger-Fuchs
  • IVT Transport Systems Group, ETH Zurich, Switzerland
Bernardo Martin-Iradi
  • IVT Transport Systems Group, ETH Zurich, Switzerland

Funding

  • Dubach, Thomas: ETH Mobility Initiative - Project LeRaBe

References

  1. Gabrio Caimi, Leo Kroon, and Christian Liebchen. Models for railway timetable optimization: Applicability and applications in practice. Journal of Rail Transport Planning & Management, 6(4):285-312, January 2017. URL: https://doi.org/10.1016/j.jrtpm.2016.11.002.
  2. SBB Infrastruktur / SBB Cargo. So entsteht der Fahrplan, April 2014. URL: https://blog.sbbcargo.com/wp-content/uploads/2014/11/A2_Plakat_Fahrplan_Infrastruktur_dt_Web.pdf.
  3. Pedro José Correia Duarte, Stéphane Dauzère-Pérès, Dennis Huisman, Carlo Mannino, Giorgio Sartor, Norman Weik, and Philipp Widmann. 50 years of OR in railway timetabling and rolling stock planning. EURO Journal on Transportation and Logistics, 14:100155, January 2025. URL: https://doi.org/10.1016/j.ejtl.2025.100155.
  4. Scott Cotton and Oded Maler. Fast and Flexible Difference Constraint Propagation for DPLL(T). In Armin Biere and Carla P. Gomes, editors, Theory and Applications of Satisfiability Testing - SAT 2006, pages 170-183, Berlin, Heidelberg, 2006. Springer. URL: https://doi.org/10.1007/11814948_19.
  5. Anna Livia Croella, Bjørnar Luteberget, Carlo Mannino, and Paolo Ventura. A MaxSAT approach for solving a new Dynamic Discretization Discovery model for train rescheduling problems. Computers & Operations Research, 167:106679, July 2024. URL: https://doi.org/10.1016/j.cor.2024.106679.
  6. Niklas Eén and Niklas Sörensson. MiniSat Page, September 2013. URL: http://minisat.se/.
  7. Florian Fuchs and Francesco Corman. An Open Toolbox for Integrated Optimization of Public Transport. In 2019 6th International Conference on Models and Technologies for Intelligent Transportation Systems (MT-ITS), pages 1-7, June 2019. URL: https://doi.org/10.1109/MTITS.2019.8883335.
  8. Florian Fuchs, Thomas Dubach, Jan Lordieck, Francesco Corman, and Bernardo Martin-Iradi. Handling conflicts in microscopic railway timetabling at scale: A parallelized approach. Journal of Rail Transport Planning & Management, 39:100600, September 2026. URL: https://doi.org/10.1016/j.jrtpm.2026.100600.
  9. Florian Fuchs, Bernardo Martin-Iradi, and Francesco Corman. Optimizing periodic stability in railway timetables: A microscopic model for networks with a macroscopic comparison. Journal of Rail Transport Planning & Management, 36:100555, December 2025. URL: https://doi.org/10.1016/j.jrtpm.2025.100555.
  10. Filipe Gouveia, Luís Albino, and Ricardo L. Saldanha. A MaxSAT Approach for the Train Timetabling Problem with Route Choice and Other Features. In José Valente de Oliveira, João Leite, João Rodrigues, João Dias, and Pedro Cardoso, editors, Progress in Artificial Intelligence, pages 179-191, Cham, 2026. Springer Nature Switzerland. URL: https://doi.org/10.1007/978-3-032-05179-0_14.
  11. Alexey Ignatiev, Antonio Morgado, and Joao Marques-Silva. RC2: an Efficient MaxSAT Solver. Journal on Satisfiability, Boolean Modeling and Computation, 11(1):53-64, September 2019. URL: https://doi.org/10.3233/SAT190116.
  12. Oddvar Kloster, Bjørnar Luteberget, Carlo Mannino, and Giorgio Sartor. An Optimization-Based Decision Support Tool for Incremental Train Timetabling. Operations Research Forum, 4(3):65, August 2023. URL: https://doi.org/10.1007/s43069-023-00243-2.
  13. Alexandre Lemos, Filipe Gouveia, Pedro T. Monteiro, and Inês Lynce. Iterative Train Scheduling under Disruption with Maximum Satisfiability. Journal of Artificial Intelligence Research, 79:1047-1090, March 2024. URL: https://doi.org/10.1613/jair.1.14924.
  14. Florin Leutwiler and Francesco Corman. A logic-based Benders decomposition for microscopic railway timetable planning. European Journal of Operational Research, 303(2):525-540, December 2022. URL: https://doi.org/10.1016/j.ejor.2022.02.043.
  15. Christian Liebchen and Rolf H. Möhring. The Modeling Power of the Periodic Event Scheduling Problem: Railway Timetables — and Beyond. In Frank Geraets, Leo Kroon, Anita Schoebel, Dorothea Wagner, and Christos D. Zaroliagis, editors, Algorithmic Methods for Railway Optimization, pages 3-40, Berlin, Heidelberg, 2007. Springer. URL: https://doi.org/10.1007/978-3-540-74247-0_1.
  16. Mark H. Liffiton and Jordyn C. Maglalang. A Cardinality Solver: More Expressive Constraints for Free. In Alessandro Cimatti and Roberto Sebastiani, editors, Theory and Applications of Satisfiability Testing — SAT 2012, pages 485-486, Berlin, Heidelberg, 2012. Springer. URL: https://doi.org/10.1007/978-3-642-31612-8_47.
  17. Ruben Martins, Saurabh Joshi, Vasco Manquinho, and Inês Lynce. Incremental Cardinality Constraints for MaxSAT. In Barry O’Sullivan, editor, Principles and Practice of Constraint Programming, pages 531-548, Cham, 2014. Springer International Publishing. URL: https://doi.org/10.1007/978-3-319-10428-7_39.
  18. Gonçalo P. Matos, Luís M. Albino, Ricardo L. Saldanha, and Ernesto M. Morgado. Solving periodic timetabling problems with SAT and machine learning. Public Transport, 13(3):625-648, October 2021. URL: https://doi.org/10.1007/s12469-020-00244-y.
  19. Antonio Morgado, Carmine Dodaro, and Joao Marques-Silva. Core-Guided MaxSAT with Soft Cardinality Constraints. In Barry O’Sullivan, editor, Principles and Practice of Constraint Programming, pages 564-573, Cham, 2014. Springer International Publishing. URL: https://doi.org/10.1007/978-3-319-10428-7_41.
  20. Andreas Niskanen, Jeremias Berg, and Matti Järvisalo. Incremental Maximum Satisfiability. In Kuldeep S. Meel and Ofer Strichman, editors, 25th International Conference on Theory and Applications of Satisfiability Testing (SAT 2022), volume 236 of Leibniz International Proceedings in Informatics (LIPIcs), pages 14:1-14:19, Dagstuhl, Germany, 2022. Schloss Dagstuhl - Leibniz-Zentrum für Informatik. URL: https://doi.org/10.4230/LIPIcs.SAT.2022.14.
  21. P. Serafini and W. Ukovich. A Periodic Job Shop Model. IFAC Proceedings Volumes, 22(14):89-94, September 1989. URL: https://doi.org/10.1016/S1474-6670(17)54331-1.
  22. Xujie Si, Xin Zhang, Vasco Manquinho, Mikoláš Janota, Alexey Ignatiev, and Mayur Naik. On Incremental Core-Guided MaxSAT Solving. In Michel Rueher, editor, Principles and Practice of Constraint Programming, volume 9892, pages 473-482. Springer International Publishing, Cham, 2016. Series Title: Lecture Notes in Computer Science. URL: https://doi.org/10.1007/978-3-319-44953-1_30.
  23. Sander Van Aken, Nikola Bešinović, and Rob M. P. Goverde. Designing alternative railway timetables under infrastructure maintenance possessions. Transportation Research Part B: Methodological, 98:224-238, April 2017. URL: https://doi.org/10.1016/j.trb.2016.12.019.
Any Issues?
X

Feedback on the Current Page

CAPTCHA

Thanks for your feedback!

Feedback submitted to Dagstuhl Publishing

Could not send message

Please try again later or send an E-mail
© 2023-2026 Schloss Dagstuhl – LZI GmbH Schloss Dagstuhl – LZI GmbH About DROPS Imprint Privacy Contact