DOI: 10.5176/2251-2179_ATAI12.10
Authors: Chanseok Oh
Abstract: 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 O(n ∙ 2w), 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.
Keywords: model counting; variable elimination; #SAT; sharp SAT; propositional satisfiability; boolean satisfiability
Updating...