Segmentation de la sériation pour la résolution de #SAT
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 i...
Gorde:
| Argitaratua izan da: | URI:https://journals.openedition.org/msh, |
|---|---|
| Egile Nagusiak: | , |
| Formatua: | Article ou chapitre numérique |
| Hizkuntza: | Français |
| Argitaratua: |
Mathématiques et sciences humaines
2006
|
| Gaiak: | |
| Sarrera elektronikoa: | Accès Université d'Orléans et IFPM Accès Université d'Orléans et IFPM |
| Gaia: | 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. |
|---|