ADDMC: Weighted Model Counting with Algebraic Decision Diagrams

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

We present an algorithm to compute exact literal-weighted model counts of Boolean formulas in Conjunctive Normal Form. Our algorithm employs dynamic programming and uses Algebraic…