Earlier quoted context omitted.
All analytical solutions to optimization problems can be seen as special cases of the brute force search I guess. But SC is impractically slow for anything except a few instructions long sequences. edit: actually I was thinking of superoptimizers, I guess it's a different concept.
Superoptimizers have gotten a lot better in the past few years. E.g. have a look at [1]. [1] https://arxiv.org/abs/1211.0557
This paper from the same project was also cool: https://raw.githubusercontent.com/StanfordPL/stoke/develop/d...
Quote from abstract: " For many applications, the best possible code is conditionally correct: the optimized kernel is equal to the code that it replaces only under certain preconditions on the kernel’s inputs. The main technical challenge in producing conditionally correct opti- mizations is in obtaining non-trivial and useful conditions and proving conditional equivalence formally in the pres- ence of loops. We combine abstract interpretation, decision procedures, and testing to yield a verification strategy that can address both of these problems. This approach yields a superoptimizer for x86 that in our experiments produces binaries that are often multiple times faster than those pro- duced by production compilers"