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 3nn for any constant u003e0.5, the correlation with Parity is at most 2n(1), and there is a #SAT algorithm (which counts the number of satisfying assignments) running in time 2nn(1); for circuit size 3nn for u003e0, 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.