CISPA
Browse
cispa_all_3576.pdf (420.17 kB)

Subcubic certificates for CFL reachability

Download (420.17 kB)
conference contribution
posted on 2023-11-29, 18:19 authored by Dmitry Chistikov, Rupak Majumdar, Philipp SchepperPhilipp Schepper
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.

History

Preferred Citation

Dmitry Chistikov, Rupak Majumdar and Philipp Schepper. Subcubic certificates for CFL reachability. In: Symposium on Principles of Programming Languages (POPL). 2022.

Primary Research Area

  • Algorithmic Foundations and Cryptography

Name of Conference

Symposium on Principles of Programming Languages (POPL)

Legacy Posted Date

2022-02-24

Open Access Type

  • Gold

BibTeX

@inproceedings{cispa_all_3576, title = "Subcubic certificates for CFL reachability", author = "Chistikov, Dmitry and Majumdar, Rupak and Schepper, Philipp", booktitle="{Symposium on Principles of Programming Languages (POPL)}", year="2022", }

Usage metrics

    Categories

    No categories selected

    Licence

    Exports

    RefWorks
    BibTeX
    Ref. manager
    Endnote
    DataCite
    NLM
    DC