Exploiting Problem Structure for Solution Counting

This paper deals with the challenging problem of counting the number of solutions of a CSP, denoted #CSP. Recent progress have been made using search methods, such as BTD [15], which exploit the constraint graph Structure in order to solve CSPs. We propose to adapt BTD for solving the KSP problem. The resulting exact counting method has a worst-case time complexity exponential in a specific graph parameter, called tree-width. For problems with sparse constraint graphs but large tree-width, we propose an iterative method which approximates the number of Solutions by solving a partition of the set of constraints into a collection of partial chordal subgraphs. Its time complexity is exponential in the maximum clique size - the clique number - of the original problem, which call be much smaller than its tree-width. Experiments on CSP and SAT benchmarks shows the practical efficiency of our proposed approaches.