Algorithms for Propositional Model Counting (bibtex)
by Marko Samer, Stefan Szeider
Abstract:
We present algorithms for the propositional model counting problem \#SAT. The algorithms are based on tree-decompositions of graphs associated with the given CNF formula, in particular primal, dual, and incidence graphs. We describe the algorithms in a coherent fashion that admits a direct comparison of their algorithmic advantages. We analyze and discuss several aspects of the algorithms including worst-case time and space requirements and simplicity of implementation. The algorithms are described in sufficient detail for making an implementation reasonably easy.
Reference:
Algorithms for Propositional Model CountingMarko Samer, Stefan SzeiderJournal of Discrete Algorithms (JDA), volume 8, number 1, pages 50-64, March 2010, Elsevier.
Bibtex Entry:
@article{SamSze09JDA,
  author = {Marko Samer and Stefan Szeider},
  title = {Algorithms for Propositional Model Counting},
  number = {1},
  month = {March},
  year = {2010},
  journal = {Journal of Discrete Algorithms (JDA)},
  pages = {50-64},
  publisher = {Elsevier},
  volume = {8},
  abstract = {We present algorithms for the propositional model counting problem \#SAT. The algorithms are based on tree-decompositions of graphs associated with the given CNF formula, in particular primal, dual, and incidence graphs. We describe the algorithms in a coherent fashion that admits a direct comparison of their algorithmic advantages. We analyze and discuss several aspects of the algorithms including worst-case time and space requirements and simplicity of implementation. The algorithms are described in sufficient detail for making an implementation reasonably easy.},
  issn = {1570-8667},
  doi = {10.1016/j.jda.2009.06.002}
}
Powered by bibtexbrowser