0
$\begingroup$

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?

$\endgroup$

1 Answer 1

0
$\begingroup$

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.

$\endgroup$
1
  • $\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, 2023 at 23:40

Your Answer

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

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