We present a moderately exponential time algorithm for the satisfiability of Boolean formulas over the full binary basis. For formulas of size at most $cn$, our algorithm runs in time $2^{(1-mu_c)n}$ for some constant $mu_c>0$. As a byproduct of the running time analysis of our algorithm, we get strong average-case hardness of affine extractors for linear-sized formulas over the full binary basis.
展开▼
