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