Algorithms for Propositional Model CountingJ. of Discrete Algorithms, vol. 8, no. 1, pp. 50-64, 2010. A preliminary and shortened version version of the paper appeared in the Proceedings of LPAR 2007, 14th International Conference on Logic for Programming Artificial Intelligence and Reasoning, Yerevan, Armenia, October 15-19, 2007. Lecture Notes in Computer Science, vol. 4790, pp. 484-498, Springer, 2007. Abstract:We present algorithms for the propositional model counting problem #SAT. The algorithms utilize tree decompositions of certain graphs associated with the given CNF formula; in particular we consider primal, dual, and incidence graphs. We describe the algorithms coherently for a direct comparison and with sufficient detail for making an actual implementation reasonably~easy. We discuss several aspects of the algorithms including worst-case time and space requirements.Download: [paper pdf] |