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 ... more >>>