I wonder if it's possible to do a similar thing for codegen. i.e. generate more efficient code based on SMT solver and CPU model.
http://theory.stanford.edu/~aiken/publications/papers/asplos...
They had to restrict themselves to instruction sequences of length 3 due to limited resources, and say that to go beyond instruction sequences of length 4 they would need a better approach.
(both are brute force though, not solver-based)
Modeling is not even the hard part, it's modeling in a way that doesn't take till the heat death of the sun to solve ;-)