Compactly representing the solution set of a SAT instance This question has risen in my mind after reading András Salamon's and Colin McQuillan's contributions to my previous question Counting solutions of Monotone-2CNF formulas. 

EDIT 30th Mar 2011
Added question n° 2.
EDIT 29th Oct 2010
Question rephrased after András proposal to formalize it through the notion of nice representation of a solution set (I've modified his notion a little bit).

Let $F$ be a generic CNF formula with $n$ variables. Let $S$ be its solution set. Clearly, $|S|$ may be exponential in $n$. Let $R$ be a representation of $S$. $R$ is said to be nice if and only if the following facts are all true:


$R$ has polynomial size in $n$.
$R$ allows to enumerate the solutions in $S$ with polynomial delay.
$R$ allows to determine $|S|$ in polynomial time (i.e. without enumerating all the solutions).


It would be great if it is possible, in polynomial time, to build such a $R$ for every formula.


  Questions:
  
  
  Did anyone ever prove that there exists a family of formulas for which such a nice representation can't exist?
  Did anyone study the relationship between the representation of $S$ and the symmetries exhibited by $F$? Intuitively, symmetries should help to compactly represent $S$ because they avoid the explicit representation of a solution subset $S' \subset S$ when $S'$ actually boils down to just one solution (i.e. from every $s_i \in S'$ you can recover every other $s_j \in S'$ by applying a proper symmetry, thus every $s_i \in S'$ is itself representative of the whole $S'$)
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?