Mathématiques et sciences humaines/Mathematics and social sciences

n° 147, Automne 1999, spécial Classification

Version imprimable   Signaler cette page  

Segmentation de la sériation pour la résolution de ­ #SAT

Cutting seriation for approximate #SAT resolution

Israël-césar Lerman et Valérie Rouat

Résumé

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.

Abstract

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.

Index

Pour citer cet article

Israël-césar Lerman et Valérie Rouat, « Segmentation de la sériation pour la résolution de ­ #SAT », Mathématiques et sciences humaines, n° 147, Automne 1999, spécial Classification, [En ligne], mis en ligne le 10 février 2006. URL : http://msh.revues.org/document2793.html. Consulté le 28 novembre 2009.

 
Page générée par Lodel - Nous adhérons à www.revues.org

ISSN : 0987 6936
Ecole des hautes études en sciences sociales