Is it an open problem if CDCL algorithms violate SETH?

Question

Strong Exponential Time Hypothesis states that general SAT, where clauses are not limited in length, can't be solved in time $o(2^n)$. It's proven that DPLL algorithm requires $\Omega(2^n)$ time in the worst case.

CDCL algorithms, however, use more sophisticated approaches to SAT solving, primarily by using partial assignments and skipping the ones that obviously lead to unsatisfiability, such as setting all variables in a particular clause to make the clause equal to 0ドル$.

In order to violate SETH it would suffice to show that 3-SAT is solvable in $o(\sqrt[3]{2^n})$ time. Is it known if CDCL in the worst case would require more time than this?

Answer 1

No, it doesn't imply that there will be $\Omega(n)$ clauses of length $\le k$. Satisfiability of 100-CNF formulas (where all clauses have exactly 100 literals) is still NP-hard, even though there are 0 clauses of length $\le 99$.

Also, you have not accurately stated the strong exponential time hypothesis.

• rus9384: I suppose the class of formulas eligible for SETH needs to be $NP$-hard and formulas with exponentially many clauses don't belong there. Although, if that's not in the formulation of SETH, perhaps it is not even meaningful.