Why SAT Is Hard
matklad.github.io
matklad.github.io
This isn’t really true; as any undergrad will have been told, it’s at least as hard as any NP problem, where A is as hard as B when there is polynomial-time computable function f such that we may determine whether an arbitrary b ∈ B by determining whether f(b) ∈ A. (I think I’ve that the right way round.)
There are lots of these!⁰
It’s not obvious to me that there’s a robust, meaningful and useful notion of hardness on which SAT is the hardest NP problem.
0: https://en.wikipedia.org/wiki/List_of_NP-complete_problems
It is of course possible to construct a problem that will require strictly more steps than the most efficient algorithm for SAT; for example, we could give a language SAT-PRIME = {<φ,n>: φ is satisfiable and n is prime>, which will take longer to decide than SAT. (Primality can be checked by the Agrawal–Kayal–Saxena test in polynomial time.) But note that SAT-PRIME is polynomially reducible to SAT, so on the notion of hardness as given by polynomial reducibility, it is in fact just as hard.
Of course, there are other notions of hardness, but the question is whether those notions are actually useful. Not really, in this case. P is closed under many things; in particular, it is self-low—i.e., L ∈ P just in case L ∈ P^P, where A^B = {L: L is decidable in time A with access to an oracle for B deciding instances of B in one step}. Now being a bit more fine-grained is useful for problems we know to be in P—for example, the recent result on max flow.⁰ But when we’re dealing with exponential-time best-known worst-case complexities (which is the case for all NP-hard problems, since we have no proof yet that P = NP), plonking on a polynomial doesn’t seem so bad.
A minor point, admittedly, but the second part of this statement is not true. Running time is w.r.t. the length of the input, and <φ,n> is longer than just φ. Deciding whether n is prime is easy, so per bit of input the algorithm is faster.
[1] https://en.wikipedia.org/wiki/Cook%E2%80%93Levin_theorem
Yes, SAT is hard.
But, the vast majority of SAT problems can be solved really fast.
The second one is one of the little known advancements in computer science which happened in this century. Fast SAT solvers power a lot of the interesting software out there.
Can you give examples? I can't think of anything I use regularly that would use that, with possible exceptions of Make and maybe a compiler (for optimisation)
I'd concur that these are interesting but maybe seldom used pieces of software, except for package management.
I don't think the standard TLA+ checker (TLC) uses SAT explicitly, though there's an alternate checker (Apalache) that uses a Satisfiability Modulo Theories solver like Z3. (Caveat that I've been wrong about stuff like this before, never dug into the implementation of TLA+ tools, but that's what I pick up from https://lamport.azurewebsites.net/tla/tools.html )
It is now easier and faster to encode most graph problems and have a SAT solver go at it, compared to carefully designing and tuning your custom graph algorithm for performance in the kinds of graphs you care about.
As for examples, there isn't much retail software that really needs SAT. But you might have indirectly used firewall/configuration management, home automation, flight/factory scheduling, route planning, etc.
There are some other uses, e.g. for programming languages with advanced type systems, but I doubt most people interact with SAT solvers basically ever.
You are right that most people do not have to interact with SAT solvers. Everyone has, almost surely, interacted with software with uses SAT solvers or have used SAT solvers for development tools.
If not software, your chips were definitely designed using tools which are nowadays based on SAT.
To some degree sure (assuming a generous definition of "designed"). I mentioned formal verification, and I expect synthesis uses it a bit. Still a pretty minor use IMO. You definitely could still design chips without SAT/SMT.
It turns out that most randomly generated SAT instances in this way will lack certain features that tend to make industrial instances "hard," and in fact there is research on randomly generating random SAT instances which have those features and thus which are more difficult to solve. For instance: https://dl.acm.org/doi/fullHtml/10.1145/3385651
Which would seem strange, since, intuitively, a hard worst-case means just that the problem is "possibly hard".
For SAT, you can sort of correlate difficulty with the number of irreducible clauses.
The reason why its not studied as much by theoretical computer science as is by algorithm-implementers, is that "average" is not uniquely defined. For instance, you can talk about the uniform distribution for a lot of problems, but not always. Suppose you want to investigate the complexity of solving certain types of equations, involving matrices as unknowns. How do you take the uniform distribution over matrices over the (infinite) real numbers? In principle, there are technical definitions you can make [3], and [2] has some results about this, but at the end of the day, there is no objectively superior way of doing it.
What this all leads to are two questions. (1) Would studying average-over-some-sampling-distribution-case complexity yield insights on what is computation? I don't know.
(2) Is it practically useful to classify problems in this way? Not really. Because in the real world, your distribution will rarely be uniform, so it is far better to optimize your algorithms for the distribution you do get.
[1] https://en.wikipedia.org/wiki/Average-case_complexity
[2] https://arxiv.org/pdf/cs/0606037.pdf
[3] https://mathoverflow.net/questions/76295/intuition-for-haar-...
> Note that it is not desirable for the candidate function to be NP-complete since this would only guarantee that there is likely no efficient algorithm for solving the problem in the worst case; what we actually want is a guarantee that no efficient algorithm can solve the problem over random inputs (i.e. the average case). In fact, both the integer factorization and discrete log problems are in NP ∩ coNP, and are therefore not believed to be NP-complete.
Regarding this question:
> How do you take the uniform distribution over matrices over the (infinite) real numbers?
Well, naively, how about screw the real numbers and just take the uniform distribution over the, say, 64 bit floats, which are conveniently finite? At least if we use those in practice? But I guess this goes in the direction of "Because in the real world, your distribution will rarely be uniform", since the 64 bit floats are a subset of the real numbers, and any uniform distribution over the former is equivalent to a non-uniform distribution over the latter (probability 0 to any reals not in the 64 bit floats).
Complexity theory is a very subtle science.
I hate apt/deb bundling. I prefer brew/port/pkg atomicity with explicitly defined version dependent declarations and metaports distinct.
That might be how most people interact with SAT.
Makefiles too maybe, I'm unsure if make does it's dependency checks in SAT
The reason package dependencies can get complex in Linux distributions is that you can choose different versions of a package, and each version has dependencies on specific version ranges of other packages. Of course it would be a lot easier if you could choose to install multiple versions of the same package in parallel, and don't care about minimising the number of parallel versions.
[1] https://en.wikipedia.org/wiki/Boolean_satisfiability_problem
x^4 and x^10 are both polynomials.
what are you referring to?
Obviously x^4 != x^10, but noone has ever proven that "if SAT is P, then it would have the lowest (or highest) polynomial complexity among the other problems", or anything similar
> [All NP-hard problems] have equivalent difficulty.
I get what OP meant, but there can still be some NP-hard problems that are more difficult than others.
As I said, x^4 and x^10 are both polynomials. I wouldn‘t call them "equivalent" though.
A problem A is NP-complete if:
- you can verify it's solution in polynomial time
- you can reduce it to any other NP-complete problem in polynomial time
Since polynomial reduction is transitive, the second point is equivalent to saying that "you can reduce it to SAT in polynomial time".
The reduction is simply a function that compiles the starting problem to SAT and preserves it's solvability (in a bijective way). In other words, to prove that a problem is NP-compelte, you must write a compilation function to SAT and also prove that every solution to the starting problem is also a solution to the destination problem in SAT. Furthermore you must also prove that any solution in the SAT version can be "decompiled" to a proper solution in the starting problem, so this is where the equivalence comes from and it's the reason that SAT is not really anyhow harder than other NP-complete problems.
The thing is, SAT has been heavily researched, so that's why you have extremely efficient SAT-solvers. So if you want to solve an NP-complete problem, you can simply compile it to SAT, solve it with well-known SAT-solvers and "decompile" the solution to your starting problem
The intuition here is that if you have a magic algorithm which solves X efficiently, you should be able to use this algorithm to solve any other NP problem, like SAT.
Tangentially related: I have thought recently that we really need to refresh the way that we explain these ideas to beginners in this new world of AI/ML doing everything.
For instance, here is an excerpt from Scott Aaronson's excellent paper on the topic:
"To illustrate, suppose we wanted to program a computer to create new Mozart-quality symphonies and Shakespeare-quality plays. If P = NP via a practical algorithm, then these feats would reduce to the seemingly easier problem of writing a computer program to recognize great works of art. And interestingly, P = NP might also help with the recognition problem: for example, by letting us train a neural network that reverse-engineered the expressed artistic preferences of hundreds of human experts. But how well that neural network would perform is an empirical question outside the scope of mathematics."
This has been kind of the standard way to explain this stuff to beginners for the last 20 years or so. It is an excellent paper and I highly recommend reading. Aaronson also goes on to explain how these are imperfect metaphors, that they are just for building intuition, etc, and gives better technical details. But it's still a good intuition-builder regardless.
Or at least it was. How do we explain all of this stuff now that we have StableDiffusion and ChatGPT? From here on, people are going to grow up in a world in which these things are commonplace, rather than it being questionable how physically possible they will ever be. The "empirical question" Aaronson talks about has largely been proven in the affirmative, so given that we are here, how do we explain this stuff now?
Some abbreviations are so well known in certain fields that spelling them out in a text written for people experienced with that field isn't that necessary. For people who have any familiarity with this field at all, SAT (and NP in NP-complete, for that matter) are such abbreviations. I'm not against the idea of explaining what SAT stands for either, but your rule clearly doesn't hold up.
EDIT: one point I will agree with though is that the Hacker News title should have been written for a more general audience; something like "Why SAT (boolean satisfiability) is hard". But that's a complaint about the submitter, not the author.
I’ve been out of academics for a while, and at first I thought this was talking about the American college exam.
Feels like the audience that this post is directed to is essentially "an earlier version of the author", which, to be fair, is a common mistake. I anticipate the average HN reader should be able to understand this blog post - I know what the boolean satisfiability problem is but have never seen it abbreviated as just "SAT".
Don't mean to be overly harsh toward the author, but a first step in good writing is to define who your audience is.
I'm curious what else you think of when you see SAT, though?
My bodily arrangement when I ate breakfast
The sixth day of the week according to crontab
Etc etc
In those comments, people complain that they don't understand what kind of gnu you're talking about, that they thought you were talking about wildebeest herding, and they say you obviously should have expanded the GNU abbreviation in the title.
That's what I feel is going on here.
And not just dive in with something like this: „Ever wondered what happens if you open a TTY and APT something?“, more like: „Have you ever wondered what happens if you install Linux packages with APT on the console?“
I agree that GP's rule doesn't apply in all cases (and they did say "rule of thumb," which implies imprecision), but I think it applies to this blog post. The author explains Big-O notation and Turing Machines, but uses the abbreviation SAT without explaining what it means.
The inconsistency is a symptom of the author forgetting to think through their intended audience and what they can be assumed to know already. I see this often on technical blog posts, and it's unfortunate because it's easily fixable.
If the author is trying to reach the type of reader who doesn't immediately recognize terms like "Big-O" or "Turing Machine," then they need to explain SAT more.
As for the previous commenter, all of their examples are pretty much irrelevant to what you are trying to do. A random Linux tutorial doesn't need to spell out CLI acronyms, but if you write an article "Hacking Bash for fun and profit" it's expected you put one paragraph background on bash, and explain the acronym.
Yes, it is generally a good practice.
I would avoid abbreviations if possible: "install xyz with your package manager", "switch to terminal", "run the script", "extract the archive". In your last example, I would ask myself if I need to specify it's a TAR. Does it matter that it's TAR? Are there any other archives in this project?
I agree that you should write for your audience and if you know they are experts like you, you don't have to explain everything. Personally, I err on the side of assuming less and explaining more.
Funny thing is, if you search for SAT on Hacker News [1] is has results for both satisfiability problems and admission tests. Even funnier is that in the second context, SAT nowadays means just SAT.