[agent327]

I seem to remember that program equivalence is an NP-hard problem. I very much doubt that you can solve it by reducing it to logic gates.

[viraptor]

NP-hard is just a complexity class, not a minimal threshold. SAT solving is kind of a guided optimistic bruteforcing. If the example is small enough, you can still solve it very quickly. Same as you can solve travelling salesman for a small number of cities. We solve small cases of NP-hard things all over the place.

[viraptor]

(not to confirm it's an np-hard problem - it may not even be decidable generally, but in practice yes, you can check it that way and SMT2 theories provide the right ops)

[dragontamer]

That's why superoptimizers work on short sequences of code and take a long time doing so.