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

Lerman, Israël-César ; Rouat, Valérie

Mathématiques et Sciences humaines, Tome 147 (1999), p. 113-134 / Harvested from Numdam

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.

Détail

Publié le : 1999-01-01

MR 1717096

Mots clés: satisfiabilité, théorie de la complexité, dénombrement de solutions, problèmes #P-complets, classification, sériation

Bibliographie

[1] Aspvall (B.), Plass (M.F.) et Tarjan (R.E.). - A linear-time algorithm for testing the truth of certain quantified boolean formulas. Information Processing Letters, vol. 8, n° 3, mars 1979, pp. 121-123. | MR 526451 | Zbl 0398.68042

[2] Bailleux (O.) et Chabrier (J.J.). - Counting by statistics on search trees: Application to constraint satisfaction problems. Intelligent Data Analysis, 1997.

[3] Cook (S.A.). - The complexity of theorem-proving procedures. In : 3rd Annual ACM Symposium on the Theory of Computing, éd. par ACM, pp. 151-158.- New-York, 1971. | Zbl 0253.68020

[4] Dubois (O.). - Counting the number of solutions for instances of satisfiability. Theoretical Computer Science, no81, 1991, pp. 49-64. | MR 1103098 | Zbl 0725.68045

[5] Karp (R.M.) et Luby (M.). - Monte-carlo algorithms for enumeration and reliability problems. In : 24th IEEE Symposium of Foundations of Computer Science, pp. 56-64. - 1983.

[6] Lassaigne (R.) et De Rougemont (M.). - Logique et complexité. - Hermes, 1996. | Zbl 0847.68035

[7] Leredde (H.). - La méthode des pôles d'attraction, la méthode des pôles d'agrégation; deux nouvelles familles d'algorithmes en classification automatique et sériation. - Thèse de 3e cycle, Université de Paris VI, octobre 1979.

[8] Lerman (I.-C.). - Analyse du phénomène de la "sériation" à partir d'un tableau d'incidence. Mathématiques et Sciences Humaines, no38, 1972, pp. 39-57. | Numdam | MR 303795 | Zbl 0243.62040

[9] Lerman (I.-C.). - Croisement de classifications floues. Publication de l'institut statistique des universités de Paris, vol. XXIV, n° 1-2, 1979, pp. 13-46. | MR 547264 | Zbl 0448.62039

[10] Lerman (I.-C.). - Cartesian and Statistical Approaches of the Satisfiability Problem. - rapport de recherche Inria n° 1685, Irisa, mai 1992.

[11] Lerman (I.-C.)- Statistical reduction of the satisfiability problem by means of a classification method. Data Science and its Application, 1995, pp. 219-234.

[12] Lerman (I.-C.), Peter (P.) et Leredde (H.). - Principes et calculs de la méthode implantée dans le programme CHAVL (classification hiérarchique par analyse de la vraisemblance des liens) 1ère partie. La revue de Modulad, no12, décembre 1993, pp. 33-70.

[13] Lerman (I.-C.) et Rouat (V.). - Une résolution approchée du problème #SAT par un algorithme de sériation. In : Cinquièmes Rencontres de la Société Francophone de Classification, pp. 29-34. - Lyon, septembre 1997.

[14] Lozinskii (E.L.). - Counting propositional models. Information Processing Letters, no41, avril 1992, pp. 327-332. | MR 1163045 | Zbl 0780.68065

[15] Marcotorchino (F.). - Block seriation problems: a unified approach. Applied Stochastic Models and Data Analysis, vol. 3, n° 2, juin 1987, pp. 73-91. | Zbl 0624.90048

[16] Mitchell (D.), Selman (B.) et Levesque (H.). - Hard and easy distributions of SAT problems. In : Tenth National Conférence on Artificial Intelligence (AAAI-92), pp. 459-465. - San Jose, 1992. | MR 1175183

[17] Papadimitriou (C.H.). - Computational complexity. - Addison Wesley, 1994. | MR 1251285 | Zbl 0833.68049

[18] Pearson (K.). - Notes on the history of corrélation. Biometrika, no13, 1920, pp. 25-45.

[19] Roth (D.). - On the hardness of approximate reasoning. Artificial Intelligence, no82, 1996, pp. 273-302. | MR 1391064

[20] Rouat (V.). - Validité de l'approche classification dans la réduction statistique de la complexité de #SAT. - Thèse de doctorat, Université de Rennes1, janvier 1999.

[21] Rouat (V.) et Lerman (I.-C.). - Utilisation de la sériation pour une résolution approchée du problème #SAT. In: JNPC'97, résolution pratique de problèmes NP-complets, pp. 55-60. - Rennes, avril 1997.

[22] Rouat (V.) et Lerman (I.-C.). - Problématique de la coupure dans la résolution de #SAT par sériation. In: JNPC'98, résolution pratique de problèmes NP-complets, pp. 109-114. - Nantes, mai 1998.

[23] Simon (J.C.) et Dubois (O.). - Number of solutions of satisfiability instances- applications to knowledge bases. International Journal of Pattern Recognition and Artificial Intelligence, vol. 3, n° 1, 1989, pp. 53-65.

[24] Toda (S.). - On the computational power of PP and ⊕P. In: 30th Annual Symposium on Foundations of Computer Science, pp. 514-519. - 1989.

[25] Valiant (L.G.). - The complexity of enumeration and reliability problems. SIAM Journal on Computing, vol. 8, n° 3, août 1979, pp. 410-421. | MR 539258 | Zbl 0419.68082