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.


1 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.

  • $\begingroup$ 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. $\endgroup$
    – rus9384
    Jul 8 at 23:40

Your Answer

By clicking “Post Your Answer”, you agree to our terms of service and acknowledge that you have read and understand our privacy policy and code of conduct.

Not the answer you're looking for? Browse other questions tagged or ask your own question.