3
$\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$
3
$\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.

| cite | improve this answer | |
$\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 '19 at 15:09
  • $\begingroup$ Hi! Could you please explain why is it true that for any SAT formula there is an algorithm that finds it easy? Or at least could you point me to some literature on this? Thank you. $\endgroup$ – Алексей Уваров Jul 20 at 8:51
  • 1
    $\begingroup$ @АлексейУваров I am thinking of an algorithm that contains a hardcoded solution to the particular SAT formula and just outputs it (after checking that the input is equal to the preprogrammed formula). The point is that you can never hope to construct a single example formula that is hard to solve for all algorithms. $\endgroup$ – Tom van der Zanden Jul 21 at 6:31

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.