Discussion :

[hollys]

Bonjour,

Je suis confronté dans le cadre de mes études à un problème de satisfiabilité.
Pour le résoudre, je dois utiliser un SAT-SOLVER.
J'ai donc créer un programme qui traduit les conditions en variables booléennes, et je génère un fichier txt au format DIMACS.

Ce qui devrait ensuite être un jeu d'enfant me bloque complètement.
Il suffit maintenant de passer ce fichier à un solver pour que celui-ci propose une solution si elle existe.

Et là, problème... J'utilise Dev-C++ sous Windows et impossible de trouver comment faire marcher cette petite machine...
J'ai choisi Minisat (http://minisat.se/) que j'ai téléchargé.
J'ai essayé de le compiler et de l'exécuter en lui passant mon fichier en argument sans résultat.

Si quelqu'un a une expérience des SAT-SOLVER je serai ravi de la partager...

[ternel]

Commence par résoudre le premier problème:

Dev-c++ est une antiquité, qui n'utilise qu'un très vieux compilateur. Remplace le par code::blocks ou un équivalent.

Ensuite, précises nous la nature de tes soucis.
"Ma voiture ne marche pas", c'est moins causant que "j'ai beau tourné la clé, le moteur ne démarre pas"