|
@@ -0,0 +1,193 @@
|
|
|
+#include <iostream>
|
|
|
+#include <stdlib.h>
|
|
|
+#include <stdio.h>
|
|
|
+#include "GSATThread.hpp"
|
|
|
+#include "color.h"
|
|
|
+
|
|
|
+/* --- Public --- */
|
|
|
+
|
|
|
+GSATThread::GSATThread(int _nbThread, int argc, char** argv) {
|
|
|
+ nbThread = _nbThread;
|
|
|
+ gsat = std::vector<GSAT*>(_nbThread);
|
|
|
+ time = std::vector<double>(_nbThread);
|
|
|
+ threads = std::vector<std::thread>(_nbThread);
|
|
|
+ for(int i = 0; i < _nbThread; i++) {
|
|
|
+ gsat[i] = new GSAT();
|
|
|
+ gsat[i]->setParameters(argc,argv);
|
|
|
+ gsat[i]->initialize();
|
|
|
+ time[i] = 0;
|
|
|
+ }
|
|
|
+}
|
|
|
+
|
|
|
+GSATThread::~GSATThread() {
|
|
|
+ for(int i = 0; i < nbThread; i++) {
|
|
|
+ delete gsat[i];
|
|
|
+ }
|
|
|
+}
|
|
|
+
|
|
|
+void GSATThread::useAverageMethod() {
|
|
|
+ cb.setMethod(MT_AVG);
|
|
|
+}
|
|
|
+
|
|
|
+void GSATThread::useEpsilonMethod(double epsilon) {
|
|
|
+ cb.setMethod(MT_EPS);
|
|
|
+ cb.setEpsilon(epsilon);
|
|
|
+}
|
|
|
+
|
|
|
+bool GSATThread::solve() {
|
|
|
+ return this->solve(true);
|
|
|
+}
|
|
|
+
|
|
|
+bool GSATThread::solve(bool verbose) {
|
|
|
+ end = false;
|
|
|
+ calcTime = 0;
|
|
|
+ //Lance Initialise
|
|
|
+ printf("--- Initialize ---------------------------------------------------------------------------\n");
|
|
|
+ this->initBandit(verbose);
|
|
|
+ //Si la reponse n'a pas été trouvé durant l'initialisation
|
|
|
+ if(!end) {
|
|
|
+ //Lance les bandit avec la méthode choisit
|
|
|
+ printf("--- Search -------------------------------------------------------------------------------\n");
|
|
|
+ this->runBandit(verbose);
|
|
|
+ }
|
|
|
+ //Resultat
|
|
|
+ if(verbose) {
|
|
|
+ printf("--- Result -------------------------------------------------------------------------------\n");
|
|
|
+ this->printResult();
|
|
|
+ }
|
|
|
+ return end;
|
|
|
+}
|
|
|
+
|
|
|
+void GSATThread::printResult() {
|
|
|
+ if(end) {
|
|
|
+ printf(GREEN "s SATISFIABLE\n" RESET);
|
|
|
+ } else {
|
|
|
+ printf(RED "NOT FOUND\n" RESET);
|
|
|
+ }
|
|
|
+ //printf("s %s\n",end?"SATISFIABLE":"NOT FOUND");
|
|
|
+ if(!end && calcTime == 0) {
|
|
|
+ //Si on à pas trouver
|
|
|
+ calcTime = gsat[0]->realTime() - time[0];
|
|
|
+ }
|
|
|
+ printf(YELLOW);
|
|
|
+ if(end) {
|
|
|
+ printf("c [thread:%2d][iteration:%5d][fill:%d][heuristic:%d]Satisfied clauses (begin: %d)(end:%d)\n",
|
|
|
+ result.threadId,
|
|
|
+ result.nbIteration,
|
|
|
+ result.heuristicFill,
|
|
|
+ result.heuristicSolve,
|
|
|
+ result.nbSatisfiedClausesFill,
|
|
|
+ result.nbSatisfiedClausesSolve);
|
|
|
+ }
|
|
|
+ printf("c real time : %.4f seconds\n", calcTime);
|
|
|
+ printf(RESET);
|
|
|
+}
|
|
|
+
|
|
|
+/* --- Private --- */
|
|
|
+
|
|
|
+void GSATThread::initBandit(bool verbose) {
|
|
|
+ threads.clear();
|
|
|
+ //Lance thread
|
|
|
+ for(int i = 0; i < nbThread; i++) {
|
|
|
+ time[i] = gsat[i]->realTime();
|
|
|
+ threads[i] = std::thread(&GSATThread::initThread, this, i, verbose);
|
|
|
+ }
|
|
|
+ //Attend resultat
|
|
|
+ for(int i = 0; i < nbThread; i++){
|
|
|
+ threads[i].join();
|
|
|
+ }
|
|
|
+}
|
|
|
+
|
|
|
+void GSATThread::runBandit(bool verbose) {
|
|
|
+ threads.clear();
|
|
|
+ //Lance thread
|
|
|
+ for(int i = 0; i < nbThread; i++) {
|
|
|
+ threads[i] = std::thread(&GSATThread::runThread, this, i, verbose);
|
|
|
+ }
|
|
|
+ //Attend resultat
|
|
|
+ for(int i = 0; i < nbThread; i++){
|
|
|
+ threads[i].join();
|
|
|
+ }
|
|
|
+}
|
|
|
+
|
|
|
+void GSATThread::initThread(int id, bool verbose) {
|
|
|
+ //Les threads vont jouer les bandits pour etablir les moyennes
|
|
|
+ bool solve = false;
|
|
|
+ while(!end && !solve && !cb.queueIsEmpty()){
|
|
|
+ //Recup le prochaine fill et heuristic à tester
|
|
|
+ fillAndHeuristic fah = cb.next();
|
|
|
+ //Calcul
|
|
|
+ solve = gsat[id]->start(fah.fill, fah.heuristic);
|
|
|
+ //Affiche
|
|
|
+ if(verbose) {
|
|
|
+ if(solve) {
|
|
|
+ printf(CYAN);
|
|
|
+ }
|
|
|
+ printf("c [thread:%2d][iteration:%5d][fill:%d][heuristic:%d]Satisfied clauses (begin: %d)(end:%d)\n",
|
|
|
+ id,
|
|
|
+ gsat[id]->getNbIterations(),
|
|
|
+ gsat[id]->getHeuristicFill(),
|
|
|
+ gsat[id]->getHeuristicSolve(),
|
|
|
+ gsat[id]->getNbSatisfiedClausesFill(),
|
|
|
+ gsat[id]->getNbSatisfiedClausesSolve());
|
|
|
+ if(solve) {
|
|
|
+ printf(RESET);
|
|
|
+ }
|
|
|
+ }
|
|
|
+ //Ajoute le resultat aux moyenne
|
|
|
+ cb.addFill(fah.fill, gsat[id]->getNbSatisfiedClausesFill());
|
|
|
+ cb.addHeuristic(fah.heuristic, gsat[id]->getNbSatisfiedClausesSolve());
|
|
|
+ }
|
|
|
+ //Si 1er arreter
|
|
|
+ if(!end && solve) {
|
|
|
+ end = true;
|
|
|
+ calcTime = gsat[id]->realTime() - time[id];
|
|
|
+ result.threadId = id;
|
|
|
+ result.nbIteration = gsat[id]->getNbIterations();
|
|
|
+ result.heuristicFill = gsat[id]->getHeuristicFill();
|
|
|
+ result.heuristicSolve = gsat[id]->getHeuristicSolve();
|
|
|
+ result.nbSatisfiedClausesFill = gsat[id]->getNbSatisfiedClausesFill();
|
|
|
+ result.nbSatisfiedClausesSolve = gsat[id]->getNbSatisfiedClausesSolve();
|
|
|
+ }
|
|
|
+}
|
|
|
+
|
|
|
+void GSATThread::runThread(int id, bool verbose) {
|
|
|
+ //Les threads vont jouer les bandits avec la méthode choisit
|
|
|
+ bool solve = false;
|
|
|
+ while(!end && !solve){
|
|
|
+ //Recup le prochaine fill et heuristic à tester
|
|
|
+ fillAndHeuristic fah = cb.next();
|
|
|
+ //Calcul
|
|
|
+ solve = gsat[id]->start(fah.fill, fah.heuristic);
|
|
|
+ //Affiche
|
|
|
+ if(verbose) {
|
|
|
+ if(solve) {
|
|
|
+ printf(CYAN);
|
|
|
+ }
|
|
|
+ printf("c [thread:%2d][iteration:%5d][fill:%d][heuristic:%d]Satisfied clauses (begin: %d)(end:%d)\n",
|
|
|
+ id,
|
|
|
+ gsat[id]->getNbIterations(),
|
|
|
+ gsat[id]->getHeuristicFill(),
|
|
|
+ gsat[id]->getHeuristicSolve(),
|
|
|
+ gsat[id]->getNbSatisfiedClausesFill(),
|
|
|
+ gsat[id]->getNbSatisfiedClausesSolve());
|
|
|
+ if(solve) {
|
|
|
+ printf(RESET);
|
|
|
+ }
|
|
|
+ }
|
|
|
+ //Ajoute le resultat aux moyenne
|
|
|
+ cb.addFill(fah.fill, gsat[id]->getNbSatisfiedClausesFill());
|
|
|
+ cb.addHeuristic(fah.heuristic, gsat[id]->getNbSatisfiedClausesSolve());
|
|
|
+ }
|
|
|
+ //Si 1er arreter
|
|
|
+ if(!end && solve) {
|
|
|
+ end = true;
|
|
|
+ calcTime = gsat[id]->realTime() - time[id];
|
|
|
+ result.threadId = id;
|
|
|
+ result.nbIteration = gsat[id]->getNbIterations();
|
|
|
+ result.heuristicFill = gsat[id]->getHeuristicFill();
|
|
|
+ result.heuristicSolve = gsat[id]->getHeuristicSolve();
|
|
|
+ result.nbSatisfiedClausesFill = gsat[id]->getNbSatisfiedClausesFill();
|
|
|
+ result.nbSatisfiedClausesSolve = gsat[id]->getNbSatisfiedClausesSolve();
|
|
|
+ }
|
|
|
+}
|