用于CFL可达性的次立方证书
Subcubic Certificates for CFL Reachability
摘要：
过程间程序分析中的许多问题可以建模为图上的上下文无关语言（CFL）可达性问题，并可以在立方时间内求解。尽管多年的努力，有没有真正的子立方算法为这个问题。我们研究相关的认证任务：CFL的可达性的一个实例，是否有小的和有效的可检查的证书的存在和不存在的路径？我们表明，在这两种情况下，存在简洁的证书（$O(n^2)$在问题的大小），这些证书可以在次立方（矩阵乘法）时间检查。证书基于基于路径的基于语法的压缩（对于正实例）和表示为矩阵约束的不变量（对于负实例）。因此，CFL的可达性在于不确定和共不确定的亚立方时间。一个自然的问题是CFL可达性的更快算法是否会导致布尔可满足性（SAT）等组合问题的更快算法。作为我们的认证结果的结果，我们表明，不能有一个细粒度的减少从SAT到CFL的可达性的条件下限强于$n^ω$，除非非确定性强指数时间假设（NSETH）失败。我们的研究结果扩展到相关的次立方等价问题：下推可达性和双向非确定性下推自动机（2NPDA）的语言识别。例如，我们描述了下推不可达性（归纳不变量）的简洁证书，并观察到它们可以在矩阵乘法时间内进行检查。我们还提取了一个新的最难的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 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^ω$, 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.
机构、总结、中文摘要均由AI分析而来，可能存在错误，请以论文正文为准。
