ADDMC: Weighted Model Counting with Algebraic Decision Diagrams
Authors: Jeffrey Dudek, Vu Phan, Moshe Vardi1468-1476
AAAI 2020 | Conference PDF | Archive PDF | Plain Text | LLM Run Details
| Reproducibility Variable | Result | LLM Response |
|---|---|---|
| Research Type | Experimental | We empirically evaluate various heuristics that can be used with ADDMC. We then compare ADDMC to four stateof-the-art weighted model counters (Cachet, c2d, d4, and mini C2D) on 1914 standard model counting benchmarks and show that ADDMC significantly improves the virtual best solver. |
| Researcher Affiliation | Academia | Jeffrey M. Dudek, Vu H. N. Phan, Moshe Y. Vardi Rice University 6100 Main Street Houston, Texas 77005 {jmd11, vhp1, vardi}@rice.edu |
| Pseudocode | Yes | Algorithm 1: ADD Literal-Weighted CNF Model Counting |
| Open Source Code | Yes | The ADDMC source code and experimental data can be obtained from a public repository (https://github.com/vardigroup/ADDMC). |
| Open Datasets | Yes | We use a set of 1914 CNF literal-weighted model counting benchmarks, which were gathered from two sources. First, the Bayes class1 contains 1091 benchmarks. The application domain is Bayesian inference (Sang, Beame, and Kautz 2005). The accompanied literal weights are in the interval [0, 1]. Second, the Non-Bayes class2 contains 823 benchmarks. This benchmark class is subdivided into eight families: Bounded Model Checking (BMC), Circuit, Configuration, Handmade, Planning, Quantitative Information Flow (QIF), Random, and Scheduling (Clarke et al. 2001; Sinz, Kaiser, and K uchlin 2003; Palacios and Geffner 2009; Klebanov, Manthey, and Muise 2013). Footnote 1 refers to 'https://www.cs.rochester.edu/u/kautz/Cachet/' and Footnote 2 refers to 'http://www.cril.univ-artois.fr/KC/benchmarks.html'. |
| Dataset Splits | No | The paper refers to using standard benchmarks for evaluation but does not specify explicit train/validation/test splits or their proportions. |
| Hardware Specification | Yes | On a Linux cluster with Xeon E5-2650v2 CPUs (2.60GHz), we run each combination of heuristics on each benchmark using a single core, 24 GB of memory, and a 10-second timeout. |
| Software Dependencies | No | We implement Algorithm 1 using the ADD package CUDD to produce ADDMC, a new weighted model counter. While CUDD is named, a specific version number is not provided for it or any other software dependency used for the experiments. |
| Experiment Setup | Yes | On a Linux cluster with Xeon E5-2650v2 CPUs (2.60GHz), we run each combination of heuristics on each benchmark using a single core, 24 GB of memory, and a 10-second timeout. ADDMC heuristic configurations are constructed from five clustering heuristics (Mono, BE-List, BE-Tree, BM-List, and BM-Tree) together with seven variable order heuristics (Random, MCS, Inv MCS, Lex P, Inv Lex P, Lex M, and Inv Lex M). |