The Library
Subcubic certificates for CFL reachability
Tools
Chistikov, Dmitry, Majumdar, Rupak and Schepper, Philipp (2022) Subcubic certificates for CFL reachability. In: ACM SIGPLAN Symposium on Principles of Programming Languages (POPL 2022), Philadelphia, Pennsylvania, United States, 16-22 Jan 2022. Published in: Proceedings of the ACM on Programming Languages, 6 (POPL). doi:10.1145/3498702 ISSN 2475-1421.
|
PDF
WRAP-Subcubic-certificates-CFL-reachability-2021.pdf - Published Version - Requires a PDF viewer. Available under License Creative Commons Attribution 4.0. Download (420Kb) | Preview |
Official URL: https://doi.org/10.1145/3498702
Abstract
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(n2) 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.
Item Type: | Conference Item (Paper) | |||||||||||||||
---|---|---|---|---|---|---|---|---|---|---|---|---|---|---|---|---|
Subjects: | Q Science > QA Mathematics > QA76 Electronic computers. Computer science. Computer software | |||||||||||||||
Divisions: | Faculty of Science, Engineering and Medicine > Science > Computer Science | |||||||||||||||
Library of Congress Subject Headings (LCSH): | Machine theory, Computer algorithms, Formal languages | |||||||||||||||
Journal or Publication Title: | Proceedings of the ACM on Programming Languages | |||||||||||||||
Publisher: | ACM | |||||||||||||||
ISSN: | 2475-1421 | |||||||||||||||
Official Date: | 12 January 2022 | |||||||||||||||
Dates: |
|
|||||||||||||||
Volume: | 6 | |||||||||||||||
Number: | POPL | |||||||||||||||
Article Number: | 41 | |||||||||||||||
DOI: | 10.1145/3498702 | |||||||||||||||
Status: | Peer Reviewed | |||||||||||||||
Publication Status: | Published | |||||||||||||||
Access rights to Published version: | Open Access (Creative Commons) | |||||||||||||||
Date of first compliant deposit: | 8 November 2021 | |||||||||||||||
Date of first compliant Open Access: | 31 January 2022 | |||||||||||||||
RIOXX Funder/Project Grant: |
|
|||||||||||||||
Conference Paper Type: | Paper | |||||||||||||||
Title of Event: | ACM SIGPLAN Symposium on Principles of Programming Languages (POPL 2022) | |||||||||||||||
Type of Event: | Other | |||||||||||||||
Location of Event: | Philadelphia, Pennsylvania, United States | |||||||||||||||
Date(s) of Event: | 16-22 Jan 2022 | |||||||||||||||
Related URLs: |
Request changes or add full text files to a record
Repository staff actions (login required)
View Item |
Downloads
Downloads per month over past year