Sat solver

[wildelkhadra2]

Bonjour à tous et bonne année.

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

La description :

################ Lien supprimé

Le code:

################ Lien supprimé
-----

[wildelkhadra2]

Bonsoir,
Je vous laisse le code et une petite doc qui explique la méthodologie.

Pièce jointe supprimée : le zip n’est pas lisible.

algo.pdf

[polo974]

Bonjour à tous et bonne année.

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

Description succincte (en 2 ou 3 lignes sans passer par un pdf) ? ?

Dans quel but ? ? ?

[wildelkhadra2]

Bonsoir,

Je tente une dernière fois de mettre la pj.

NewSat.zip


Le but de ce poste est de partager et d'avoir des avis sur une recherche modeste.


L'idée comme dit dans le pdf est de partir d'une instance de 2In3Sat ( exactement deux true sur 3) et de faire les choses suivantes:
1) de l'instance on généré un système 2Sat.
2) ON procède à une analyse logique de ce système (2Sat) en supposant que le système de départ contient une solution( valide).
cette analyse permet d'avoir des informations sur les variables ( assigner de valeurs ou égalité entre variables ).
3) Si on n'a pas de contradiction à ce niveau on utilise l'algo de Tarjan pour trouver un solution de 2Sat simplifié.
4) Si 2Sat simplifié est invalide on arrête sinon la solution donnée par Tarjan va subir un nouveau traitement ( on se déplace dans l'ensemble des solutions ) pour transformer les clauses qui ont eu une assignation 111 par Tarjan en des assignations 110, 011 ou 101.


Si vous avez des questions , n'hésitez pas.
Bonne nuit.

[A voir en vidéo sur Futura]

[wildelkhadra2]

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

[wildelkhadra2]

Bonjour;

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

Je posterai d'ici demain la nouvelle version du code et la doc explicative du solver , cette nouvelle version s'appuie pour le moment sur une conjecture , avis aux volontaire pour m'aider à la démontrer ou à trouver un contre-exemple .

Je donnerai toutes les infos possibles aux volontaires 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èmes 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 24000 et 120000 variables distinctes dans les deux jeux de tests.

[pm42]

Ici, c'est un forum, pas un blog.
Si on regarde le fil, on a un peu l'impression que tu te parles à toi même.

De plus, ton sujet étant quand même un peu spécialisé (euphémisme) comparé aux autres questions qui sont habituellement posées dans la rubrique "programmation" de FS, je me demande s'il est à sa place.

[wildelkhadra2]

Salut,

je suis en monologue faute de volontaires pour avoir un échange
Ce n'est pas grave , je vous laisse tranquilles .

Ceux qui s'intéressent au sujet trouveront sans problème mon blog.

Bonne journée.

[Ikhar84]

Bonjour!
Ce n'est pas que le sujet n'est pas interressant, mais on n'est pas dans le cadre d'une demande d'aide, mais dans de l'auto-promotion dans un domaine bien spécialisé quand même.
De plus les pièces jointes en zip n'aident pas forcément à appâter les curieux, il vaut mieux déposer le code entre les bonnes balises et les autres documents directement accessible, pour ceux qui, comme moi, sont souvent en mobilité et utilisent l'appli mobile...