# Is it an open problem if CDCL algorithms violate SETH?

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

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.

• 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. Jul 8 at 23:40