Header menu link for other important links
X
An improved deterministic #SAT algorithm for small de Morgan formulas
R. Chen, V. Kabanets,
Published in Springer Verlag
2014
Volume: 8635 LNCS
   
Issue: PART 2
Pages: 165 - 176
Abstract
We give a deterministic #SAT algorithm for de Morgan formulas of size up to n 2.63, which runs in time. This improves upon the deterministic #SAT algorithm of [3], 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 [12]. 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. © 2014 Springer-Verlag Berlin Heidelberg.