Variable Elimination Algorithm for Model Counting for #SAT.

This paper presents a new algorithm to solve the model counting problem for boolean formulas (#SAT), together with an analysis of its time and space complexity. The algorithm features novel techniques based on a simple framework of manipulating layers, which are essentially arrays of model counts. It is distinguished from other existing approaches to #SAT that are mostly based on DPLL, and this non-DPLL framework suggests many advantages for real-world applications. Its time complexity matches the best one currently achievable with other proposed algorithms, specifically, the upper bound of 0(n · 2"), where w is the induced width of the underlying variable graph. To highlight the practicality of our new algorithm, we also present a preliminary research on industrial SAT examples and suggest prospective areas for real-world applications. [ABSTRACT FROM AUTHOR]