Superoptimizers can be used to improve conventional optimizers by highlighting missed opportunities so a human can write additional rules.
Traditionally, superoptimizing is performed via exhaustive brute-force search in the space of valid instruction sequences.
It is also possible to use a SMT solver to approach the problem, vastly improving the search efficiency (although inputs more complex than a basic block remains out of reach).
[5] In 2001, goal-directed superoptimizing was demonstrated in the Denali project by Compaq research.
[6] In 2006, answer set declarative programming was applied to superoptimization in the Total Optimisation using Answer Set Technology (TOAST) project[7] at the University of Bath.