Absolutely. See [1] for instance. Superoptimization has been around since the 80s and at the first superoptimizer by Alexia Massalin targeted the 68000 instruction set.

[1] http://superoptimization.org/w/images/f/f1/Wp4.pdf

It's been done:

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.

This has been done in '87 by Massalin: https://www.cs.arizona.edu/~collberg/Teaching/553/2011/Resou...

(both are brute force though, not solver-based)

Massalin's superoptimizer required humans to check the correctness of optimizations. It also didn't generate parameterized peephole optimizations; it directly optimized concrete instruction sequences.

Yes, there are tons of papers on doing optimal scheduling/instruction selection/register allocation by using integer linear programming.

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 ;-)

I want to see efficient backends automatically generated from a flat list of assembly instruction descriptions using similar methods.