Hacker News Reader

Comment by fooker | Hacker News Reader

There 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.

View on HN

>> 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)

Package 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.

They 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.

For 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 )

Yup, TLC is a brute force model checker and Apalache uses SMT.

Most package managers don't actually use SAT, because it's hard to get data about the version conflicts when it's unsatisfiable.

Think of it in terms of weird graph problems and algorithms.

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.

Print shops use SAT solvers to lay out pages on a large sheet of paper in the most efficient way, for example.

He's stretching the definition of "interesting" I think. The main application of modern SAT solvers (and SMT solvers) is formal verification, which I do think is interesting, but you're very unlikely to be using it.

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.

Have you used, interacted with, or benefited from AWS? ;)

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.

> 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.

Wait, does this mean "hard" refers merely to worst-case complexity, not to average-case complexity?

Which would seem strange, since, intuitively, a hard worst-case means just that the problem is "possibly hard".

Yes, "hard" in this context refers to worst-case complexity. In practice, lots of NP-hard problems can be solved, or approximately solved, in a reasonable amount of time. This is why traveling salesmen can exist, for instance.

Then it seems there should exist a more interesting category "really hard" which refers to average-case complexity. Yet I've never heard of such a complexity class?

The issue with defining such terms properly is that it's unclear what makes an 'average' problem instance.

For SAT, you can sort of correlate difficulty with the number of irreducible clauses.

That seems very reasonable for SAT.

Average-case complexity is studied quite a bit. There is some discussion on wikipedia [1]. Also see this paper, which discusses the average-case complexity of NP problems [2]

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-...

Well, thanks for the Wikipedia link. It says average complexity is very important for sorting algorithms and cryptographic one-way functions. I found especially this part remarkable:

> 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).

64-bit floats are a finite set. The solution of problems where the real numbers are replaced by the finite set is sometimes easier, but often much more difficult. The reason is that you can't do calculus over finite fields. For instance, taking the inverse of the natural log is efficient, but the inverse of the discrete log is a hard problem, and hence is used in cryptographic algorithms.

Complexity theory is a very subtle science.

Nontheless, in practice most algorithms have a limited range of inputs, in which case there should be no problem with infinity?

Beyond average case complexity, which is discussed below, there is also a rich research line on approximation algorithms. Interestingly, the effectiveness of approximation algorithms is not uniform across NP-Complete problems. There are problems where efficient approximation algorithms can be arbitrarily good and there are problems where if P!=NP then approximation algorithms have hard caps on their effectiveness. This is relevant for a lot of optimization tasks where you don't necessarily care about getting the best possible solution but would be happy getting pretty close.

As a nit, I think the vast majority cannot be solved fast? A large number of interesting ones can, though. Right?

Maybe (can't remember, might have never known), but not necessarily. As an example of the idea, consider the simplex algorithm as it applies to linear programming. It has exponential worst-case behavior, but people noticed that in practice the vast majority of interesting problems could be solved quickly. Later it was shown that all non-polynomial inputs do actually lie in some diminutive subspace.

"Vast majority" and "vast majority of interesting ones" may be completely different. The vast majority are just random; the vast majority of interesting ones will have some kind of structure, given by the real-world problem they represent.

As I understand it, I think that any randomly generated SAT problem will not be able to be solved quickly; however, SAT problems in the real world, even when they're large, tend to be quick for SAT solvers (most people solve the "Wedding Seating" problem for their own weddings, after all!), Why ordinary SAT problems tend to be easy to solve, last I checked was an open problem.

The "vast majority" of SAT instances would be something like a SAT instance you would draw uniformly at random from some kind of distribution on all possible circuits. Making this idea rigorous is what k-random SAT is all about.

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

Reply on news.ycombinator.com