posts/sat-supercompilation

[giscus[bot]]

posts/sat-supercompilation

https://hirrolot.github.io/posts/sat-supercompilation.html

[mocenigo]

Hi, I am a cryptographer and we use a lot of XORs, therefore we tend to use solvers like cryptominisat that added direct XOR support. Does your experiment implement XOR support, or would it be easy/trivial to add it (without expressing the XOR in terms of ANDs and ORs, which would quickly become too expensive)?

[hirrolot]

The solver demonstrated in the blog post uses an "internal representation" consisting of If (x, m, n), T, and F. Therefore, XOR must be encoded in terms of these three constructors. Since expressing XOR via OR and AND and then boiling down this combination of ORs and ANDs to the internal representation does effectively this, I think it's the only way to encode XOR.

Of course, it'd be very expensive to solve even relatively small SAT formulas. A possible way to optimize it is to partially evaluate the supercompiler based on the knowledge of the SAT solver (for example, using Flambda). The unknown "data" component would then be a particular SAT formula. This will reduce some interpretive overhead.

One more thing to try is to leverage metasystem jumping. Since supercompilation can be seen as a metasystem transition (in Turchin's terminology), it should be possible to resort to direct interpretation if some unknown variable doesn't get in the way of supercompilation. In modern language, this is somewhat similar to JIT. See "Metavariables: their Implementation and Use in Program Transformation" for more details.

[mocenigo]

For some reason I thought this would bring some speedups, I am THAT naive. Anyway, glorious stuff you are doing, and I mean it.