The relation of and , i.e. efficiency of different encodings might be highly dependent on different solvers.
Equivalence preserving transformations are and different notions of equivalence are an important point, effects to performance however, are not completely clear.
One possibility would be ``blind" optimizations (e.g. by dropping rules), using equivalence verifiers as recently proposed.