Not all FPRASs are equal: demystifying FPRASs for DNF-counting

作     者：Meel, Kuldeep S. Shrotri, Aditya A. Vardi, Moshe Y. 

作者机构：Natl Univ Singapore Singapore Singapore Rice Univ Houston TX 77005 USA 

出 版 物：《CONSTRAINTS》 (约束)

年 卷 期：2019年第24卷第3-4期

页      面：211-233页

核心收录：

学科分类：08[工学] 0812[工学-计算机科学与技术（可授工学、理学学位）] 

基　　金：NSF [IIS1527668] NUS ODPRT Grant [R-252-000-685-133] AI Singapore Grant [R-252-000-A16-490] Sung Kah Kay Assistant Professorship Fund 

主　　题：Model counting Hashing Disjunctive normal form Boolean formulas Fully polynomial randomized approximation scheme ApproxMC 

摘      要：The problem of counting the number of solutions of a DNF formula, also called #DNF, is a fundamental problem in artificial intelligence with applications in diverse domains ranging from network reliability to probabilistic databases. Owing to the intractability of the exact variant, efforts have focused on the design of approximate techniques for #DNF. Consequently, several Fully Polynomial Randomized Approximation Schemes (FPRASs) based on Monte Carlo techniques have been proposed. Recently, it was discovered that hashing-based techniques too lend themselves to FPRASs for #DNF. Despite significant improvements, the complexity of the hashing-based FPRAS is still worse than that of the best Monte Carlo FPRAS by polylog factors. Two questions were left unanswered in previous works: Can the complexity of the hashing-based techniques be improved? How do the various approaches stack up against each other empirically? In this paper, we first propose a new search procedure for the hashing-based FPRAS that removes the polylog factors from its time complexity. We then present the first empirical study of runtime behavior of different FPRASs for #DNF. The result of our study produces a nuanced picture. First of all, we observe that there is no single best algorithm that outperforms all others for all classes of formulas and input parameters. Second, we observe that the algorithm with one of the worst time complexities solves the largest number of benchmarks.