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

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

Mathématiques et Sciences Humaines (1999)

  • Volume: 147, page 113-134
  • ISSN: 0987-6936

Abstract

top
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.

How to cite

top

Lerman, Israël-César, and Rouat, Valérie. "Segmentation de la sériation pour la résolution de #SAT." Mathématiques et Sciences Humaines 147 (1999): 113-134. <http://eudml.org/doc/94528>.

@article{Lerman1999,
abstract = {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.},
author = {Lerman, Israël-César, Rouat, Valérie},
journal = {Mathématiques et Sciences Humaines},
keywords = {satisfiability; complexity theory; counting; #P-complete problems; classification; seriation},
language = {fre},
pages = {113-134},
publisher = {Ecole des hautes-études en sciences sociales},
title = {Segmentation de la sériation pour la résolution de #SAT},
url = {http://eudml.org/doc/94528},
volume = {147},
year = {1999},
}

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 et Sciences Humaines
PY - 1999
PB - Ecole des hautes-études en sciences sociales
VL - 147
SP - 113
EP - 134
AB - 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.
LA - fre
KW - satisfiability; complexity theory; counting; #P-complete problems; classification; seriation
UR - http://eudml.org/doc/94528
ER -

References

top
  1. [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. Zbl0398.68042MR526451
  2. [2] Bailleux ( O.) et Chabrier ( J.J.). - Counting by statistics on search trees: Application to constraint satisfaction problems. Intelligent Data Analysis, 1997. 
  3. [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. Zbl0253.68020
  4. [4] Dubois ( O.). - Counting the number of solutions for instances of satisfiability. Theoretical Computer Science, no81, 1991, pp. 49-64. Zbl0725.68045MR1103098
  5. [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. [6] Lassaigne ( R.) et de Rougemont ( M.). - Logique et complexité. - Hermes, 1996. Zbl0847.68035
  7. [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. [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. Zbl0243.62040MR303795
  9. [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. Zbl0448.62039MR547264
  10. [10] Lerman ( I.-C.). - Cartesian and Statistical Approaches of the Satisfiability Problem. - rapport de recherche Inria n° 1685, Irisa, mai 1992. 
  11. [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. [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. [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. [14] Lozinskii ( E.L.). - Counting propositional models. Information Processing Letters, no41, avril 1992, pp. 327-332. Zbl0780.68065MR1163045
  15. [15] Marcotorchino ( F.). - Block seriation problems: a unified approach. Applied Stochastic Models and Data Analysis, vol. 3, n° 2, juin 1987, pp. 73-91. Zbl0624.90048
  16. [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. MR1175183
  17. [17] Papadimitriou ( C.H.). - Computational complexity. - Addison Wesley, 1994. Zbl0833.68049MR1251285
  18. [18] Pearson ( K.). - Notes on the history of corrélation. Biometrika, no13, 1920, pp. 25-45. 
  19. [19] Roth ( D.). - On the hardness of approximate reasoning. Artificial Intelligence, no82, 1996, pp. 273-302. MR1391064
  20. [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. [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. [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. [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. [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. [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. Zbl0419.68082MR539258

NotesEmbed ?

top

You must be logged in to post comments.

To embed these notes on your page include the following JavaScript code on your page where you want the notes to appear.

Only the controls for the widget will be shown in your chosen language. Notes will be shown in their authored language.

Tells the widget how many notes to show per page. You can cycle through additional notes using the next and previous controls.

    
                

                
Note: Best practice suggests putting the JavaScript code just before the closing </body> tag.