# ADDMC: Weighted Model Counting with Algebraic Decision Diagrams

## TL;DR

This paper introduces ADDMC, an exact weighted model counting algorithm using Algebraic Decision Diagrams, which outperforms existing counters on a large benchmark set.

## Contribution

The paper presents a novel model counting algorithm employing Algebraic Decision Diagrams and demonstrates its superior performance over state-of-the-art methods.

## Key findings

- ADDMC significantly outperforms existing model counters on benchmark tests.
- Empirical evaluation shows the effectiveness of heuristics used with ADDMC.
- ADDMC improves the virtual best solver performance in weighted model counting.

## 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 primary 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 state-of-the-art exact weighted model counters (Cachet, c2d, d4, and miniC2D) on 1914 standard model counting benchmarks and show that ADDMC significantly improves the virtual best solver.