Railway Scheduling Using Boolean Satisfiability Modulo Simulations

TL;DR

This paper introduces a novel approach to railway scheduling by combining SAT solving with ODE simulations, enabling more flexible and extensible solutions compared to traditional dedicated simulators.

Contribution

It presents a new SAT modulo ODE framework for railway scheduling, integrating discrete and continuous modeling for improved flexibility.

Findings

Solver is competitive with dedicated railway simulators

Method effectively models timing and ordering constraints

Approach is more general and extensible

Abstract

Railway scheduling is a problem that exhibits both non-trivial discrete and continuous behavior. In this paper, we simulate train networks at a low level, where a number of timing and ordering constraints can appear. 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.