SAT solvers can prove that some (shorter) sequences are equivalent to other (longer) sequences. But it takes a brute force search.
IIRC, these super optimizing SAT solvers can see patterns and pick 'Multiply' instructions as part of their search. So it's more than traditional SAT. But it's still... At the end of the day.... A SAT equivalence problem.