"Strong ETH Holds for Regular Resolution"
Chris Beck
Princeton University
Thursday, August 1st, 2013, 11:00 am
EBU3B, Room 4217
Abstract:
Let $c_k$ be the smallest number so that $k$-SAT is solvable in time $2^{c_k n} poly(n)$. The Strong Exponential Time Hypotheis is that the limit of the sequence $c_k$ is $1$, i.e., that the
difficulty of $k$-SAT approaches exhaustive search as $k$ increases. This is true for the best algorithms currently known for $k$-SAT, as well as an empirical observation about the performance of SAT solvers on instances with large clauses.
Since many SAT solvers are based on the resolution proof system, lower bounds for this system give lower bounds for large families of such solvers. We show that no algorithm formalizable in the subsystem of regular resolution can be a counter-example to SETH. More precisely, we show that there are unsatisfiable $k$-CNF formulas on $n$ variables so that any regular resolution refutation requires size $2^{1-\epsilon_k}n$, where $\epsilon_k = \tilde{O} (k^{1/4})$. We also improve the lower bounds for general resolution substantially, showing that the same formulas require general resolution size at least $(3/2)^{(1-\epsilon_k)n}$.
Joint work with Russell Impagliazzo (UCSD).