| ▲ | criemen 8 hours ago |
| 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 7 hours ago | parent | next [-] |
| 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 6 hours ago | parent | next [-] | | 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 | | | |
| ▲ | ashkankiani 7 hours ago | parent | prev | next [-] | | What do you mean by "galactic"? | | |
| ▲ | 2 minutes ago | parent | next [-] | | [deleted] | |
| ▲ | yyyk 7 hours ago | parent | prev | next [-] | | 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 7 hours ago | parent [-] | | 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 6 hours ago | parent | next [-] | | 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 4 hours ago | parent | prev | next [-] | | 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 4 hours ago | parent [-] | | Well optimized radix sorts are actually pretty fast (assuming you have the proper fallbacks to quicksort/insertion sort to deal with medium/small sizes) |
| |
| ▲ | 6 hours ago | parent | prev [-] | | [deleted] |
|
| |
| ▲ | kite42 7 hours ago | parent | prev [-] | | https://en.wikipedia.org/wiki/Galactic_algorithm |
| |
| ▲ | gradus_ad 6 hours ago | parent | prev [-] | | Do we know they are galactic? |
|
|
| ▲ | infamouscow 8 hours ago | parent | prev [-] |
| 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 7 hours ago | parent [-] | | I also haven't read ths paper but coding agents absolutely are a part of modern SAT solver coding challenges. |
|
