The Logic-Constrained Shortest Path Problem (LCSP) 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 LCSP. 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 LCSP. 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 LCSP. 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 LCSP 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 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.

翻译：逻辑约束最短路径问题（LCSP）将一对一最短路径问题与施加在路由图上的可满足性约束相结合。该场景出现在飞行规划中，空中交通管制（ATC）机构为提升安全性与通行能力，对航空器航路实施一系列交通流限制（TFR）。本文提出一种新的基于分支定界法的LCSP求解算法。该算法包含三个主要可调节维度：节点选择规则、分支规则与冲突集。尽管混合整数规划（MIP）与可满足性（SAT）研究领域对节点选择与分支规则已有长期探索，但其中多数规则无法直接适用于LCSP。本文系统回顾现有文献，并针对最具代表性的规则开发定制化变体。冲突集——即分支规则所作用的变量集合——是LCSP特有的设计要素，我们深入分析了其对分支定界算法的理论影响。在论文第二部分，我们展示了如何将含TFR的飞行规划问题建模为LCSP，并运用分支定界算法进行求解。通过基于全球飞行图及约20000条来自行业合作伙伴汉莎航空系统有限公司的真实TFR数据集进行测试，验证了算法的高效性。该数据集已公开。最后，我们对节点选择规则、分支规则及冲突集进行了深入的实证分析。实验表明，相较于无指导的随机选择，精心配置三者的组合策略可实现算法性能的数量级提升。