Circuit Size Lower Bounds and #SAT Upper Bounds Through a General Framework

摘要: Most of the known lower bounds for binary Boolean circuits with unrestricted depth are proved by gate elimination method. The most efficient algorithms #SAT problem on use similar case analyses to ones in elimination. Chen and Kabanets recently showed that can also be used prove average circuit bounds, is, size approximations an explicit function. In this paper, we provide a general framework proving worst/average upper is built ideas Kabanets. A proof such goes as follows. One starts fixing three parameters: class circuits, complexity measure, set allowed substitutions. main ingredient follows: going through number cases, one shows any from given class, find substitution measure reduces sufficient amount. This analysis immediately implies bound #SAT. To~obtain needs present construction function disperser/extractor sources defined substitutions under consideration. We show many proofs (of #SAT) fall into framework. Using framework, following new bounds: 3.24n 2.59n over U_2 B_2, respectively (though basis B_2 quadratic disperser whose not currently known), faster than 2^n #SAT-algorithms at 2.99n, respectively. Here mean all bivariate functions, functions except parity its complement.