Pith. sign in

REVIEW 1 cited by

ADDMC: Weighted Model Counting with Algebraic Decision Diagrams

Not yet reviewed by Pith; the record is open.

Re-run · record.json Download PDF Read on arXiv ↗

This paper has not been read by Pith yet. Machine review is queued; the pith claim, tier, and objections will appear here once it completes.

SPECIMEN: schema-true, not a live event

T0 review · schema-true

One-sentence machine reading of the paper's core claim.

pith:XXXXXXXX · record.json · timestamp

arxiv 1907.05000 v2 pith:K5G7SQ7K submitted 2019-07-11 cs.LO cs.AIcs.DS

Jeffrey M. Dudek , Vu H. N. Phan , Moshe Y. Vardi This is my paper · ORCID
classification cs.LOcs.AIcs.DS
keywords addmcmodelalgebraicalgorithmcountingdecisiondiagramsexact
verification ladder T0 review T1 audit T2 compute T3 formal

Signed reviews

No signed human review yet.

0 comments
read the original 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.

Discussion (0). Continue with ORCID to comment.

Forward citations

Cited by 1 Pith paper

Reviewed papers in the Pith corpus that reference this work. Sorted by Pith novelty score. Full citation record

  1. On Symbolic Approaches for Computing the Matrix Permanent

    cs.DS 2019-08 conditional novelty 6.0 of 10

    An ADD-based symbolic Ryser algorithm computes permanents of dense and similar-row matrices up to size 70-80, outperforming CNF-based exact counters and explicit Ryser on these instances.

Pith tools