Correlation bounds and #SAT algorithms for small linear-size circuits

We revisit the gate elimination method, generalize it to prove correlation bounds of boolean circuits with Parity, and also derive deterministic satisfiability counting algorithms for small linear-size circuits. Let B2 be the full binary basis, and let U2=B2∖{⊕,≡}. We prove that, for circuits over U2 of size 3n−nϵ for any constant ϵ>0.5, the correlation with Parity is at most 2−nΩ(1), and there is a #SAT algorithm (which counts the number of satisfying assignments) running in time 2n−nΩ(1); for circuit size 3n−ϵn for ϵ>0, the correlation with Parity is at most 2−Ω(n), and there is a #SAT algorithm running in time 2n−Ω(n). Similar correlation bounds and algorithms are also proved for circuits over B2 of size almost 2.5n.