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

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

Mathématiques informatique et sciences humaines, Tome 147 (1999), pp. 113-134.

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.

Mot clés : satisfiabilité, théorie de la complexité, dénombrement de solutions, problèmes #P-complets, classification, sériation
Mots clés : satisfiability, complexity theory, counting, #P-complete problems, classification, seriation

[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 | Zbl

[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

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

[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

[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 | Zbl

[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 | Zbl

[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 | Zbl

[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

[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

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

[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

[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 | Zbl