We give a \#SAT algorithm for boolean formulas over arbitrary finite bases. Let B k be the basis composed of all boolean functions on at most k inputs. For B k -formulas on n inputs of size cn , our algorithm runs in time 2 n (1 − c k ) for c k = c − O ( c 2 k 2 k ) . We also show the average-case hardness of computing affine extractors using linear-size B k -formulas.

We also give improved algorithms and lower bounds for formulas over finite unate bases, i.e., bases of functions which are monotone increasing or decreasing in each of the input variables.