The logic-constrained shortest path problem (LCSPP) combines a one-to-one shortest path problem with satisfiability constraints imposed on the routing graph. This setting arises in flight planning, where air traffic control (ATC) authorities are enforcing a set of traffic flow restrictions (TFRs) on aircraft routes in order to increase safety and throughput. We propose a new branch and bound-based algorithm for the LCSPP. The resulting algorithm has three main degrees of freedom: the node selection rule, the branching rule and the conflict. While node selection and branching rules have been long studied in the MIP and SAT communities, most of them cannot be applied out of the box for the LCSPP. We review the existing literature and develop tailored variants of the most prominent rules. The conflict, the set of variables to which the branching rule is applied, is unique to the LCSPP. We analyze its theoretical impact on the B&B algorithm. In the second part of the paper, we show how to model the flight planning problem with TFRs as an LCSPP and solve it using the branch and bound algorithm. We demonstrate the algorithm's efficiency on a dataset consisting of a global flight graph and a set of around 20000 real TFRs obtained from our industry partner Lufthansa Systems GmbH. We make this dataset publicly available. Finally, we conduct an empirical in-depth analysis of dynamic shortest path algorithms, node selection rules, branching rules and conflicts. Carefully choosing an appropriate combination yields an improvement of an order of magnitude compared to an uninformed choice.

翻译：逻辑约束最短路径问题（LCSPP）将一对一最短路径问题与施加于路由图的可满足性约束相结合。该问题场景出现在航班规划中，空中交通管制（ATC）当局为提升安全性与吞吐量，对飞机航线实施一系列交通流量限制措施（TFRs）。我们针对LCSPP提出一种新的基于分支定界的算法。该算法具有三个主要自由度：节点选择规则、分支规则及冲突集。虽然节点选择与分支规则已在MIP和SAT领域得到长期研究，但多数规则无法直接应用于LCSPP。我们回顾现有文献，并为最主流规则开发定制化变体。冲突集——即分支规则所应用的变量集合——是LCSPP所独有的特性。我们从理论层面分析其对分支定界（B&B）算法的影响。在论文第二部分，我们展示如何将带有TFRs的航班规划问题建模为LCSPP，并运用分支定界算法求解。我们在包含全球航班图及来自行业合作伙伴汉莎系统公司（Lufthansa Systems GmbH）约20000个真实TFRs的数据集上验证了算法效率，并将该数据集公开共享。最后，我们对动态最短路径算法、节点选择规则、分支规则及冲突集进行深入实证分析。精心选择适当组合相较于未经优化的选择可提升一个数量级的性能。