• Classified by Research Topic • Sorted by Date • Classified by Publication Type •
A Scalable Approximate Model Counter.
Supratik Chakraborty, Kuldeep S. Meel and Moshe Y. Vardi.
In Proceedings of International Conference on Constraint Programming (CP), pp. 200–216, September 2013.
Selected for CP 25th Anniversary Volume
Propositional model counting (#SAT), i.e., counting the numberof satisfying assignments of a propositional formula, is a problem ofsignificant theoretical and practical interest. Due to the inherent complexityof the problem, approximate model counting, which counts thenumber of satisfying assignments to within given tolerance and confi-dence level, was proposed as a practical alternative to exact model counting.Yet, approximate model counting has been studied essentially onlytheoretically. The only reported implementation of approximate modelcounting, due to Karp and Luby, worked only for DNF formulas. A fewexisting tools for CNF formulas are bounding model counters; they canhandle realistic problem sizes, but fall short of providing counts withingiven tolerance and confidence, and, thus, are not approximate modelcounters.We present here a novel algorithm, as well as a reference implementation,that is the first scalable approximate model counter for CNF formulas.The algorithm works by issuing a polynomial number of calls to a SATsolver. Our tool, ApproxMC, scales to formulas with tens of thousandsof variables. Careful experimental comparisons show that ApproxMC reports,with high confidence, bounds that are close to the exact count,and also succeeds in reporting bounds with small tolerance and highconfidence in cases that are too large for computing exact model counts.
@inproceedings{CMV13b,
title={A Scalable Approximate Model Counter},
bib2html_dl_pdf={../Papers/CP2013.pdf},
code={https://bitbucket.org/kuldeepmeel/approxmc},
author={Chakraborty, Supratik and Meel, Kuldeep S. and Vardi, Moshe Y.},
booktitle=CP,
pages={200--216},
year={2013},
month=sep,
bib2html_rescat={Counting},
note={Selected for CP 25th Anniversary Volume},
bib2html_pubtype={Refereed Conference,Award Winner},
abstract={
Propositional model counting (#SAT), i.e., counting the number
of satisfying assignments of a propositional formula, is a problem of
significant theoretical and practical interest. Due to the inherent complexity
of the problem, approximate model counting, which counts the
number of satisfying assignments to within given tolerance and confi-
dence level, was proposed as a practical alternative to exact model counting.
Yet, approximate model counting has been studied essentially only
theoretically. The only reported implementation of approximate model
counting, due to Karp and Luby, worked only for DNF formulas. A few
existing tools for CNF formulas are bounding model counters; they can
handle realistic problem sizes, but fall short of providing counts within
given tolerance and confidence, and, thus, are not approximate model
counters.
We present here a novel algorithm, as well as a reference implementation,
that is the first scalable approximate model counter for CNF formulas.
The algorithm works by issuing a polynomial number of calls to a SAT
solver. Our tool, ApproxMC, scales to formulas with tens of thousands
of variables. Careful experimental comparisons show that ApproxMC reports,
with high confidence, bounds that are close to the exact count,
and also succeeds in reporting bounds with small tolerance and high
confidence in cases that are too large for computing exact model counts.
},
}
Generated by bib2html.pl (written by Patrick Riley with layout from Sanjit A. Seshia ) on Sun Apr 14, 2024 11:15:51