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 positive instances) and on invariants represented as matrix constraints (for negative instances). 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^\omega$, unless the nondeterministic strong exponential time hypothesis (NSETH) fails. Our results extend to related subcubic equivalent problems: pushdown reachability and two-way nondeterministic pushdown automata (2NPDA) language recognition. 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.
翻译:程序间程序分析中的许多问题可以建模为图表上不上下文语言( CFL) 的可达性问题, 并且可以在立方时间里解决。 尽管多年的努力, 这个问题并不存在已知的真正的亚立方算法。 我们研究相关的认证任务: 鉴于 CFL 的可达性, 是否有小且高效的可核实证书来证明路径的存在和不存在? 我们显示, 在两种情况下, 都有简洁的证书( 问题大小中为O (n2) 美元), 这些证书可以在亚立方( 矩阵倍增) 时间里检查 。 这些证书是以基于语法的路径压缩( 正面实例) 为基础, 并且基于内立方( 负立方) 限制。 因此, CFLC 的可达性取决于非定性和非定时性 。 自然的问题是, CFLFL 的可快速的可达标值能导致对像 Boolean 的可达度问题进行更快的算法的快速的可达性分析( SAT) 。 由于不易达性( 的不可达) 的不可达性, 我们的不可变化的硬性, 我们无法判断性地解的不可变化的递增化的解的结果。