RW-Solvers

AIST and JR-East
last updated 2023.08.03
[ Isobe > RW-Solver ]
RW-Solver  (RailWay-Solver)
AIST and JR-East

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


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:
  • In the microscopic level, models can express the details of the railway networks and the platforms in each station area as shown in Fig.1(a).  In this level, train timetables are often improved by simulations.
  • In the macroscopic level, models usually represent each station as a black-box as shown in Fig.1(c), and schedules in the models consist of departure and arrival times at the black-box.
  • Mesoscopic levels are more concrete than the macroscopic level and more abstract than the microscopic level. For example, in a mesoscopic level models can express available platforms for each direction in each station area as shown in Fig.1(b) and it is still possible to automatically generate timetable even if it is difficult in the microscopic level.



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


About the strategy for solving constraints, there are the following two classes of methods:
  • Exact solution method: Constraint solvers such as SAT-Solver are used for checking whether a timetable to satisfy the given set of constraints exists or not.  Such a problem is known to be NP-complete.
  • Heuristic solution method: Some heuristic approaches such as genetic algorithm and greedy procedure have been applied for heuristically generating timetables to satisfy the given set of constraints in reasonable computational time.
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


License

Download
  • The OCaml source files of RW-Solver can be download from this GitHub site.
    • AIST Program-IP No. H30PRO-2219
    • National Institute of Advanced Industrial Science and Technology (AIST) and
      East Japan Railway Company (JR-East)
  • The manual for RW-Solver [English PDF (32KB), Japanese PDF (81KB)]
Example
Publication
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)