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$.
This means that on a $k$-clause the algorithm will only try $2^k-1$ out of $2^k$ partial assignments, and given that hard formulas have $\Omega(n)$ clauses*, there will be $\Omega(n)$ clauses of length $\le k$ for some $k<\log n$. Which implies that a fraction of $\Omega\Big(\big(\frac{2^k-1}{2^k}\big)^{\Omega(n)}\Big)$ of all assignments will be skipped. Potentially even more because every meaningful partial assignment shortens some clauses, except when all clauses evaluate to $1$ without assigning remaining variables.
Does that not violate SETH? And in general are there known worst case lower bounds for CDCL? Such algorithms as WalkSAT and PPSZ are known to not violate it.
*Complexity classes are defined on input sizes and SETH is defined using complexity classes.
