基于满足模论的集成周期性铁路时刻表求解：铁路 routing 与车辆循环的可扩展方法

本文提出了一种用于联合求解周期性火车时刻表问题（TTP）、火车routing与车辆循环问题（VCP）的新方法。虽然这些规划阶段传统上按顺序解决，但它们的相互依赖性常导致车辆使用效率不佳。我们提出了VCR-PESP（Vehicle Circulation and Routing for Periodic Timetables）集成模型，旨在最小化编制周期时刻表所需的车队规模，同时确保时刻表可行且符合基础设施要求。我们提出了首个基于满足模论（SMT）的方法来求解VCR-PESP，从而解决大规模实例。与布尔满足问题（SAT）不同，SMT支持连续时间通过差分约束，消除了时间离散化与编码规模之间的权衡。我们的做法避免了四舍五入误差，并在实际规模的实例中表现出优异的扩展性，优于SAT和混合整数规划（MIP）模型。我们使用来自瑞士窄轨车队运营商RhB的真实数据进行大量实验，以评估时间离散化、车辆循环策略、路由灵活性和规划集成的影响。我们表明，离散模型会膨胀车辆需求，完全集成的解决方案比顺序方法显著减少车队需求。我们的框架始终能够以可控的运行时间提供高分辨率解决方案，即使在大型复杂网络中也是如此。通过结合建模精度与可扩展求解器技术，本工作将SMT确立为铁路规划中强大的工具。它展示了如何通过放宽离散化并跨规划层面求解，从而实现更高效、更可操作的时刻表。