Solving SAT via Positive Supercompilation

Re:Solving SAT via Positive Supercompilation by tgv on Friday February 02, 2024 @02:18AM (#39226004)

Any idea why there aren't? Not even to a small degree? To me, it looks like fairly straight-forward rewriting. Perhaps it's hard to tell how much is useful?

> deep program transformation

It doesn't have to be deep, does it? You can't transform the entire program, so there's an arbitrary cut-off anyway.

[ Parent | on HN ]

Re:Solving SAT via Positive Supercompilation by rowanG077 on Friday February 02, 2024 @04:18AM (#39226764)

I think there are a few big problems. Performance is a big one, code bloat is another. You also need a very good termination heurestic or there will be edge cases where compilation time spins out of control.

Here is some discussion here on why a pretty serious for GHC stalled: https://www.reddit.com/r/haskell/comments/2s97d0/the_state_a...

[ Parent | on HN ]

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

Supercompilation acts as global program optimization. As far as I'm aware, there were no attempts to supercompile separate libraries.

In fact, supercompilation subsumes many common optimizations, such as function inlining, constant propagation, list fusion, etc. So we can say that it's actually used "to a small degree", although I wouldn't really call it "supercompilation" per se.

The reason that full-blown supercompilation is not used is that it's too unpredictable -- the direct consequence of being too smart. I've elaborated on it in the final section of the blog post.

[ Parent | on HN ]