gsat-solver/Bandit/GSATThread.cpp

#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();
	}
}