A SATISFIABILITY ALGORITHM AND AVERAGE-CASE HARDNESS FOR FORMULAS OVER THE FULL BINARY BASIS

摘要

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-μ_c)n for someconstant μ_c＞ 0. As a byproduct of the running time analysis of our algorithm, we obtain strong average-case hardness of affine extractors for linear-sized formulas over the full binary basis.