I think the only reason And does this is that it uses a frozenset internally, so by design it cannot hold duplicate arguments. 

I don't know what the code of using full expressions is here. I do know that in the SAT solver, everything is converted to a much more efficient set of integers representation, so you don't need to worry about that.