ADDMC: Weighted Model Counting with Algebraic Decision Diagrams
Jeffrey M. Dudek, Vu Phan, Moshe Y. Vardi
Abstract
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 Decision Diagrams as the main data structure. We implement this technique in ADDMC, a new model counter. We empirically evaluate various heuristics that can be used with ADDMC. We then compare ADDMC to four state-of-the-art weighted model counters (Cachet, c2d, d4, and miniC2D) on 1914 standard model counting benchmarks and show that ADDMC significantly improves the virtual best solver.
Topics & Concepts
HeuristicsComputer scienceLiteral (mathematical logic)Algebraic numberTrue quantified Boolean formulaBinary decision diagramSolverConjunctive normal formAlgorithmTheoretical computer sciencePropositional formulaBoolean satisfiability problemMathematicsProgramming languagePropositional variableMathematical analysisIntermediate logicOperating systemDescription logicBayesian Modeling and Causal InferenceFormal Methods in VerificationMachine Learning and Algorithms