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:
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
2. License
Following the ideas of open source software, we allow anyone to use RW-Solver without fee, under the GNU General Public License version 3 (GPL v3). You have to agree with the license before using RW-Solver.
3. 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)
