gsat-solver

Projet SPD Master 1 Artois 2018-2019

Arthur Brandao & Maxence Bacquet

Structure du projet

Le projet est divisé en deux dossiers, un pour chaque partie, nommés Partie_1 et Partie_2. Le dossier Partie_1 comporte 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

Chaque programme possèdent sont makefile. Ces 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 affichent 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 (optionnel, par défaut 4)
• -s : Active le mode silencieux seule la satisfaisabilité (ou non) est affichée (optionnel)
• -m int : Le nombre maximum d'itérations avant l'arrêt du programme (optionnel)

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

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 [-t int]

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 (optionnel, par défaut 4)

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 (optionnel, par défaut 4)
• -s : Active le mode silencieux seule la satisfaisabilité (ou non) est affichée (optionnel)
• -e double : Utilisation de l'epsilon greedy avec la valeur donnée. La valeur doit être comprise entre 0 et 1 sinon la valeur utilisée est 0.1 (optionnel)

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 à 0.2

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 (optionnel, par défaut 4)
• -s : Active le mode silencieux seule la satisfaisabilité (ou non) est affichée (optionnel)
• -e double : Utilisation de l'epsilon greedy avec la valeur donnée. La valeur doit être comprise entre 0 et 1 sinon la valeur utilisée est 0.1 (optionnel)
• -d : Utilisation d'un alpha dynamique qui évolue entre 0.4 et 0.6 (optionnel)

Exemple de commande (celle éxécutée par make start) :

./GSATSolver -i ../../benchmarks/uf150/uf150-099.cnf -t 4 -d -e 0.2