RW-Solver  (RailWay-Solver)
AIST and JR-East

RW-Solver is a tool for generating train timetables with the help of SMT-Solver.

1. Introduction

RW-Solver is a formal tool for generating train timetables with the help of SMT-Solver, in a mesoscopic level that is more concrete than the macroscopic level, where each station is simply expressed in a black-box, and more abstract than the microscopic level, where the infrastructure in each station-area is expressed in detail. The accuracy of generated timetable and the computational effort for the generation is a trade-off.

About the accuracy of railway models, the following three levels are often discussed:

Fig.1  Micro-, meso-, and macroscopic models of a station

About the strategy for solving constraints, there are the following two classes of methods:
RW-Solver is an implementation of an exact solution-method for automatically generating train timetables in a mesoscopic level. Fig.2 shows the overview of the generation of timetables by RW-Solver. RW-Solver generates constraint formulae from given mesoscopic railway models, and submits the constraint formulae to SMT-Solver, and takes the results from STM-Solver, and then generates graphical files (PDF) of the timetables.

Fig.2  The overview of the generation of timetables by RW-Solver

2. License
3. Download
4. Example
5. Publication
6. Contact

Yoshinao Isobe
Cyber Physical Security Research Center
National Institute of Advanced Industrial Science and Technology (AIST), Japan

Last modified: 7 February 2019

(since 07/02/2019)