|
@@ -1,9 +1,126 @@
|
|
|
-# Projet SPD
|
|
|
+# Projet SPD Master 1 Artois 2018-2019
|
|
|
|
|
|
-Arthur Brandoa M1 S2 2018-2019
|
|
|
+**Arthur Brandao & Maxence Bacquet**
|
|
|
|
|
|
|
|
|
|
|
|
-## Bug
|
|
|
+## Structure du projet
|
|
|
|
|
|
-Aucun bug trouvé
|
|
|
+Le projet est divisé en deux dossiers, un pour chaque partie nommée Partie_1 et Partie_2. Le dossier Partie_1 comportes 3 sous-dossiers, et le dossier Partie_2 comporte 2 sous-dossiers. Chaque sous-dossier correspond à un programme avec son makefile pour la compilation et un ReadMe.txt pour rappeler ses commandes et son utilisation (qui est aussi décrite plus bas dans ce document). Le dossier benchmark à la racine du projet contient les fichiers cnf utilisés pour l'exécution des programmes.
|
|
|
+
|
|
|
+
|
|
|
+
|
|
|
+## Utilisation
|
|
|
+
|
|
|
+Tous les makefile ont 3 fonctionnalités communes :
|
|
|
+
|
|
|
+- `make` pour compiler le programme. L'exécutable généré se nommera toujours GSATSolver.
|
|
|
+- `make clean` pour supprimer le fichier exécutable et les .o
|
|
|
+- `make run` pour lancer le programme
|
|
|
+
|
|
|
+Certains makefile ont des commandes supplémentaires pour lancer le programme avec des options différentes. Le fichier ReadMe.txt de chaque programme indique l'utilité du programme, les commandes du fichier makefile, ainsi que la commande pour lancer le programme depuis le terminal avec les différents arguments possibles (de plus tous les programmes affiche leur liste d'arguments en cas de mauvaise utilisation).
|
|
|
+
|
|
|
+
|
|
|
+
|
|
|
+## Partie 1
|
|
|
+
|
|
|
+Les 3 sous-dossiers correspondent aux 3 versions (Multi threads, MPI, Hybride) du solveur SAT à réaliser pour cette partie.
|
|
|
+
|
|
|
+### Thread
|
|
|
+
|
|
|
+C'est le programme qui implémente un solveur SAT en multi threads. Il ne possède pas de commande spécifique dans le makefile. Le programme s'utilise avec la commande suivante :
|
|
|
+
|
|
|
+`./GSATSolver -i file.cnf [-t int] [-s] [-m int]`
|
|
|
+
|
|
|
+Les arguments sont les suivants :
|
|
|
+
|
|
|
+- -i file.cnf : Le chemin vers le fichier cnf à résoudre
|
|
|
+- -t int : Le nombre de threads à utiliser
|
|
|
+- -s : Active le mode silencieux seul la satisfaisabilité (ou non) est affiché
|
|
|
+- -m int : Le nombre maximum d'itération avant l'arret du programme
|
|
|
+
|
|
|
+Exemple de commande (celle exécutée par `make run`) :
|
|
|
+
|
|
|
+`./GSATSolver -i ../../benchmarks/uf150/uf150-099.cnf -t 4`
|
|
|
+
|
|
|
+### MPI
|
|
|
+
|
|
|
+C'est le programme qui implémente un solveur SAT en utilisant MPI.Il ne possède pas de commande spécifique dans le makefile. Le programme s'utilise avec la commande suivante :
|
|
|
+
|
|
|
+`mpirun -n ./GSATSolver int -i file.cnf`
|
|
|
+
|
|
|
+Les arguments sont les suivants :
|
|
|
+
|
|
|
+- -n int : Le nombre de processus à utiliser
|
|
|
+- -i file.cnf : Le chemin vers le fichier cnf à résoudre
|
|
|
+
|
|
|
+Exemple de commande (celle exécutée par `make run`) :
|
|
|
+
|
|
|
+`mpirun -n 4 ./GSATSolver -i ../../benchmarks/uf150/uf150-099.cnf`
|
|
|
+
|
|
|
+### Hybride
|
|
|
+
|
|
|
+C'est le programme qui implémente un solveur SAT utilsant MPI et du multi threads. Il ne possède pas de commande spécifique dans le makefile. Le programme s'utilise avec la commande suivante :
|
|
|
+
|
|
|
+`mpirun -n int ./GSATSolver -i file.cnf`
|
|
|
+
|
|
|
+Les arguments sont les suivants :
|
|
|
+
|
|
|
+- -n int : Le nombre de processus à utiliser
|
|
|
+- -i file.cnf : Le chemin vers le fichier cnf à résoudre
|
|
|
+- -t int : Le nombre de threads à utiliser
|
|
|
+
|
|
|
+Exemple de commande (celle exécutée par `make run`) :
|
|
|
+
|
|
|
+`mpirun -n 3 ./GSATSolver -i ../../benchmarks/uf150/uf150-099.cnf -t 2`
|
|
|
+
|
|
|
+
|
|
|
+
|
|
|
+## Partie 2
|
|
|
+
|
|
|
+Le 1er sous-dossier (Moyenne) utilise une moyenne classique pour le choix du fill et de l'heuristique et le 2nd sous-dossier (EMA) utilise lui une moyenne exponentielle glissante.
|
|
|
+
|
|
|
+### Moyenne
|
|
|
+
|
|
|
+Le programme implémente le principe des bandits manchots avec une moyenne classique, et en utilisant ou non un epsilon greedy. Le programme possède une commande spécifique dans son makefile :
|
|
|
+
|
|
|
+- `make epsilon` pour lancer le programme avec un epsilon greedy à 0.2
|
|
|
+
|
|
|
+Le programme se lance avec la commande suivante :
|
|
|
+
|
|
|
+`./GSATSolver -i file.cnf [-t int] [-s] [-e double]`
|
|
|
+
|
|
|
+Les arguments sont les suivants :
|
|
|
+
|
|
|
+- -i file.cnf : Le chemin vers le fichier cnf à résoudre
|
|
|
+- -t int : Le nombre de threads à utiliser
|
|
|
+- -s : Active le mode silencieux seul la satisfaisabilité (ou non) est affiché
|
|
|
+- -e double : Utilisation de l'epsilon greedy avec la valeur donné (la valeur doit être compirse entre 0 et 1 sinon la valeur utilisé est 0.1)
|
|
|
+
|
|
|
+Exemple de commande (celle exécutée par `make epsilon`) :
|
|
|
+
|
|
|
+`./GSATSolver -i ../../benchmarks/uf150/uf150-099.cnf -t 4 -e 0.2`
|
|
|
+
|
|
|
+### EMA
|
|
|
+
|
|
|
+Le programme implémente le principe des bandits manchots avec une moyenne exponentielle glissante, et en utilisant ou non un epsilon greedy. Par défaut le programme se lance avec un alpha statique (dont la valeur est 0.5). Le programme possède plusieurs commandes spécifiques dans son makefile :
|
|
|
+
|
|
|
+- `make epsilon` pour lancer le programme avec un epsilon greedy à 0.2
|
|
|
+- `make dynamic` pour lancer le programme avec un alpha dynamique sans epsilon greedy
|
|
|
+- `make start` pour lancer le programme avec un alpha dynamique avec epsilon greedy
|
|
|
+
|
|
|
+Le programme se lance avec la commande suivante :
|
|
|
+
|
|
|
+`./GSATSolver -i file.cnf [-t int] [-s] [-e double] [-d]`
|
|
|
+
|
|
|
+Les arguments sont les suivants :
|
|
|
+
|
|
|
+- -i file.cnf : Le chemin vers le fichier cnf à résoudre
|
|
|
+- -t int : Le nombre de threads à utiliser
|
|
|
+- -s : Active le mode silencieux seul la satisfaisabilité (ou non) est affiché
|
|
|
+- -e double : Utilisation de l'epsilon greedy avec la valeur donné (la valeur doit être compirse entre 0 et 1 sinon la valeur utilisé est 0.1)
|
|
|
+- -d : Utilisation d'un alpha dynamique qui évolue entre 0.4 et 0.6
|
|
|
+
|
|
|
+Exemple de commande (celle éxécuté par `make start`) :
|
|
|
+
|
|
|
+`./GSATSolver -i ../../benchmarks/uf150/uf150-099.cnf -t 4 -d -e 0.2`
|