Satisfiability Checking for Optimization of Timetables in Railway


Rebecca Haehn


+49 241 80 21243



In many application areas of logic in computer science the aspect of uncertainty plays an increasingly important role. For example in planning in the railway industry the travel times of trains in shortest-path problems do not only depend on the distance, but also on external influences like weather conditions and traffic of other network users. An additional uncertainty results from unreliable railway networks, some of the edges, for example, tracks, might even fail completely, for example due to construction work. Especially for long forecast periods the models of railway traffic include various uncertainties.

Despite the uncertainty in the available data long-term decisions on the design of railway networks, train-schedules, and construction periods have to be made. These decisions are required to be robust that is to deliver almost optimal solutions even for uncertain input data or at least allow for efficient re-scheduling and re-routing. Inconveniently even small changes in the input data can lead to arbitrarily bad and even infeasible solutions.

The aim of this project is to create an efficient system that can cope with uncertainty in railway traffic while making reliable statements about the network capacity. In conventional models of railway networks capacities are determined for individual infrastructure elements. This does neither answer how much additional traffic the infrastructure can handle in the future nor which railway expansion projects are the most useful. These questions were dealt with before by Christian Meirich in his dissertation project. His approach, however, does not take uncertainty into account, which leaves room for further investigations.

The main objectives of this dissertation project in order to estimate railway network capacities under consideration of uncertainties are:

  • Mathematically model railway systems under consideration of random events.
  • Develop a mathematical formulation of the problem to optimize train schedules using the models mentioned above.
  • Solve this optimization problem using linear programming and / or SMT solving.
  • Examining the impact of the problem formulation on the running times of the optimization.