GSATThread.cpp 4.7 KB

123456789101112131415161718192021222324252627282930313233343536373839404142434445464748495051525354555657585960616263646566676869707172737475767778798081828384858687888990919293949596979899100101102103104105106107108109110111112113114115116117118119120121122123124125126127128129130131132133134135136137138139140141142143144145146147148149150151152153154155156157158159160161162163164165166167168169170171172173174175176
  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::useEmaMethod(bool statique) {
  25. cb.setMethod(MT_EMA, statique);
  26. }
  27. void GSATThread::useEpsilonMethod(double epsilon, bool statique) {
  28. cb.setMethod(MT_EPS, statique);
  29. cb.setEpsilon(epsilon);
  30. }
  31. bool GSATThread::solve() {
  32. return this->solve(true);
  33. }
  34. bool GSATThread::solve(bool verbose) {
  35. 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(!end) {
  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 end;
  52. }
  53. void GSATThread::printResult() {
  54. if(end) {
  55. printf(GREEN "s SATISFIABLE\n" RESET);
  56. } else {
  57. printf(RED "NOT FOUND\n" RESET);
  58. }
  59. //printf("s %s\n",end?"SATISFIABLE":"NOT FOUND");
  60. if(!end && calcTime == 0) {
  61. //Si on à pas trouver
  62. calcTime = gsat[0]->realTime() - time[0];
  63. }
  64. printf(YELLOW);
  65. if(end) {
  66. printf("c [thread:%2d][iteration:%4d][fill:%d][heuristic:%d]Satisfied clauses (begin: %d)(end:%d)\n",
  67. result.threadId,
  68. result.nbIteration,
  69. result.heuristicFill,
  70. result.heuristicSolve,
  71. result.nbSatisfiedClausesFill,
  72. result.nbSatisfiedClausesSolve);
  73. }
  74. printf("c real time : %.4f seconds\n", calcTime);
  75. printf(RESET);
  76. }
  77. /* --- Private --- */
  78. void GSATThread::initBandit(bool verbose) {
  79. threads.clear();
  80. //Lance thread
  81. for(int i = 0; i < nbThread; i++) {
  82. time[i] = gsat[i]->realTime();
  83. threads[i] = std::thread(&GSATThread::initThread, this, i, verbose);
  84. }
  85. //Attend resultat
  86. for(int i = 0; i < nbThread; i++){
  87. threads[i].join();
  88. }
  89. }
  90. void GSATThread::runBandit(bool verbose) {
  91. threads.clear();
  92. //Lance thread
  93. for(int i = 0; i < nbThread; i++) {
  94. threads[i] = std::thread(&GSATThread::runThread, this, i, verbose);
  95. }
  96. //Attend resultat
  97. for(int i = 0; i < nbThread; i++){
  98. threads[i].join();
  99. }
  100. }
  101. void GSATThread::initThread(int id, bool verbose) {
  102. //Les threads vont jouer les bandits pour etablir les moyennes
  103. bool solve = false;
  104. while(!end && !solve && !cb.queueIsEmpty()){
  105. solve = this->calc(id, verbose);
  106. }
  107. //Si 1er arreter
  108. if(!end && solve) {
  109. end = true;
  110. calcTime = gsat[id]->realTime() - time[id];
  111. result.threadId = id;
  112. result.nbIteration = gsat[id]->getNbIterations();
  113. result.heuristicFill = gsat[id]->getHeuristicFill();
  114. result.heuristicSolve = gsat[id]->getHeuristicSolve();
  115. result.nbSatisfiedClausesFill = gsat[id]->getNbSatisfiedClausesFill();
  116. result.nbSatisfiedClausesSolve = gsat[id]->getNbSatisfiedClausesSolve();
  117. }
  118. }
  119. void GSATThread::runThread(int id, bool verbose) {
  120. //Les threads vont jouer les bandits avec la méthode choisit
  121. bool solve = false;
  122. while(!end && !solve){
  123. solve = this->calc(id, verbose);
  124. }
  125. //Si 1er arreter
  126. if(!end && solve) {
  127. end = true;
  128. calcTime = gsat[id]->realTime() - time[id];
  129. result.threadId = id;
  130. result.nbIteration = gsat[id]->getNbIterations();
  131. result.heuristicFill = gsat[id]->getHeuristicFill();
  132. result.heuristicSolve = gsat[id]->getHeuristicSolve();
  133. result.nbSatisfiedClausesFill = gsat[id]->getNbSatisfiedClausesFill();
  134. result.nbSatisfiedClausesSolve = gsat[id]->getNbSatisfiedClausesSolve();
  135. }
  136. }
  137. bool GSATThread::calc(int id, bool verbose) {
  138. //Recup le prochaine fill et heuristic à tester
  139. fillAndHeuristic fah = cb.next();
  140. //Calcul
  141. bool solve = gsat[id]->start(fah.fill, fah.heuristic);
  142. //Affiche
  143. if(verbose) {
  144. if(solve) {
  145. printf(CYAN);
  146. }
  147. printf("c [thread:%2d][iteration:%4d][fill:%d][heuristic:%d]Satisfied clauses (begin: %d)(end:%d)\n",
  148. id,
  149. gsat[id]->getNbIterations(),
  150. gsat[id]->getHeuristicFill(),
  151. gsat[id]->getHeuristicSolve(),
  152. gsat[id]->getNbSatisfiedClausesFill(),
  153. gsat[id]->getNbSatisfiedClausesSolve());
  154. if(solve) {
  155. printf(RESET);
  156. }
  157. }
  158. //Ajoute le resultat aux moyenne
  159. cb.addFill(fah.fill, gsat[id]->getNbSatisfiedClausesFill());
  160. cb.addHeuristic(fah.heuristic, gsat[id]->getNbSatisfiedClausesSolve());
  161. return solve;
  162. }