Bonjour, cliquez-ici pour vous inscrire et participer au forum.
  • Login:



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

Sat solver

  1. wildelkhadra2

    Date d'inscription
    janvier 2018
    Messages
    4

    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 à 13h21. Motif: Les pièces jointes ne doivent pas se situer sur un site externe.
     


    • Publicité



  2. wildelkhadra2

    Date d'inscription
    janvier 2018
    Messages
    4

    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 ; 11/01/2018 à 00h43.
     

  3. polo974

    Date d'inscription
    février 2007
    Messages
    8 409

    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...
     

  4. wildelkhadra2

    Date d'inscription
    janvier 2018
    Messages
    4

    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.
     

  5. wildelkhadra2

    Date d'inscription
    janvier 2018
    Messages
    4

    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
     


    • Publicité




    • Publicité







Sur le même thème :


    301 Moved Permanently

    301 Moved Permanently


    nginx/1.2.1