Lower bounds on #SAT?
To my knowledge, no one has figured out how to exploit the &quot;counting solutions&quot; property of #SAT in any lower bound on deterministic algorithms, so unfortunately the best known lower bounds for #SAT are basically the same as that for SAT.
However, there has been a little progress. Note that the decision version of #SAT is called &quot;Majority-SAT&quot;: given a formula, do at least $1/2$ of the possible assignments satisfy it? &quot;Majority-SAT&quot; is $PP$-complete, and given an algorithm for Majority-SAT, one can solve #SAT with $O(n)$ calls to the algorithm.
The closest that people have gotten to new lower bounds for #SAT (that are not known to hold for SAT) is with lower bounds for &quot;Majority-of-Majority-SAT&quot;: given a propositional formula over two sets of variables X and Y, for at least $1/2$ of the possible assignments to $X$, is it true that at least $1/2$ of the assignments to $Y$ make the formula satisfiable? This problem is in the &quot;second level&quot; of the counting hierarchy (the class $PP^{PP}$). Quantum time-space lower bounds (and more) are known for this class.
The survey at http://pages.cs.wisc.edu/~dieter/Papers/sat-lb-survey-fttcs.pdf gives an overview of results in this direction.
UPDATE: As of 2019, the first paragraph in the above is obsolete. It is known that #SAT requires a time-space product that is basically $n^2$. See for example
&quot;Quadratic Time-Space Lower Bounds for Computing Natural Functions with a Random Oracle&quot; https://drops.dagstuhl.de/opus/volltexte/2018/10149/