Hacker News

points by criemen 3 days ago | 0 comments

Wow. Complexity class separations are really really rare.

Can an expert in sat solving comment if there's any immediate applications of the method from the paper? Or is SAT solving in general pretty far away from worst-case times, and this is a theoretical algorithm which would be hard to apply in practice.

[–] bsubs 3 days ago

SAT-solving expert here. No immediate applications (the results in the paper are "galactic"). The main question is whether some ideas here will snowball into other ideas, one of which could eventually be very practical.

[–] sebmellen 3 days ago

This is a complete non-sequitur, but I checked out your web page. I love the Curious George image. My daughter has been deeply into the Curious George episodes for the past couple of months, and I don't think I've seen him show up in many other places besides kids' shows :D

[–] angry_octet 3 days ago

I think of Curious George Goes to a Chocolate Factory when I fire up Claude Code.

[–] chr15m 3 days ago

Such a good show. My kids grew up on it!

[–] ashkankiani 3 days ago

What do you mean by "galactic"?

[–] yyyk 3 days ago

Galactic algorithms have such huge constants they figuratively need a galaxy-sized computer and/or galaxy-sized problem, to have any advantage over the normal solutions. Imagine a generic sorting algorithm in O(n) that had a constant of 10^92 **. Technically superior but in practice unusable.

** Yes, I know that's proven to be impossible.

[–] MichaelDickens 3 days ago

There are realistic situations where galactic O(n) sorting algorithms exist, right? 32-bit integers can be sorted in O(n) using 2^32 words of memory, using bucket sort[1].

If objects have a maximum size of 4 GB (= 2^35 bits), then arbitrary objects can be sorted in O(n) using 2^2^35 bits of memory.

[1] https://en.wikipedia.org/wiki/Bucket_sort

[–] yyyk 3 days ago

Right, that's why I wrote "a generic sorting algorithm". Your case adds the integer limit which allows it to avoid O(nlogn) minimum.

[–] adrianN 3 days ago

You can use Radix sort https://en.wikipedia.org/wiki/Radix_sort to lower the memory requirement for limited bit-width integers. But there are more practical o(n log n) methods for sorting integers.

[–] adgjlsfhk1 3 days ago

Well optimized radix sorts are actually pretty fast (assuming you have the proper fallbacks to quicksort/insertion sort to deal with medium/small sizes)

[–] kite42 3 days ago

https://en.wikipedia.org/wiki/Galactic_algorithm

[–] gradus_ad 3 days ago

Do we know they are galactic?

[–] zahlman 3 days ago

> A galactic algorithm is an algorithm with state-of-the-art theoretical (asymptotic) performance, but which is not used due to practical constraints.

Yes, I think we can pretty safely say that the algorithm in the paper is not used due to practical constraints. This is a subjective judgment, but pretty clear from the paper that the algorithms aren't practical to apply.

[–] infamouscow 3 days ago

The data you put into a SAT solver has substantial effect on it's performance in practice. Real world inputs tend to be much nicer than pathological ones, so I don't think there's much practical application, but I also haven't read the paper yet.

[–] kingstnap 3 days ago

I also haven't read ths paper but coding agents absolutely are a part of modern SAT solver coding challenges.