Accéder directement au contenu Accéder directement à la navigation
Article dans une revue

Solution counting for CSP and SAT with large tree-width

Abstract : 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.
Liste complète des métadonnées

https://hal.inrae.fr/hal-02641929
Déposant : Migration Prodinra <>
Soumis le : jeudi 28 mai 2020 - 17:53:21
Dernière modification le : samedi 3 octobre 2020 - 03:28:51

Fichier

post-print_CSC_2011_vol.2_p_1....
Fichiers produits par l'(les) auteur(s)

Identifiants

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

Collections

Citation

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⟩

Partager

Métriques

Consultations de la notice

16

Téléchargements de fichiers

17