Solution counting for CSP and SAT with large tree-width
Résumé
This paper deals with the challenging problem of counting the number of solutions of a CSP, denoted #CSP. Recent progress has been made using search methods, such as Backtracking with Tree-Decomposition (BTD) [J´egou and Terrioux, 2003], which exploit the constraint graph structure in order to solve CSPs. We propose to adapt BTD for solving the #CSP problem. The resulting exact counting method has a worst-case time complexity exponential in a specific graph parameter, called tree-width. For problems with a sparse constraint graph but a 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 can be much smaller than its tree-width. Experiments on CSP and SAT benchmarks show the practical efficiency of our proposed approaches1.
Origine : Fichiers produits par l'(les) auteur(s)