ECCC-Report TR13-150https://eccc.weizmann.ac.il/report/2013/150Comments and Revisions published for TR13-150en-usMon, 04 Nov 2013 21:33:20 +0200
Paper TR13-150
| An Improved Deterministic #SAT Algorithm for Small De Morgan Formulas |
Valentine Kabanets,
Ruiwen Chen,
Nitin Saurabh
https://eccc.weizmann.ac.il/report/2013/150We give a deterministic #SAT algorithm for de Morgan formulas of size up to $n^{2.63}$, which runs in time $2^{n-n^{\Omega(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 $n^{2.5}$.
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.Mon, 04 Nov 2013 21:33:20 +0200https://eccc.weizmann.ac.il/report/2013/150