Solution counting for CSP and SAT with large tree-width - INRAE - Institut national de recherche pour l’agriculture, l’alimentation et l’environnement Accéder directement au contenu
Article Dans Une Revue Control Systems and Computers Année : 2011

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.
Fichier principal
Vignette du fichier
post-print_CSC_2011_vol.2_p_1.4-13_SDG&AF (241.7 Ko) Télécharger le fichier
Origine : Fichiers produits par l'(les) auteur(s)

Dates et versions

hal-02641929 , version 1 (28-05-2020)

Identifiants

  • HAL Id : hal-02641929 , version 1
  • PRODINRA : 166643

Citer

Aurélie Favier, Simon de Givry, Philippe Jégou. Solution counting for CSP and SAT with large tree-width. Control Systems and Computers, 2011, Vol. 2, pp.4-13. ⟨hal-02641929⟩
16 Consultations
8 Téléchargements

Partager

Gmail Facebook X LinkedIn More