2020/08/19 by Jeffrey M. Dudek, Dudek, Jeffrey M., Vu H. N. Phan +3 · 4 citations
Computer Science · #Artificial Intelligence (cs.AI) #Bayesian Modeling and Causal Inference #Constraint Satisfaction and Optimization #Data Structures and Algorithms (cs.DS) #FOS: Computer and information sciences #Formal Methods in Verification #Logic in Computer Science (cs.LO)
paper · pdf · doi:10.48550/arxiv.2008.08748
openalex publication_date 2020/08/19 · openalex created_date 2022/07/23 · openalex updated_date 2026/07/28
We propose a unifying dynamic-programming framework to compute exact\nliteral-weighted model counts of formulas in conjunctive normal form. At the\ncenter of our framework are project-join trees, which specify efficient\nproject-join orders to apply additive projections (variable eliminations) and\njoins (clause multiplications). In this framework, model counting is performed\nin two phases. First, the planning phase constructs a project-join tree from a\nformula. Second, the execution phase computes the model count of the formula,\nemploying dynamic programming as guided by the project-join tree. We\nempirically evaluate various methods for the planning phase and compare\nconstraint-satisfaction heuristics with tree-decomposition tools. We also\ninvestigate the performance of different data structures for the execution\nphase and compare algebraic decision diagrams with tensors. We show that our\ndynamic-programming model-counting framework DPMC is competitive with the\nstate-of-the-art exact weighted model counters cachet, c2d, d4, and miniC2D.\n