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.
replyThis 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
replyI think of Curious George Goes to a Chocolate Factory when I fire up Claude Code.
replySuch a good show. My kids grew up on it!
replyWhat do you mean by "galactic"?
replyGalactic 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.
reply** Yes, I know that's proven to be impossible.
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].
replyIf 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.
Right, that's why I wrote "a generic sorting algorithm". Your case adds the integer limit which allows it to avoid O(nlogn) minimum.
replyYou 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.
replyWell optimized radix sorts are actually pretty fast (assuming you have the proper fallbacks to quicksort/insertion sort to deal with medium/small sizes)
replydeleted
replydeleted
replyDo we know they are galactic?
reply> A galactic algorithm is an algorithm with state-of-the-art theoretical (asymptotic) performance, but which is not used due to practical constraints.
replyYes, 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.
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.
replyI also haven't read ths paper but coding agents absolutely are a part of modern SAT solver coding challenges.
reply