Résumé | The context-free language (CFL) reachability problem on graphs, as well as
a closely related problem of language emptiness for pushdown automata, are
core problems in interprocedural program analysis and model checking,
respectively. Both can be solved in cubic time but, despite years of
efforts, there are no truly sub-cubic algorithms known for either.
We study the related certification task: given a problem instance, are
there small and efficiently checkable certificates for the existence and
for the non-existence of a path (or language non-emptiness and emptiness,
respectively)? 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.
A natural question is whether faster algorithms for CFL reachability or
PDA emptiness will lead to faster algorithms for other combinatorial
problems such as SAT. As a consequence of our certification results, we
show that there cannot be a fine-grained reduction from SAT to CFL
reachability or PDA emptiness for a conditional lower bound stronger than
$n^omega$, unless the nondeterministic strong exponential-time hypothesis
(NSETH) fails.
This is joint work with Rupak Majumdar and Philipp Schepper.
A preprint is available at https://arxiv.org/abs/2102.13095 .
Enregistrement : https://u-bordeaux-fr.zoom.us/rec/share/kcrUh-SsH97onePRKAyCrw_B2H7Y2iVQAbGVLdumtgI_0-ZMCnxflRjbBeVv5iCH.Qzri0hDgia6JjQnU |