An Improved Deterministic #SAT Algorithm for Small de Morgan Formulas

作者：Chen Ruiwen; Kabanets Valentine; Saurabh Nitin^*

来源：Algorithmica, 2016, 76(1): 68-87.

DOI：10.1007/s00453-015-0020-z

• de Morgan formulas
• Random restrictions
• Shrinkage exponent
• Concentrated shrinkage
• Algorithms from circuit lower bounds
• Deterministic #SAT algorithms

We give a deterministic #SAT algorithm for de Morgan formulas of size up to , which runs in time . This improves upon the deterministic #SAT algorithm of Chen et al. (Proceedings of the twenty-ninth annual IEEE conference on computational complexity, 2014), which has similar running time but works only for formulas of size less than . Our new algorithm is based on the shrinkage of de Morgan formulas under random restrictions, shown by Paterson and Zwick (Random Struct Algorithms 4(2):135-150, 1993). 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 given deterministic polynomial-time formula-simplification algorithm.

• 出版日期2016-9