123456789101112131415161718192021222324252627282930313233343536373839404142434445464748495051525354555657585960616263646566676869707172737475767778798081828384858687888990919293949596979899100101102103104105106107108109110111112113114115116117118119120121122123124125126127128129130131132133134135136137138139140141142143144145146147148149150151152153154155156157158159160161162163164165166167168169170171172173174175176177178179180181182183184185186187188189 |
- #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) {
- this->end(false);
- calcTime = 0;
- //Lance Initialise
- printf("--- Initialize --------------------------------------------------------------------------\n");
- this->initBandit(verbose);
- //Si la reponse n'a pas été trouvé durant l'initialisation
- if(!this->isEnd()) {
- //Lance les bandit avec la méthode choisit
- printf("--- Search ------------------------------------------------------------------------------\n");
- this->runBandit(verbose);
- }
- //Resultat
- if(verbose) {
- printf("--- Result ------------------------------------------------------------------------------\n");
- this->printResult();
- }
- return this->isEnd();
- }
- void GSATThread::end() {
- this->end(true);
- }
- void GSATThread::end(bool endOrNot) {
- std::lock_guard<std::mutex> guard(mEnd);
- bEnd = endOrNot;
- }
- bool GSATThread::isEnd() {
- std::lock_guard<std::mutex> guard(mEnd);
- return bEnd;
- }
- void GSATThread::printResult() {
- if(this->isEnd()) {
- printf(GREEN "s SATISFIABLE\n" RESET);
- } else {
- printf(RED "NOT FOUND\n" RESET);
- }
- if(!this->isEnd() && calcTime == 0) {
- //Si on à pas trouver
- calcTime = gsat[0]->realTime() - time[0];
- }
- printf(YELLOW);
- printf("c real time : %.4f seconds\n", calcTime);
- if(this->isEnd()) {
- printf("c [thread:%2d][iteration:%4d][fill:%d][heuristic:%d]Satisfied clauses (begin: %d)(end:%d)\n",
- result.threadId,
- result.nbIteration,
- result.heuristicFill,
- result.heuristicSolve,
- result.nbSatisfiedClausesFill,
- result.nbSatisfiedClausesSolve);
- }
- 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(!this->isEnd() && !solve && !cb.queueIsEmpty()){
- solve = this->calc(id, verbose);
- }
- //Si 1er arreter
- if(!this->isEnd() && solve) {
- this->end();
- 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(!this->isEnd() && !solve){
- solve = this->calc(id, verbose);
- }
- //Si 1er arreter
- if(!this->isEnd() && solve) {
- this->end();
- 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();
- }
- }
- bool GSATThread::calc(int id, bool verbose) {
- //Recup le prochaine fill et heuristic à tester
- fillAndHeuristic fah = cb.next();
- //Calcul
- bool solve = gsat[id]->start(fah.fill, fah.heuristic);
- //Affiche
- if(verbose) {
- if(solve) {
- printf(CYAN);
- }
- printf("c [thread:%2d][iteration:%4d][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());
- return solve;
- }
|