Un petit solveur SAT

**wildelkhadra** · 10/01/2018, 21h30

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** · 15/01/2018, 23h07

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** · 02/04/2018, 17h40

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** · 02/04/2018, 21h04

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

**Ry0_Saeba** · 15/11/2018, 13h34

Bonjour,

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

Nom : img.png
Affichages : 569
Taille : 9,9 Ko

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** · 15/11/2018, 15h41

Envoyé par Ry0_Saeba

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/

.

**Ry0_Saeba** · 15/11/2018, 15h47

Ce "on" c'est mon prof d'info,

Car ayant fait un BTS systèmes et réseaux, et comme je suis entré dans des études en dev, j'ai pas beaucoup de connaissance, (principalement java et C), et je dois savoir faire ce genre de projet pour tenir les partiels et rattraper mon retard de niveau

.

Merci pour le lien, cela me sera très utile je pense

**wildelkhadra** · 22/11/2018, 13h14

Bonjour et je suis désolé pour le retard.

Comme on vous a dit SAT n'est pas le problème le plus facile pour commencer à programmer mais rien n’empêche d’essayer...::

Pour les langages informatiques , le c est en train de devenir un langage ésotérique et il vaut mieux commencer par c# , java ou c++ 11 , cela donne plus de facilité et d'ouverture sur le monde du travail.

Il vaut mieux aussi commencer par manipuler des structures basiques comme les listes , les maps , les arbres et les bases du langage ( récursivité , if then else , swittch,for , foreach....) avant de passer à la programmation OO ou async...

J'ai fait une mise à jour de la doc et du code ( il y a un cas logique que je n'ai vu dans l'analyse logique ) que je reposerai ASAP sur le site ..

**anapurna** · 22/11/2018, 16h43

salut

dis moi si j'ai bien compris tu est en train de travailler sur un solveur boolean
tes variables ne peuvent être que vrai ou faux

cela me fait penser furieusement a de l’algèbre de boole et ses tables de vérité

a	b	a ET b	a OU b	a OUex b	NON(a ET b)	NON(a OU b)	NON(a OUex b)	NON a	NON b	(NON a) ET b	a ET (NON b)	(NON a) OU b	a OU (NON b)
0	0	0	0	0	1	1	1	1	1	0	0	1	1
0	1	0	1	1	1	0	0	1	0	1	0	1	0
1	0	0	1	1	1	0	0	0	1	0	1	0	1
1	1	1	1	0	0	0	1	0	0	0	0	1	1

tu peux remplacer les 0 par vrai et 1 par faux cela ne change rien a la logique
pour ce faire j'utiliserais un graphe dans lesquel les feuille serais le valeurs et les nœud les operateur et contient aussi le resultat

exemple
imaginons a =1 , b= 0, c=1

			Not(0)
		\|(1)
	&(0)		c(1)
a(1)		b(0)

**wildelkhadra** · 01/12/2018, 21h05

Bonjour,

Je ne vois pas comment on peut utiliser votre arbre pour trouver une solution de 3SAT.

J'ai fait une mise à jour de la doc :

http://wild-elkhadra.e-monsite.com/p...se-a-jour.html

**dourouc05** · 01/12/2018, 22h05

Envoyé par wildelkhadra

Je ne vois pas comment on peut utiliser votre arbre pour trouver une solution de 3SAT.

L'objectif de 3SAT, c'est de trouver une assignation de valeurs aux variables pour rendre la formule vraie. Tu as, par exemple, un arbre binaire : à la racine, tu choisis une variable ; dans le premier fils, tu l'imposes à zéro, dans l'autre à un. Dès que tu vois qu'il n'y a pas moyen de satisfaire la formule dans une branche à cause du choix de valeurs, alors il n'y a plus besoin de l'explorer.

**wildelkhadra** · 01/12/2018, 23h50

Je vois mieux mais et sauf erreur de ma part votre approche est exponentielle.
L'enjeu est de trouver un algo polynomial.

**dourouc05** · 03/12/2018, 03h29

Sauf qu'il n'en existe aucun actuellement et qu'il est très probable qu'on n'en trouve jamais

.

**anapurna** · 03/12/2018, 14h44

salut

il est peut être possible d'appliquer les lois de Morgan sur l'arbre binaire afin de simplifier les formules
mais de toutes les manières la simplification passera forcement par le parcourt de toutes les feuilles d'arbres pertinentes

**wildelkhadra** · 03/12/2018, 23h13

Bonjour,

Si le sujet vous intéresse l'un des meilleurs solvers aujourd’hui est CDCL

https://en.wikipedia.org/wiki/Confli...lause_learning

**wildelkhadra** · 29/12/2019, 23h43

Bonjour,

J'ai mis en place une nouvelle approche qui consiste à transformer le problème 2In3SAT en un NAE3SAT ( not all equal ) qui est dans P dans le cas planaire.

Pour le NAE :

https://en.wikipedia.org/wiki/Not-al...satisfiability

La nouvelle approche:

http://wild-elkhadra.e-monsite.com/pages/sat-est-p.html

Bonne lecture et bonnes fêtes.

Un petit solveur SAT

Contribuez

Discussions similaires

Partager

Partager