Geodesic
Segmentation de la sériation pour la résolution de #SAT
Mathématiques informatique et sciences humaines, Tome 147 (1999), pp. 113-134

Voir la notice de l'article provenant de la source Numdam

Le problème général traité est celui de l’évaluation approchée du nombre de solutions d’une formule booléenne F sous forme normale conjonctive. En appliquant le principe «diviser pour résoudre», la méthode présentée permet de réduire de façon considérable la complexité algorithmique du problème. Elle est basée sur la segmentation d’une sériation établie sur la table d’incidence associée à F. Nous montrons, dans des cas aléatoires difficiles de génération d’une formule F, l’intérêt de la sériation et de sa meilleure coupure en deux parties connexes et de tailles comparables. De plus, nous définissons la notion d’indépendance en probabilité pour F. On propose ici et on valide théoriquement et par une vaste expérimentation la méthode.

We propose here a general method for approximating the number of solutions of a boolean formula in conjunctive normal form F. By applying the principle “divise to resolve”, this method reduces considerably the computational complexity. It is based on cutting a seriation established on an incidence data table associated with F. Moreover, the independence probability concept is finely exploited. Theoretical justification and intensive experimentation validate the proposed method.

Mots-clés : satisfiabilité, théorie de la complexité, dénombrement de solutions, problèmes #P-complets, classification, sériation
Keywords: satisfiability, complexity theory, counting, #P-complete problems, classification, seriation 
@article{MSH_1999__147__113_0,
     author = {Lerman, Isra\"el-C\'esar and Rouat, Val\'erie},
     title = {Segmentation de la s\'eriation pour la r\'esolution de {#SAT}},
     journal = {Math\'ematiques informatique et sciences humaines},
     pages = {113--134},
     publisher = {Ecole des hautes-\'etudes en sciences sociales},
     volume = {147},
     year = {1999},
     mrnumber = {1717096},
     language = {fr},
     url = {http://geodesic.mathdoc.fr/item/MSH_1999__147__113_0/}
}
TY  - JOUR
AU  - Lerman, Israël-César
AU  - Rouat, Valérie
TI  - Segmentation de la sériation pour la résolution de #SAT
JO  - Mathématiques informatique et sciences humaines
PY  - 1999
SP  - 113
EP  - 134
VL  - 147
PB  - Ecole des hautes-études en sciences sociales
UR  - http://geodesic.mathdoc.fr/item/MSH_1999__147__113_0/
LA  - fr
ID  - MSH_1999__147__113_0
ER  - 
%0 Journal Article
%A Lerman, Israël-César
%A Rouat, Valérie
%T Segmentation de la sériation pour la résolution de #SAT
%J Mathématiques informatique et sciences humaines
%D 1999
%P 113-134
%V 147
%I Ecole des hautes-études en sciences sociales
%U http://geodesic.mathdoc.fr/item/MSH_1999__147__113_0/
%G fr
%F MSH_1999__147__113_0
Lerman, Israël-César; Rouat, Valérie. Segmentation de la sériation pour la résolution de #SAT. Mathématiques informatique et sciences humaines, Tome 147 (1999), pp. 113-134. http://geodesic.mathdoc.fr/item/MSH_1999__147__113_0/