Solving SAT via Positive Supercompilation

Re:Solving SAT via Positive Supercompilation by zellyn on Thursday February 01, 2024 @02:25PM (#39220066)

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/

[ Parent | on HN ]

Re:Solving SAT via Positive Supercompilation by Hirrolot on Thursday February 01, 2024 @03:06PM (#39220641)

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.

[ Parent | on HN ]

Re:Solving SAT via Positive Supercompilation by zellyn on Thursday February 01, 2024 @03:29PM (#39220987)

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

[ Parent | on HN ]

Re:Solving SAT via Positive Supercompilation by CobrastanJorji on Thursday February 01, 2024 @02:55PM (#39220471)

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

[ Parent | on HN ]

Re:Solving SAT via Positive Supercompilation by zellyn on Thursday February 01, 2024 @03:33PM (#39221044)

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!

[ Parent | on HN ]

Re:Solving SAT via Positive Supercompilation by gbacon on Friday February 02, 2024 @02:09PM (#39232829)

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.

[ Parent | on HN ]

Re:Solving SAT via Positive Supercompilation by NooneAtAll3 on Thursday February 01, 2024 @04:58PM (#39222040)

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

SAT conferences aren't on youtube either :(

[ Parent | on HN ]

Re:Solving SAT via Positive Supercompilation by pixelpoet on Friday February 02, 2024 @12:25AM (#39225377)

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

[ Parent | on HN ]

Re:Solving SAT via Positive Supercompilation by Hirrolot on Friday February 02, 2024 @01:56AM (#39225879)

Haha, awesome!

[ Parent | on HN ]