GSATThread.cpp 5.0 KB

123456789101112131415161718192021222324252627282930313233343536373839404142434445464748495051525354555657585960616263646566676869707172737475767778798081828384858687888990919293949596979899100101102103104105106107108109110111112113114115116117118119120121122123124125126127128129130131132133134135136137138139140141142143144145146147148149150151152153154155156157158159160161162163164165166167168169170171172173174175176177178179180181182183184185186187188189
  1. #include <iostream>
  2. #include <stdlib.h>
  3. #include <stdio.h>
  4. #include "GSATThread.hpp"
  5. #include "color.h"
  6. /* --- Public --- */
  7. GSATThread::GSATThread(int _nbThread, int argc, char** argv) {
  8. nbThread = _nbThread;
  9. gsat = std::vector<GSAT*>(_nbThread);
  10. time = std::vector<double>(_nbThread);
  11. threads = std::vector<std::thread>(_nbThread);
  12. for(int i = 0; i < _nbThread; i++) {
  13. gsat[i] = new GSAT();
  14. gsat[i]->setParameters(argc,argv);
  15. gsat[i]->initialize();
  16. time[i] = 0;
  17. }
  18. }
  19. GSATThread::~GSATThread() {
  20. for(int i = 0; i < nbThread; i++) {
  21. delete gsat[i];
  22. }
  23. }
  24. void GSATThread::useAverageMethod() {
  25. cb.setMethod(MT_AVG);
  26. }
  27. void GSATThread::useEpsilonMethod(double epsilon) {
  28. cb.setMethod(MT_EPS);
  29. cb.setEpsilon(epsilon);
  30. }
  31. bool GSATThread::solve() {
  32. return this->solve(true);
  33. }
  34. bool GSATThread::solve(bool verbose) {
  35. this->end(false);
  36. calcTime = 0;
  37. //Lance Initialise
  38. printf("--- Initialize --------------------------------------------------------------------------\n");
  39. this->initBandit(verbose);
  40. //Si la reponse n'a pas été trouvé durant l'initialisation
  41. if(!this->isEnd()) {
  42. //Lance les bandit avec la méthode choisit
  43. printf("--- Search ------------------------------------------------------------------------------\n");
  44. this->runBandit(verbose);
  45. }
  46. //Resultat
  47. if(verbose) {
  48. printf("--- Result ------------------------------------------------------------------------------\n");
  49. this->printResult();
  50. }
  51. return this->isEnd();
  52. }
  53. void GSATThread::end() {
  54. this->end(true);
  55. }
  56. void GSATThread::end(bool endOrNot) {
  57. std::lock_guard<std::mutex> guard(mEnd);
  58. bEnd = endOrNot;
  59. }
  60. bool GSATThread::isEnd() {
  61. std::lock_guard<std::mutex> guard(mEnd);
  62. return bEnd;
  63. }
  64. void GSATThread::printResult() {
  65. if(this->isEnd()) {
  66. printf(GREEN "s SATISFIABLE\n" RESET);
  67. } else {
  68. printf(RED "NOT FOUND\n" RESET);
  69. }
  70. if(!this->isEnd() && calcTime == 0) {
  71. //Si on à pas trouver
  72. calcTime = gsat[0]->realTime() - time[0];
  73. }
  74. printf(YELLOW);
  75. printf("c real time : %.4f seconds\n", calcTime);
  76. if(this->isEnd()) {
  77. printf("c [thread:%2d][iteration:%4d][fill:%d][heuristic:%d]Satisfied clauses (begin: %d)(end:%d)\n",
  78. result.threadId,
  79. result.nbIteration,
  80. result.heuristicFill,
  81. result.heuristicSolve,
  82. result.nbSatisfiedClausesFill,
  83. result.nbSatisfiedClausesSolve);
  84. }
  85. printf(RESET);
  86. }
  87. /* --- Private --- */
  88. void GSATThread::initBandit(bool verbose) {
  89. threads.clear();
  90. //Lance thread
  91. for(int i = 0; i < nbThread; i++) {
  92. time[i] = gsat[i]->realTime();
  93. threads[i] = std::thread(&GSATThread::initThread, this, i, verbose);
  94. }
  95. //Attend resultat
  96. for(int i = 0; i < nbThread; i++){
  97. threads[i].join();
  98. }
  99. }
  100. void GSATThread::runBandit(bool verbose) {
  101. threads.clear();
  102. //Lance thread
  103. for(int i = 0; i < nbThread; i++) {
  104. threads[i] = std::thread(&GSATThread::runThread, this, i, verbose);
  105. }
  106. //Attend resultat
  107. for(int i = 0; i < nbThread; i++){
  108. threads[i].join();
  109. }
  110. }
  111. void GSATThread::initThread(int id, bool verbose) {
  112. //Les threads vont jouer les bandits pour etablir les moyennes
  113. bool solve = false;
  114. while(!this->isEnd() && !solve && !cb.queueIsEmpty()){
  115. solve = this->calc(id, verbose);
  116. }
  117. //Si 1er arreter
  118. if(!this->isEnd() && solve) {
  119. this->end();
  120. calcTime = gsat[id]->realTime() - time[id];
  121. result.threadId = id;
  122. result.nbIteration = gsat[id]->getNbIterations();
  123. result.heuristicFill = gsat[id]->getHeuristicFill();
  124. result.heuristicSolve = gsat[id]->getHeuristicSolve();
  125. result.nbSatisfiedClausesFill = gsat[id]->getNbSatisfiedClausesFill();
  126. result.nbSatisfiedClausesSolve = gsat[id]->getNbSatisfiedClausesSolve();
  127. }
  128. }
  129. void GSATThread::runThread(int id, bool verbose) {
  130. //Les threads vont jouer les bandits avec la méthode choisit
  131. bool solve = false;
  132. while(!this->isEnd() && !solve){
  133. solve = this->calc(id, verbose);
  134. }
  135. //Si 1er arreter
  136. if(!this->isEnd() && solve) {
  137. this->end();
  138. calcTime = gsat[id]->realTime() - time[id];
  139. result.threadId = id;
  140. result.nbIteration = gsat[id]->getNbIterations();
  141. result.heuristicFill = gsat[id]->getHeuristicFill();
  142. result.heuristicSolve = gsat[id]->getHeuristicSolve();
  143. result.nbSatisfiedClausesFill = gsat[id]->getNbSatisfiedClausesFill();
  144. result.nbSatisfiedClausesSolve = gsat[id]->getNbSatisfiedClausesSolve();
  145. }
  146. }
  147. bool GSATThread::calc(int id, bool verbose) {
  148. //Recup le prochaine fill et heuristic à tester
  149. fillAndHeuristic fah = cb.next();
  150. //Calcul
  151. bool solve = gsat[id]->start(fah.fill, fah.heuristic);
  152. //Affiche
  153. if(verbose) {
  154. if(solve) {
  155. printf(CYAN);
  156. }
  157. printf("c [thread:%2d][iteration:%4d][fill:%d][heuristic:%d]Satisfied clauses (begin: %d)(end:%d)\n",
  158. id,
  159. gsat[id]->getNbIterations(),
  160. gsat[id]->getHeuristicFill(),
  161. gsat[id]->getHeuristicSolve(),
  162. gsat[id]->getNbSatisfiedClausesFill(),
  163. gsat[id]->getNbSatisfiedClausesSolve());
  164. if(solve) {
  165. printf(RESET);
  166. }
  167. }
  168. //Ajoute le resultat aux moyenne
  169. cb.addFill(fah.fill, gsat[id]->getNbSatisfiedClausesFill());
  170. cb.addHeuristic(fah.heuristic, gsat[id]->getNbSatisfiedClausesSolve());
  171. return solve;
  172. }