一句话：证明 CFL 可达性存在 O(n^2) 大小的存在性与非存在性证书，并可在次三次时间内验证。
CFL 可达性可刻画大量过程间程序分析问题，已知有三次时间算法，但无真正次三次算法。本文研究其证书问题：给定实例，能否为路径存在与不存在提供简短易验证的证明？作者证明两类证书都只需 O(n^2) 大小，并可在次三次（矩阵乘法）时间内检查：可达性证书基于路径的文法压缩，不可达性证书基于矩阵不等式表示的不变式。由此 CFL 可达性属于非确定性与余非确定性次三次时间。该结果还推出，除非 NSETH 失败，SAT 的细粒度归约无法给出强于 n^ω 的条件下界；并扩展到下推可达性、2NPDA 识别与全对 CFL 可达性，提取出一个新的最难 2NPDA 语言。
Many problems in interprocedural program analysis can be modeled as the context-free language (CFL) reachability problem on graphs and can be solved in cubic time. Despite years of efforts, there are no known truly sub-cubic algorithms for this problem. We study the related certification task: given an instance of CFL reachability, are there small and efficiently checkable certificates for the existence and for the non-existence of a path? We show that, in both scenarios, there exist succinct certificates ( O ( n 2 ) in the size of the problem) and these certificates can be checked in subcubic (matrix multiplication) time. The certificates are based on grammar-based compression of paths (for reachability) and on invariants represented as matrix inequalities (for non-reachability). Thus, CFL reachability lies in nondeterministic and co-nondeterministic subcubic time. A natural question is whether faster algorithms for CFL reachability will lead to faster algorithms for combinatorial problems such as Boolean satisfiability (SAT). As a consequence of our certification results, we show that there cannot be a fine-grained reduction from SAT to CFL reachability for a conditional lower bound stronger than n ω , unless the nondeterministic strong exponential time hypothesis (NSETH) fails. In a nutshell, reductions from SAT are unlikely to explain the cubic bottleneck for CFL reachability. Our results extend to related subcubic equivalent problems: pushdown reachability and 2NPDA recognition; as well as to all-pairs CFL reachability. For example, we describe succinct certificates for pushdown non-reachability (inductive invariants) and observe that they can be checked in matrix multiplication time. We also extract a new hardest 2NPDA language, capturing the “hard core” of all these problems.
@article{paperbot1583,
title = {Subcubic certificates for CFL reachability},
author = {Dmitry Chistikov and Rupak Majumdar and Philipp Schepper},
journal = {Proceedings of the ACM on Programming Languages},
volume = {6},
number = {POPL},
year = {2022},
doi = {10.1145/3498702}
}