Compactly representing the solution set of a SAT instance
As stated (revision 3), the question has a simple answer: no.

The reason is that even for the highly restricted class of representations given by Boolean circuits with AND, OR, and NOT gates, no nontrivial lower bounds are known.  (Clearly a circuit that represents $F$ will also represent $S$ implicitly, and it is easy to enumerate the solutions by changing the inputs to the circuit.)

For even more restricted representations, like monotone or constant depth circuits, exponential lower bounds are known.  There are also exponential lower bounds for representing formulas in CNF or DNF form, although these can be seen as special cases of constant depth circuits.  Finally, BDD representations can be seen as compact forms of DNF, but there exist formulas for which the BDD requires exponential size for any variable ordering.

To make your question more precise, please consider @Joshua's answer in some detail, and please clarify what you mean by "trivial to enumerate every single solution".



For revision 4, note the statement about BDD size.  Part of what you seem to be asking is: is there a more compact representation of DNF formulas than BDDs?  Let "BDD $B$ has superpolynomial size" mean "every BDD representing the same function as $B$, regardless of variable ordering, has superpolynomial size", and let "nice representation" mean "a representation that allows solutions to be enumerated with polynomial delay".  This more specific question then becomes:


  is there a family of formulas and a nice representation that has polynomial size while its BDDs have superpolynomial size?


Does this capture the essence of what you are asking?