标题： 带满足性模理论的集成周期铁路时刻表求解：一种可扩展的路径和车辆循环方法 显示英文标题

标题： Solving Integrated Periodic Railway Timetabling with Satisfiability Modulo Theories: A Scalable Approach to Routing and Vehicle Circulation

摘要： 本文介绍了一种新的方法，通过统一的优化模型联合求解周期性列车时刻表问题（TTP）、列车径路选择和车辆循环问题（VCP）。虽然这些规划阶段传统上是依次处理的，但它们之间的相互依赖性常常导致车辆使用效率不高。我们提出了VCR-PESP，这是一种集成公式，在确保可行且符合基础设施要求的周期性时刻表的同时，最小化车队规模。我们提出了第一个基于满足性模理论（SMT）的方法来解决VCR-PESP，以求解大规模实例。与需要时间离散化的布尔满足性问题（SAT）不同，SMT通过差分约束支持连续时间，消除了时间精度与编码大小之间的权衡。我们的方法避免了四舍五入伪影，并能有效扩展，在非平凡实例中优于SAT和混合整数规划（MIP）模型。使用瑞士窄轨运营商RhB的真实数据，我们进行了广泛的实验，评估时间离散化、车辆循环策略、路径灵活性和规划集成的影响。我们证明了离散模型会增加车辆需求，而完全集成的解决方案相比顺序方法显著减少了车队需求。我们的框架在大型复杂网络中始终能够提供高分辨率的解决方案，运行时间可控。通过将建模准确性与可扩展的求解器技术相结合，这项工作确立了SMT作为集成铁路规划的强大工具。它展示了如何放松离散化并在规划层面上求解，从而实现更高效且可实施的时刻表。 显示英文摘要

摘要： This paper introduces a novel approach for jointly solving the periodic Train Timetabling Problem (TTP), train routing, and Vehicle Circulation Problem (VCP) through a unified optimization model. While these planning stages are traditionally addressed sequentially, their interdependencies often lead to suboptimal vehicle usage. We propose the VCR-PESP, an integrated formulation that minimizes fleet size while ensuring feasible and infrastructure-compliant periodic timetables. We present the first Satisfiability Modulo Theories (SMT)-based method for the VCR-PESP to solve the resulting large-scale instances. Unlike the Boolean Satisfiability Problem (SAT), which requires time discretisation, SMT supports continuous time via difference constraints, eliminating the trade-off between temporal precision and encoding size. Our approach avoids rounding artifacts and scales effectively, outperforming both SAT and Mixed Integer Program (MIP) models across non-trivial instances. Using real-world data from the Swiss narrow-gauge operator RhB, we conduct extensive experiments to assess the impact of time discretisation, vehicle circulation strategies, route flexibility, and planning integration. We show that discrete models inflate vehicle requirements and that fully integrated solutions substantially reduce fleet needs compared to sequential approaches. Our framework consistently delivers high-resolution solutions with tractable runtimes, even in large and complex networks. By combining modeling accuracy with scalable solver technology, this work establishes SMT as a powerful tool for integrated railway planning. It demonstrates how relaxing discretisation and solving across planning layers enables more efficient and implementable timetables.