2
$\begingroup$

The $3-SAT$ problem is known to be NP-complete problem. Which means that (as far as I understand), unless $P \neq NP$, for every algorithm $A$ which decides $3-SAT$, $A$ runs in super polynomial time (I know that this is not well defined). A stronger assumption is the "Strong Exponential Time Hypothesis " which states that every algorithm has to run in worst case exponential time.
Does that mean, for example, that every algorithm $A$ (here I refer to a "real" or practical implementation, such as Glucoses, DPLL, Z3, etc.), has an instance of size, say 200, which $A$ will not be able to solve in a reasonable time? I see many sat solvers solving formulas with millions of variables in very short time; and I am aware of subsets of $3-SAT$ which are easy, such as Horn clauses, or a random instance with a known density - but it seems that these solvers work amazingly fast without any assumptions on the input.
I have searched for Sat benchmarks, or instances which should be hard, but when running them on a modern sat solver, it doesn't seem to be a problem.
It is known that complexity assumptions (or claims) are about the asymptotic behavior, my question is: do we know for which $n_0$ these assumptions "kick in" in the case of $3-SAT$? Can we generate, or at least be confident of the existence of a relatively small formula ($< 200$), such that every algorithm requires $\sim2^{200}$ operations?

$\endgroup$
2
$\begingroup$

do we know for which $n_0$ these assumptions "kick in" in the case of $3-SAT$? Can we generate, or at least be confident of the existence of a relatively small formula ($< 200$), such that every algorithm requires $\sim2^{200}$ operations?

$3-SAT$ is known to be solvable in time $O(1.321^n)$. Therefore, there is no instance that would force a $\Omega(2^n)$ run time. SETH does not hold for $k-SAT$ for any bounded $k$; it is only expected to hold for general Satsifiability (with no limit on clause size). We don't really know what asymptotic runtime to expect for $k$-SAT for any $k$ (other than something exponential).

Also, for any $SAT$ formula, there is an algorithm solving it in $O(n)$ time. You could never hope to find a single example hard for all algorithms.

One way to generate hard SAT instances is to reduce from Integer Factorization.

$\endgroup$
  • $\begingroup$ Thanks. I didn't expect for a single instance which will be hard on all algorithms, but given an algorithm, how can I find its hard instances. The question came since every modern SAT solver that I tried seemed to work very fast (obviously, I can only try a tiny fraction of the space), so I am trying to understand where the "exponential barrier" in practice. About int factorization - it is not known this problem is NPC, so why would that way makes hard instances? $\endgroup$ – Jonathan Oct 10 at 15:09

Your Answer

By clicking “Post Your Answer”, you agree to our terms of service, privacy policy and cookie policy

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