We give a deterministic #SAT algorithm for de Morgan formulas of size up to n263, which runs in time 2n−n(1). This improves upon the deterministic #SAT algorithm of \cite{CKKSZ13}, which has similar running time but works only for formulas of size less than n25.

Our new algorithm is based on the shrinkage of de Morgan formulas under random restrictions, shown by Paterson and Zwick~\cite{PZ93}. We prove a concentrated and constructive version of their shrinkage result. Namely, we give a deterministic polynomial-time algorithm that selects variables in a given de Morgan formula so that, over the random assignments to the chosen variables, the original formula shrinks in size, when simplified using a deterministic polynomial-time formula-simplification algorithm