8 ms·
Why SAT Is Hard
- fastball 4y agoFor those confused, this is not "SAT" as in the Scholastic Assessment Test, but rather SAT for "boolean SATisfiability"[1]. [1] https://en.wikipedia.org/wiki/Boolean_satisfiability_problem https://en.wikipedia.org/wiki/Boolean_satisfiability_problem
- bee_rider 4y agoIf it were the former, the title would have to be “why the SAT is hard.”
- andix 4y agoA rule of thumb: the first time you use an abbreviation in a text you explain it.
- deleted 4y ago[deleted]
- mort96 4y agoIf you write a post for experienced Linux users about using Linux, do you generally write "first, install package xyz with Advanced Package Tool (APT)", or "switch to a Terminal TYpewriter (TTY)" or "Run the following Bourne Again SHell (BASH) script"? "Extract this Tape ARchive (TAR) ball"? 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.
- bobthepanda 4y agoThe thing is that SAT has many possible meanings as an acronym and this isn’t the most common one. I’ve been out of academics for a while, and at first I thought this was talking about the American college exam.
- mort96 4y agoThis sounds like a complaint about the hacker news title, which should have been written for a general HN audience, not a complaint about the blog post, where it is perfectly clear (for its target audience) that SAT means the boolean satisfiability problem.
- andix 4y agoThe title in the blog post is exactly the same.
- mort96 4y agoWhich is the problem if the title of the blog post is intended for a mathematical audience and the title of the HN post is intended for the general HN audience.
- hn_throwaway_99 4y agoAs others have pointed out, if this is a blog post for a mathematical audience that understands basic concepts in complexity theory, why bother explaining "Big-O notation is a standard instrument for describing performance of algorithms, as it erases small differences which depend on a particular implementation of the algorithm." 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.
- totetsu 4y agoYeah.. Sat Is hard because of the Hangover from Fri?
- tantalor 4y agohttps://en.wikipedia.org/wiki/Boolean_satisfiability_problem https://en.wikipedia.org/wiki/Boolean_satisfiability_problem
- tromp 4y agoThis post sketches a proof of the NP-hardness of SATisfiabiliy of boolean formula [1]. [1] https://en.wikipedia.org/wiki/Cook%E2%80%93Levin_theorem https://en.wikipedia.org/wiki/Cook%E2%80%93Levin_theorem
- ggm 4y agoThose dependency chains in apt, brew, port/pkg.. that's one of the problem space SAT solvers address. 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
- unnah 4y agoYou don't need any complex algorithms such as SAT solvers for makefiles, because make does not need to choose from alternative ways to build an out-of-date makefile dependency. Either the dependency file already has a date newer than all its dependencies, or the file will be rebuilt by following deterministic rules. 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.
- deleted 4y ago[deleted]
- fooker 4y agoThere is an interesting bit of nuance here. 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.
- phkahler 4y ago>> 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)
- F-W-M 4y agoPackage manager, Static Analysis, Model Checking (like TLA+), probably scheduling software. I'd concur that these are interesting but maybe seldom used pieces of software, except for package management.
- F-W-M 4y agoThey play a big role in hardware design and verification as well. All in all, SAT solvers became very good, so the solution to many NP-hard problems is to encode them in SAT and solve them this way.
- hcs 4y agoFor model checking Alloy might be a better example, it directly builds SAT instances (through the Kodkod constraint solver) that are then solved with a SAT solver. 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 https://lamport.azurewebsites.net/tla/tools.html )
- 4y ago
- firechickenbird 4y agoInteresting informal summarization of SAT. However, there is no such thing as "the hardest" NP-complete problem. By definition of NP-completeness, if you solve ANY NP-complete problem in polynomial time, you can solve every other NP-complete problem in polynomial time, thus they have equivalent difficulty (although, some problems may seem intuitively easier than others).
- Hendrikto 4y agoThat is not entirely true. If you compare two implementations of bubble sort, they will both be O(n^2). Yet one can still be much more efficient than the other. x^4 and x^10 are both polynomials.
- firechickenbird 4y ago> That is not entirely true 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
- Hendrikto 4y agoI was referring to this: > [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.
- Avshalom 4y agoI think that was a slightly odd way of mentioning https://en.m.wikipedia.org/wiki/NP-hardness https://en.m.wikipedia.org/wiki/NP-hardness
- Strilanc 4y agoThat's only true if you focus purely on the cost as being polynomial or not. The constant factors, the exponents, and the ability to represent difficult problems compactly, can of course differ pretty substantially. The ability to find approximate solutions, and the difficulty of the average case, can also differ substantially from problem to problem. An example of an application where these kinds of details are crucial is cryptography.
- deafpolygon 4y agoSAT, what? Standardized Aptitude Tests?
- eynsham 4y ago> SAT is harder than any NP problem 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 https://en.wikipedia.org/wiki/List_of_NP-complete_problems
- klysm 4y agoTo form a counter example, could you make a marginally more difficult version of SAT? Or would it always be reducible to SAT?
- eynsham 4y agoIf it’s NP it’s polynomially reducible to SAT. There are problems that do not admit a polynomial reduction to SAT, but by Cook-Levin they’re not in NP. 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. 0: https://arxiv.org/abs/2203.00671 https://arxiv.org/abs/2203.00671
- ComplexSystems 4y agoGood post. 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?
- dusted 4y agoSite Acceptance Test? SATtelite communication ? We don't know, but we now know it's hard.
- temporal828 4y ago[flagged]
- Dalewyn 4y agoA link/title should be informative and useful with no prerequisites. Personally, I thought this was something to do with satelites.
- Wildgoose 4y agoI'm sorry, but on a tech site full of people working in IT, I genuinely think this is obviously about Boolean Satisfiability. There has to be a minimum standard of expected understanding - e.g. "Rust" on this site is unlikely to be about corrosion.
- imadethis 4y agoAnd as a person working in tech for the past 10 years, I had never heard of Boolean Satisfiability let alone SAT until I read through the comments on the post and the linked Wiki page. I would suggest that this topic is not as universal as you think it is.
- doctor_eval 4y agoPretty sure if they’d used the term “Boolean satisfiability” even once, we would have been able to work it out. But SAT could mean a million things and if you’re not using this stuff on a daily basis then it’s simply non obvious. It’s not the authors fault, they can write what they want. what’s pissing me off is the utterly unhelpful attitude of people responding to questions about wtf the guy is talking about.
- 4y ago