Lower bound on the number of solutions of 2SAT To compute the number of solutions of a 2SAT is a hard problem. Is there some nontrivial lower or upper bound on this number in terms of a “coarse-grained” description of the Boolean formula, for example, in terms of the number of clauses with only affermative literals, with one negation and with two negations.
 A: I don't have a definitive answer, but here are some thoughts.
For the sake of simplicity, consider only formulas where every clause has size 2 (no unit clauses) and with only positive literals (also known as monotone). One can re-interpret such a formula as a graph whose vertices are the variables and edges are the clauses (also known as the primal graph).
Now, it is obvious that setting all variables to true is a satisfying assignment. What do other satisfying assignments look like? Well, they set several variables to false, but in such way that no two variables set to false occur together in a clause. In the language of the primal graph, the variables set to false in any satisfying assignment form an independent set. The same is true in reverse: an independent set gives rise to a satisfying assignment, in which the independent variables are set to false. Thus the number of satisfying assignments is just the number of independent sets, including the empty set.
It directly follows that if the primal graph has an independent set of size $k$, then the formula has at least $2^k$ satisfying assignments. But computing the independence number (the size of the maximum independent set) is NP-hard itself.
But this doesn't necessarily yield a non-trivial lower bound. Consider the formula on $n$ variables whose primal graph is the complete graph $K_n$. Then its only maximal independent sets are singletons; and similarly all its satisfying assignments are the ones in which at most one variable is set to false, a total of $n+1$. This is, however, trivial: any monotone 2-CNF formula has all these models.
You can get a non-trivial lower bound in terms of the maximum degree of the primal graph (i.e., the maximum number of times a variable occurs in a clause), let's call it $\Delta$. By Brooks' Theorem, in a graph with $n$ vertices and maximum degree $\Delta$ that is neither a complete graph nor an odd cycle, there must be an independent set of size at least $\frac{n}{\Delta}$ , and thus the number of satisfying assignments of the corresponding formula must be at least $2^{\lceil\frac{n}{\Delta}\rceil}$. If you know more about your primal graph, you can use other results from graph theory to show existence of large and/or many independent sets.
EDIT
As a further suggestion, this paper proves that any connected graph with $n$ vertices and $m$ edges has an independent set of size at least
$$ \alpha(n,m) := \frac{1}{2} \left[(2m + n + 1) − \sqrt{(2m + n + 1)^2 − 4n^2}\right],$$
so a corresponding formula has at least $2^{\alpha(n,m)}$ satisfying assignments. A more recent paper mentions other bounds on the independence number in terms of coarse graph characteristics, as well as many references to other results about independent sets.
The example of the complete graph also shows that this lower bound can be arbitrarily off, because for $K_n$ we have $\alpha(n, m)=1$, so we have a lower bound of $2$ satisfying assignments, while the true number is $n+1$.
It's also not obvious to me whether this kind of reasoning can be generalized to formulas with negative literals; although monotone formulas themselves are interesting, because counting remains $\#P$ hard.
