I'm trying to compare two formulae to see which one is easier to satisfy and I thought that comparing how many models they have would be a good way to do so.
From what I've seen and read, it seems harder to count the number of models when a proposition appear more than once in a formula so I was wondering if it is possible to transform any propositional logic formula so that every propositions in it appears only once. If it is, is it more optimal to count the number of models after doing this transformation ?
There is no finite set of truth functions that will allow you to write every propositional formula without repeating letters.
Suppose that you have $k$ functions in your set.
Without loss of generality we can assume that there is no unary function -- you can avoid that by instead having each of your functions come in versions that precompose it with $\neg$ in each position, as well as with the everywhere true and false functions. Then there are still only finitely many functions.
Now if you have an expression with involving $n$ propositional variables, then without repeating variables there are at most $n-1$ function applications in the expression. So the number of symbols if we write down the expression in Polish notation is at most $2n-1$, and there are $n+k$ different symbols, so the number of different expressions is at most $(n+k)^{2n-1}$.
On the other hand, the number of truth functions we might want to express is $2^{2^n}$, which grows much faster than the number of expressions. So there cannot be an expression for each truth function.