Number of SAT checks that are needed to find all combinations of subset of boolean variables of a propositional formula
If you really want to enumerate all the assignments, then you really need to find a satisfying assignment and then block it by a clause. E.g. if you find a satisfying assignment $a_1=a_2=a_3=0$ you'd block it by $a_1\lor a_2\lor a_3$.

One, relatively easy improvement, is to reduce the found assignment to a (prime) implicant. For instance, if $a_1\rightarrow f$, then you know that all assignments with $a_1=1$ are satisfying ($a_1$ is an implicant). You can reduce an existing satisfying assignment to an implicant by throwing one variable at a time. Similar approach published first (I think) here [1].

Somewhat more general problem is quantifier elimination, i.e. you're given $\exists X. f$ with some free variables $Y$, where $X$ and $Y$ are sets of variables. The output is a formula $f'$ that has only free variables $Y$ and has the same set of satisfying assignments as $\exists X. f$. Some recent  papers on the problem [2][3].
(am a coauthor of the [3]).

[1] McMillan: Applying SAT Methods in Unbounded Symbolic Model Checking. CAV 2002

[2] Goldberg,Manolios: Quantifier elimination via clause redundancy. FMCAD 2013

[3] Klieber et: al Solving QBF with Free Variables. CP 2013