[zellyn]

I'm almost completely clueless with both 3-SAT and supercompilation, but I'm willing to bet that if you found a neat trick that solves 3-SAT problems easily, then either or both (a) there are classes and/or sizes of 3-SAT problems for which your solution breaks down badly (goes exponential), or (b) what you're doing reduces to a 3-SAT strategy that the people who enter 3-SAT contests[1] already knew about a long time ago.

[1] http://www.satcompetition.org/

[Hirrolot]

The solution has exponential time and space complexity, which I noted in the blog post. It is only interesting for its simplicity and as a stress test for supercompilers.

[zellyn]

Ah, I missed that. Makes perfect sense! By the way, if you're interested in the "this problem can blow up badly because it can be converted to 3-SAT", you might like https://research.swtch.com/version-sat

[CobrastanJorji]

3-SAT is NP-Complete, so either (a) is correct or else P=NP.

[zellyn]

Touché! I guess I was thinking that there are often sub-classes of NP-complete problems that are amenable to much more efficient algorithms, and it might be easy to accidentally not try any hard ones. Turns out the author fully acknowledged exponential explosion, which I would have known had I read Final Words section instead of skimming everything after the intro!

[gbacon]

3-SAT is at least as hard as SAT, or SAT ≤p 3-SAT. We know this because we can translate arbitrary SAT instances into 3-SAT in polynomial time. 3-SAT is in NP because we can check a candidate solution in polynomial time by plugging in the values and evaluating.

More accurate than “an NP-complete subset of SAT” would be to say that SAT is polynomial-time reducible to 3-SAT or that we can solve SAT in terms of 3-SAT.

Combining both of these, each is reducible to the other. In some sense, they are the same problem. 3-SAT imposes just enough structure to force it into NP-complete. 2-SAT is in P.

[NooneAtAll3]

sad that SAT competition still hasn't moved from 00s and still is on http

SAT conferences aren't on youtube either :(

[pixelpoet]

I love that the favicon for the 2023 results is a Doge, lol: https://satcompetition.github.io/2023/results.html

[Hirrolot]

Haha, awesome!