The (Coarse) Fine-Grained Structure of NP-Hard SAT and CSP Problems

We study the fine-grained complexity of NP-complete satisfiability (SAT) problems and constraint satisfaction problems (CSPs) in the context of the strong exponential-time hypothesis (SETH), showing non-trivial lower and upper bounds on the running time. Here, by a non-trivial lower bound for a problem SAT(Gamma) (respectively CSP(Gamma)) with constraint language F, we mean a value c(0) > 1 such that the problem cannot be solved in time O(c(n)) for any c < c(0) unless SETH is false, while a non-trivial upper bound is simply an algorithm for the problem running in time O(c(n)) for some c < 2. Such lower bounds have proven extremely elusive, and except for cases where c(0) = 2 effectively no such previous bound was known. We achieve this by employing an algebraic framework, studying constraint languages r in terms of their algebraic properties. We uncover a powerful algebraic framework where a mild restriction on the allowed constraints offers a concise algebraic characterization. On the relational side we restrict ourselves to Boolean languages closed under variable negation and partial assignment, called sign-symmetric languages. On the algebraic side this results in a description via partial operations arising from system of identities, with a close connection to operations resulting in tractable CSPs, such as near unanimity operations and edge operations. Using this connection we construct improved algorithms for several interesting classes of sign-symmetric languages, and prove explicit lower bounds under SETH. Thus, we find the first example of an NP-complete SAT problem with a non-trivial algorithm which also admits a non-trivial lower bound under SETH. This suggests a dichotomy conjecture with a close connection to the CSP dichotomy theorem: an NP-complete SAT problem admits an improved algorithm if and only if it admits a non-trivial partial invariant of the above form.Funding Agencies|Swedish resourch council (VR) [2019-03690]