Comment by zero_k | Hacker News Reader

Comment by zero_k | Hacker News Reader

Random k-SAT is useless. I won a number of awards at SAT competitions over the years -- not in random k-SAT, they don't even run that track anymore [1] And I'm pretty damned certain whatever that paper is saying, could be fixed with classical algorithms, if anyone cared about random k-SAT. But nobody does, for a good reason. I could go on ranting about quantum, but I'll stick to the one thing I actually know about, SAT solving.

I think there are some really cool things out there, if you wanna dump research money into. For example SMT, model counting, symbolic execution, automated invariant finding, CHC, BMC, function synthesis, programming language research.

Academia will one day wake up, and realize that they've been awarding tenure to people who have done nothing but a quantum buzzword generator, while the people working hard at important topics are left behind. Like the dude (Victor Ambros) who recently got the Nobel only to be previously declined tenure at Harvard. Big fail.

[1] https://satcompetition.github.io/2024/results.html

By the way, if you truly care about NP-optimization, e.g. MaxSAT algorithms, there's a lot of good work being done, just check out [1]. It's fun, and useful. You could make >$1B just by slightly improving global logistics via such algorithms. Yes, scalability can be an issue, but it only takes some work to cut the problems into chunks, and do local optimization at each level, rather than total global optimization. Yes, it won't be a global optimum, but likely significantly better than what's out there right now. They already use these algorithms for e.g. train and bus schedule optimization.

[1] https://maxsat-evaluations.github.io/

Hypothetically: If a friend with interest in this kind of logistics were to be looking for a job. Which company would one tell said friend to look at?

Cadence is a good one. There are also bus/train schedule optimization startups/companies. AWS is also hiring in this field, a lot, but I wouldn't recommend it. Even though many people there are very good, and I respect some of the individual people there very much.

I fell in love with optimisation problems but haven’t played with them in a while…

What are some books to read more about non-linear optimisation that’s also non-machine learning (I’ve dabbled a lot with metaheuristics and genetic algorithms) but haven’t implemented a SAT solver (only played with what Prolog gives you)

Geoff Hinton was denied an academic position at the University of Sussex's CS department where he had done postdoc work (That department is now 'famous' for consciousness studies and integrated information theory https://osf.io/preprints/psyarxiv/zsr78. I bet they are kicking themselves now ...)

> "Academia will one day wake up, and realize that"

Charlie Munger famously said, "Show me the incentive and I'll show you the outcome" ...

> Geoff Hinton was denied an academic position at the University of Sussex's CS department

These kind of anecdotes are fairly common I believe. Understanding anyone's academic potential is enormously difficult, and the competition is fierce. Hindsight is 20/20 and whatnot.

> Random k-SAT is useless

Other than cryptography, is there any real-world value in solving random problem instances of NP-complete problems (at least when average case approaches worst case, based on the parameterization of the problem)? Presumably these are instances that do not have any underlying mathematical structure as a truly random problem instance is Kolmogorov-maximal, and thus even if you solve the problem via brute-force, the result still isn't useful for any predictive purpose.

Other than cryptography? Like, you see a use-case for it there? Please do educate me! IMO there's nothing there. It's a barren landscape. The desert is more alive.

Haha, I was more so meaning that cryptography depends on the actual existence of hard problem instances, which appears to be the case but hasn’t been conclusively proved.

I'm curious, which solver did you work on? And yeah, I've been working on formally verifying bitblasting in Lean (https://github.com/leanprover/lean4/pulls?q=+is%3Apr+author%...), and it's genius --- the algorithms, the reductions, the heuristics, it's all so deep.

Wow, nice work [1] ! I used to work on CryptoMiniSat a lot. Nowadays I'm doing model counting and maybe synthesis, if all goes well [2]

[1] https://github.com/leanprover/lean4/pulls/bollu [2] https://x.com/SoosMate/status/1827308967208317241

Reply on news.ycombinator.com