Répondre à la discussion
Affichage des résultats 1 à 9 sur 9

Sat solver




  1. #1
    wildelkhadra2

    Sat solver

    Bonjour à tous et bonne année.

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

    La description :

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

    Le code:

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

    -----

    Dernière modification par Jack ; 10/01/2018 à 12h21. Motif: Les pièces jointes ne doivent pas se situer sur un site externe.

  2. Publicité
  3. #2
    wildelkhadra2

    Re : Sat solver

    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
    Dernière modification par JPL ; 10/01/2018 à 23h43.

  4. #3
    polo974

    Re : Sat solver

    Citation Envoyé par wildelkhadra2 Voir le message
    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 ? ? ?
    Le mieux est l'ennemi du bien, et c'est bien mieux comme ça...


  5. #4
    wildelkhadra2

    Re : Sat solver

    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.

  6. #5
    wildelkhadra2

    Re : Sat solver

    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

  7. A voir en vidéo sur Futura
  8. #6
    wildelkhadra2

    Re : Sat solver

    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.

  9. #7
    pm42

    Re : Sat solver

    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.

  10. Publicité
  11. #8
    wildelkhadra2

    Re : Sat solver

    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.

  12. #9
    Ikhar84

    Re : Sat solver

    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...
    J'ai glissé Chef !