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