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-\delta_{c,k})} for \delta_{c,k} = c^{-O(c^2k2^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.