Gate elimination: Circuit size lower bounds and #SAT upper bounds

We show that many known proofs (of circuit size lower bounds and upper bounds for #SAT ) fall into this framework. Using this framework, we prove the following new bounds: average case lower bounds of 3.24n and 2.59n for circuits over U2 and B2, respectively (though the lower bound for the basis B2 is given for a quadratic disperser whose explicit construction is not currently known), and faster than 2n #SAT -algorithms for circuits over U2 and B2 of size at most 3.24n and 2.99n, respectively. Here by B2 we mean the set of all bivariate Boolean functions, and by U2 the set of all bivariate Boolean functions except for parity and its complement.