Railway scheduling using Boolean satisfiability modulo simulations

DOI10.1007/978-3-031-27481-7_5MaRDI QIDQ6174526zbMATH OpenFDO

Authors Tomáš Kolárik, Stefan Ratschan

Publication date 17 August 2023

Published in Formal Methods (Search for Journal in Brave)

Full work available at URL https://arxiv.org/abs/2212.05382

Mathematics Subject Classification ID

Problem solving in the context of artificial intelligence (heuristics, search strategies, etc.) (68T20) Theorem proving (automated and interactive theorem provers, deduction, resolution, etc.) (68V15) Deterministic scheduling theory in operations research (90B35)

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.

Recommendations

• A branch and bound algorithm for scheduling trains in a railway network
• Railway scheduling by network optimization
• scientific article; zbMATH DE number 5343210
• NETWORK-BASED SIMULATION APPROACH FOR SCHEDULING TRAINS ON RAIL NETWORKS
• Modeling and Solving the Train Timetabling Problem
• Railway scheduling problems and their decomposition.
• Fast approaches to robust railway timetabling
• Railway timetabling using Lagrangian relaxation
• Models and algorithms for combinatorial optimization problems arising in railway applications

Cites work

• A novel approach to strategic planning of rail freight transport
• A survey on continuous time computations
• dReal: an SMT solver for nonlinear theories over the reals
• Improving SAT modulo ODE for hybrid systems analysis by combining different enclosure methods
• Multi-agent pathfinding with continuous time
• Optimizing the simplon railway corridor
• SAT Modulo Differential Equation Simulations
• Solving SAT and SAT modulo theories, from an abstract Davis-Putnam-Logemann-Loveland procedure to \(\operatorname{DPLL}(T)\)

Cited in

(3)

• Approaches to modeling train scheduling problems as job-shop problems with blocking constraints
• An efficient computational approach for railway booking problems
• scientific article; zbMATH DE number 5343212 (Why is no real title available?)

This page was built for publication: Railway scheduling using Boolean satisfiability modulo simulations

Report a bug (only for logged in users!)Click here to report a bug for this page (MaRDI item Q6174526)