IIRC, most of the time these just end up boiling down to 3-SAT, which will make the average Computer Science person throw up their hands in the air and say "it'

IIRC, most of the time these just end up boiling down to 3-SAT, which will make the average Computer Science person throw up their hands in the air and say "it's NP-Hard, you can't make it more efficient" (even though NP is still an open problem). I think there's one EE/CE professor at my university working on the SAT solvers that form the crux of the optimizers in most of these tools, but at the end of the day it's still a bunch of heuristics that, worst case, run in O(2^n) time.