# Practical hard 3-sat instances

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?

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.

• 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? Commented Oct 10, 2019 at 15:09
• 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. Commented Jul 20, 2020 at 8:51
• @АлексейУваров 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. Commented Jul 21, 2020 at 6:31

you could have a look at at Zero-One Designs Produce Small Hard SAT Instances

The instances are generated drawing from combinatorial block design and yield instances of up to 100 variables that were hard for solvers at the time of the paper's publicaton.
Unfortunately I'm not familiar with the topic and thus can't provide more information.

A generator for these instances can be found here.
And here is a generator for integer factoring instances.

• Can you please include at least one point from the paper hyperlinked in your answer? From help→How do I write a Good Answer?: Always quote the most relevant part of an important link Commented Jun 23 at 6:00