Des générateurs... - Githubissues

yhamoudi commented 10 years ago

J'ai commencé l'implémentation de 2 générateurs : pour tseitin et color. Leurs codes figurent dans gen.ml (en bas du fichier, en commenté). Je ne sais pas encore comment faire évoluer le générateur global pour prendre en compte ces 3 générateurs. On fait un truc identique à ce qu'on a pour les algos (un fichier de config avec parsage des arguments, puis un fichier par générateur) ?

ilsordo commented 10 years ago

Je ne les vois pas, tu as bien commit?

yhamoudi commented 10 years ago

J'ai structuré un peut tout ça. Maintenant, il y a 3 façons d'appeler gen :

./gen -cnf n l k : génère une cnf avec paramètres n l k
./gen -tseitin n c : génère une formule avec paramètres n c
./gen -color n p : génère un graphe avec paramètres n p

Du coup on a plus le format ./gen n l k (il faut maintenant ajouter n l k). On peut peut-être le rétablir avec un fichier bash ?

Autre point : la méthode utilisée actuellement des graphes ne permet pas de savoir à l'avance cmb d'arêtes il va y avoir. Deux possibilités :

il faut stocker qq part le graphe en court de construction pour pouvoir l'afficher un fois qu'on connait le nb d'arêts
on indique toujours 0 arêtes car notre algo ne s'appuie pas sur le nb d'arêtes

ilsordo commented 10 years ago

On peut laisser tel quel pour les graphes, si il faut changer ce sera pas très compliqué de toute manière.

yhamoudi commented 10 years ago

ok juste pour préciser la syntaxe actuelle : ./gen n l k ./gen tseitin n c : génère une formule avec n variables et c connecteurs ./gen color n p : génère un graphe avec n sommets et proba p pour chaque arête

ilsordo commented 10 years ago

Ok, j'ai mis des - (-tseitin) dans le main, tu peux changer si tu veux

ilsordo / SAT-SMT-Solver

Des générateurs... #9