Railway Scheduling Using Boolean Satisfiability Modulo Simulations

Authors: T. Kolárik, Stefan Ratschan
Publication year: 2023
Publication type: Konferenční příspěvek (mezinárodní konf.)
Periodical: Formal Methods: 25th International Symposium, FM 2023, Lübeck, Germany, March 6–10, 2023, Proceedings
Projects: Quasi-Decision Procedures for First-Order Theories of Real Functions
Bibliographic citation: KOLÁRIK, T., RATSCHAN, Stefan. Railway Scheduling Using Boolean Satisfiability Modulo Simulations. In: CHECHIK, M., KATOEN, J.-P., LEUCKER, M., eds. Formal Methods: 25th International Symposium, FM 2023, Lübeck, Germany, March 6–10, 2023, Proceedings. Cham: Springer, 2023, S. 56-73. Lecture Notes in Computer Science, 14000. ISBN 978-3-031-27480-0. ISSN 0302-9743
Dostupné z: doi:10.1007/978-3-031-27481-7_5.
DOI: 10.1007/978-3-031-27481-7_5
ID: 570721
Online record: View online record

Abstract

Railway scheduling is a problem that exhibits both non-trivial discrete and continuous behavior. In this paper, we model this problem using a combination of SAT and ordinary differential equations (SAT modulo ODE). In addition, we adapt our existing method for solving such problems in such a way that the resulting solver is competitive with methods based on dedicated railway simulators while being more general and extensible.