Simple Reductions from Formula-SAT to Pattern Matching on Labeled Graphs and Subtree Isomorphism

TL;DR

This paper presents simplified, tight reductions from the Formula-SAT problem to pattern matching on labeled graphs and subtree isomorphism, strengthening the basis for SETH-based lower bounds in these problems.

Contribution

It introduces simpler, tight reductions from Formula-SAT to PMLG and subtree isomorphism, expanding the scope of SETH-based hardness results beyond sequence alignment problems.

Findings

Reductions are tight and simpler than previous ones.

Results support SETH-based lower bounds for PMLG and subtree isomorphism.

Enhances understanding of reductions from Formula-SAT to graph problems.

Abstract

The CNF formula satisfiability problem (CNF-SAT) has been reduced to many fundamental problems in P to prove tight lower bounds under the Strong Exponential Time Hypothesis (SETH). Recently, the works of Abboud, Hansen, Vassilevska W. and Williams (STOC 16), and later, Abboud and Bringmann (ICALP 18) have proposed basing lower bounds on the hardness of general boolean formula satisfiability (Formula-SAT). Reductions from Formula-SAT have two advantages over the usual reductions from CNF-SAT: (1) conjectures on the hardness of Formula-SAT are arguably much more plausible than those of CNF-SAT, and (2) these reductions give consequences even for logarithmic improvements in a problems upper bounds. Here we give tight reductions from Formula-SAT to two more problems: pattern matching on labeled graphs (PMLG) and subtree isomorphism. Previous reductions from Formula-SAT were to sequence alignment problems such as Edit Distance, LCS, and Frechet Distance and required some technical work. This paper uses ideas similar to those used previously, but in a decidedly simpler setting, helping to illustrate the most salient features of the underlying techniques.