The exponential complexity of the satisfiability problem for a given class of Boolean circuits is defined to be the infimum of constants α such that the problem can be solved in time poly(m) 2~(αn), where m is the circuit size and n is the number of input variables [IP01]. We consider satisfiability of linear Boolean formula over the full binary basis and we show that the corresponding exponential complexities are "interwoven" with those of k-CNF SAT in the following sense. For any constant c, let f_c be the exponential complexity of the satisfiability problem for Boolean formulas of size at most cn. Similarly, let s_k be the exponential complexity of k-CNF SAT. We prove that for any c, there exists a k such that f_c≤ s_k. Since the Sparsification Lemma [IPZ01] implies that for any k, there exists a c such that s_k≤f_c, we have sup_c{f_c} = sup_k{s_k}. (In fact, we prove this equality for a larger class of linear-size circuits that includes Boolean formulas.) Our work is partly motivated by two recent results. The first one is about a similar "interweaving" between linear-size circuits of constant depth and k-CNFs [SS12]. The second one is that satisfiability of linear-size Boolean formulas can be tested exponentially faster than in O(2~n) time [San10, ST12].
展开▼
