Discussion :

[wildelkhadra]

Bonjour à tous et bonne année.

Je vous présente un petit algo : un sat solver.

La description :

http://wild-elkhadra.e-monsite.com/pages/page.html

Le code:

http://wild-elkhadra.e-monsite.com/p...lver-code.html



Il y a un test simple:
1) Créer un projet Console.
2) Copier-coller le code dans 1 ou 3 fichiers différents.
3) Compiler et lancer.

Sinon pour les volontaires et comme les ratio nombre de variables / nombre des clauses réduit ou augmeNTE l'espace des solutions possibles . Il faut choisir des valeurs > 3 , =3 et < 3 et regarder le comportement de l'algo
tests fait jusqu'a nombres variables =6000 et nombre clauses = 2000.

[wildelkhadra]

Bonsoir,
Pas de volontaires , pas de questions .Ok .Je vous donne quand-même la suite:
1) Publier l'algo et le code ailleurs.
2) Le prolonger par deux extensions:
a) coder la conversion 3SAT==> 1In3SAT=>2In3SAT ( facile).
b) Coder la conversion FAC to SAT et l'utiliser pour factoriser les nombres ( un peu plus compliqué).

Je vous tiens au courant ASAP

[wildelkhadra]

Bonjour;

J'ai fait quelques modifications sur l'algo et le code suite au tests .

Vous trouverez sur le site le nouveau solver qui s'appuie pour le moment sur une conjoncture , avis aux volontaire pour m'aider à la démontrer ou à trouver un contre-exemple .

Je donnerai toutes les infos possible par mail ou ici.

Pour les derniers tests j'ai résolu des système 2in3sat avec des inputs de 10000 clauses et 30000 variables en 10 minutes sur un simple portable monocore et des système de 50000 clauses et 150000 variables en 7 heures sur une machine à 4 cores
à Vrai dire comme j'utilise un random pour générer les systèmes il y a environ 12000 et 120000 variables distincts dans les deux jeux de tests.

[wildelkhadra]

désolé , il faut lire conjecture au lieu de conjoncture.

[Ry0_Saeba]

Bonjour,

Je suis peut-être mauvais mais il me semble que l'accès à la page affichant le code est bloqué ^^'



Par ailleurs, sauriez-vous comment faire ce type de projet en langage C ? avec par exemple une lecture de fichier dans lequel le valeurs sont présentes (A, !A, ...) ? Car j'essaye d'apprendre le langage C ,et on m'a conseillé ce type de projet pour commencer.

Merci par avance,

R.S.

[dourouc05]

on m'a conseillé ce type de projet pour commencer.

Je ne sais pas qui est ce "on", mais il/elle doit avoir des neurones grillés en nombre . Déjà, la lecture de fichier de ce genre n'est pas aussi simple que cela (mieux vaut commencer par des formats de fichier assez fixes — juste une série de nombres, exactement ceux qu'on attend, comme les trente-six paramètres d'une simulation numérique —, puis légèrement variables — type CSV — avant d'attaquer de petites grammaires). Ensuite, d'un point de vue algorithmique, SAT n'est pas la chose la plus simple à prendre en main… Je te dirais plutôt de faire un tour sur https://c.developpez.com/cours/ .