A satisfiability algorithm for constant depth boolean circuits with unbounded fan-in gates

We consider the problem of efficiently enumerating the satisfying assignments to AC0 circuits. AC0 circuits are Boolean circuits with n inputs and their negations, one output, m = poly(n) total gates, and constant depth, and consist of unbounded fan-in AND and OR gates. The primary technical tool we use is a new algorithmic approach for efficiently simplifying restricted classes of circuits. This approach is based on a new extended version of Hastad's Switching Lemma. As the main result, we present a Las Vegas algorithm which takes an AC0 circuit as input and outputs a set of restrictions (assignments to subsets of the inputs) which partition {0; 1}n such that under each restriction the out-put of the circuit is constant. With high probability, the algorithm runs in time poly(m; n) 2n(1-[mu]) and outputs at most 2n(1-[mu]) restrictions, where = 1=O(lg m/n + d lg d)d-1. This is optimal up to the constants in the big-O for enumerating solutions with restrictions. This also implies the best known algorithm for AC0 circuit satisfiability and for counting satisfying assignments. Using similar techniques, we also give an algorithm for enumerating the solutions to a k-cnf, but where [mu] 1=O(k). Previously, algorithms with similar savings [mu] were known for finding a single satisfying assignment to a k-cnf, but not for counting or enumerating satisfying assignments. These results have some interesting applications to circuit lower bounds. We prove a new bound on the correlation of AC0 circuits with parity which is optimal up to constants, and show how several classic AC0 circuit lower bounds follow straightforwardly from our algorithm. Then, we use a powerful theorem due to Williams to show how a minor improvement in the running time for finding a single satisfying assignment for an AC0 circuit would imply NEXP 6 NC