How hard is random SAT?

Question

There is plenty of research into the so-called "random SAT" problem, where we basically try to solve SAT instances with clauses chosen "at random" in some sense.

There are all kinds of variations of this problem, mostly referring to how the clauses are chosen. Typically you see it written as the random "$k$-SAT" problem, where the clauses have $k$ variables, and where we can also vary the total number of variables and the total number of clauses we will have. We can also look at different probability spaces the clauses are drawn from (is it uniformly at random or something else?).

My big-picture question is, in general, how computationally difficult it is to solve these "random" instances, given some common choices of these parameters. I would be happy to know even just for uniformly at random 3-SAT w/ $n$ variables and $m$ clauses. I have read that many "real-world" industrial SAT instances are much harder to solve than these "random" ones, indicating that perhaps the random-SAT problem is easier than the general SAT problem. There also seem to be various algorithms to solve random SAT instances (although I don't know how fast or successful they are). Also, for random 3-SAT w/ uniformly drawn clauses, it is known that the ratio of clauses to variables is important; if this ratio is less than ~4.25, instances are usually satisfiable, and if the ratio is greater than ~4.25, they are usually unsatisfiable, sometimes called the "threshold of unsatisfiability" for 3-SAT. There are similar analyses for other random k-SATs. This must mean that there is some way to determine if such random instances are satisfiable to begin with.

So my question: basically, at a high level, does this make "random k-SAT" somehow easier to solve than general k-SAT? Does this mean that it is in a different complexity class somehow and if so, what would it be?

Answer 1

Theoretically, we don't know how hard k-SAT is; P ?= NP remains an open question. Empirically, random $k$-SAT at the critical clause/variable ratio for each $k$ seems to require exponentially more effort as the number of variables increases. As an exercise I ran glucose on thousands of random 3-SAT instances with a 4.26 clauses/variables ratio, averaged the results for each instance size and graphed the results, number of variables vs. decisions.

As expected, the trend is exponential, though the number of decisions needed as problem size increases is nowhere near the naive $O(2^n)$ expectation or the proven $O(1.321^n)$ upper bound for a particular randomized search algorithm.

In a sense all the SAT problems that SAT solvers solve are easy. Any non-trivial problem encoded as a SAT instance will involve thousands if not millions of variables, meanwhile an $n$ value of only a few hundred produces expected worst-case runtimes that dwarf the history of our species. Yet SAT solvers are solving such problems, involving absurdly large numbers of variables and clauses, so we must either be very lucky in the problems we encounter or SAT is easy on average.

Random $k$-SAT instances in the critical region between under- and over-constrained seem harder than "industrial" instances for a given formula size. Industrial instances can have thousands of variables and still be solved rapidly enough to be useful in human timescales, while hard random 3-SAT instances of similar size would be completely infeasible to solve on average. Note also that random $k$-SAT instances can be made considerably harder by making them slightly less uniform; see "Generating Difficult SAT Instances by Preventing Triangles".