DPMC: Weighted Model Counting by Dynamic Programming on Project-Join Trees

Jeffrey M. Dudek, Vu H. N. Phan, Moshe Y. Vardi

We propose a unifying dynamic-programming framework to compute exact literal-weighted model counts of formulas in conjunctive normal form. At the center of our framework are projec…