5 ms·
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, th
by zellyn 3y ago
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/ http://www.satcompetition.org/
- CobrastanJorji 3y ago3-SAT is NP-Complete, so either (a) is correct or else P=NP.
- zellyn 3y agoTouché! 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 3y ago3-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.
- Hirrolot 3y agoThe 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 3y agoAh, 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 https://research.swtch.com/version-sat
- NooneAtAll3 3y agosad that SAT competition still hasn't moved from 00s and still is on http SAT conferences aren't on youtube either :(
- pixelpoet 3y agoI love that the favicon for the 2023 results is a Doge, lol: https://satcompetition.github.io/2023/results.html https://satcompetition.github.io/2023/results.html
- Hirrolot 3y agoHaha, awesome!