Correlation Bounds and #SAT Algorithms for Small Linear-Size Circuits.
Ruiwen Chen, Valentine Kabanets · Electronic colloquium on computational complexity · 2014
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 >0.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 >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.