Draft:Strong Exponential Time Hypothesis

${\displaystyle k{\text{-}}SAT}$

The k-satisfiability problem (${\displaystyle k{\text{-SAT}}}$) is a restricted version of SAT where the input formula is in conjunctive normal form (CNF) and each clause contains at most ${\displaystyle k}$ literals^[3].

A CNF formula is a conjunction of clauses:

${\displaystyle \varphi =C_{1}\land C_{2}\land \dots \land C_{m}}$,

where each clause ${\displaystyle C_{i}}$ is a disjunction of literals and has the form:

${\displaystyle C_{i}=\ell _{1}^{i}\lor \ell _{2}^{i}\lor \dots \lor \ell _{r_{i}}^{i},\quad r_{i}\leq k}$.^[4]

The goal of ${\displaystyle k{\text{-SAT}}}$ is to determine whether there exists an assignment to the variables that satisfies all clauses. In other words, ${\displaystyle k{\text{-SAT}}}$ returns true if there exists an assignment such that ${\displaystyle \varphi =1}$.

${\displaystyle k{\text{-SAT}}}$ Example

Consider the following ${\displaystyle {\text{k-SAT}}}$ formula where ${\displaystyle k=3}$:

${\displaystyle \varphi =(x_{1}\lor \lnot x_{2}\lor x_{3})\land (\lnot x_{1}\lor x_{2}\lor x_{4})\land (x_{2}\lor \lnot x_{3})}$.

${\displaystyle k{\text{-SAT}}}$ asks whether there exists an assignment to the variables ${\displaystyle x_{1},x_{2},x_{3},x_{4}}$ such that ${\displaystyle \varphi =1}$.

Consider the assignment:

${\displaystyle x_{1}=1,\quad x_{2}=1,\quad x_{3}=0,\quad x_{4}=1}$.

Under this assignment:

• ${\displaystyle (x_{1}\lor \lnot x_{2}\lor x_{3})=(1\lor 0\lor 0)=1}$
• ${\displaystyle (\lnot x_{1}\lor x_{2}\lor x_{4})=(0\lor 1\lor 1)=1}$
• ${\displaystyle (x_{2}\lor \lnot x_{3})=(1\lor 1)=1}$

Since all clauses are satisfied, ${\displaystyle \varphi =1}$. Therefore, the solution to this example is true.

SETH Formal Definition

Let ${\displaystyle k{\text{-}}SAT}$ denote the satisfiability problem for Boolean formulas in conjunctive normal form, containing at most ${\displaystyle k}$ literals per clause. SETH states that ${\displaystyle \lim _{k\to \infty }s_{k}=1}$, where ${\displaystyle s_{k}}$ is the infimum over all real numbers ${\displaystyle c}$ such that ${\displaystyle k{\text{-}}SAT}$ can be solved in ${\displaystyle O(2^{cn})}$ time, where ${\displaystyle n}$ is the number of variables in the formula.

Equivalently, for every ${\displaystyle \epsilon >0}$, there exists some integer ${\displaystyle k\geq 3}$ such that ${\displaystyle k{\text{-}}SAT}$ cannot be solved in ${\displaystyle O(2^{(1-\epsilon )n})}$ time^[1].

Intuition

SETH is a strengthened version of the Exponential Time Hypothesis (ETH). ETH states that ${\displaystyle 3{\text{-}}SAT}$ cannot be solved in sub-exponential time^[4]. However, SETH strengthens this claim by stating that for larger values of ${\displaystyle k}$, ${\displaystyle k{\text{-}}SAT}$ still cannot be solved significantly faster than its brute force solution with a running time proportional to ${\displaystyle 2^{n}}$^[5].

Role in Fine-Grained Complexity

SETH is used throughout fine-grained complexity theory to establish conditional lower bounds for various computational problems. Rather than proving unconditional hardness, many problems show that a significantly faster algorithm for them would imply a faster algorithm for ${\displaystyle k{\text{-}}SAT}$, thereby contradicting SETH^[1]. However, this hardness is conditioned on SETH being true.

These results are usually obtained through reductions from ${\displaystyle k{\text{-}}SAT}$ or related problems such as the Orthogonal Vectors (OV) problem. Thus, SETH provides a framework in fine-grained complexity theory for transferring hardness from satisfiability problems to a wide range of other domains such as string algorithms, graph algorithms, and dynamic data structures^[5].

References