An Improved Deterministic #SAT Algorithm for Small De Morgan Formulas

摘要

We give a deterministic #SAT algorithm for de Morgan formulas of size up to n~(2.63), which runs in time 2~(n-n~Ω) . This improves upon the deterministic #SAT algorithm of, which has similar running time but works only for formulas of size less than n~(2.5). Our new algorithm is based on the shrinkage of de Morgan formulas under random restrictions, shown by Paterson and Zwick. 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, with high probability over the random assignments to the chosen variables, the original formula shrinks in size, when simplified using a deterministic polynomial-time formula-simplification algorithm.