#include "GSAT/GSAT.hpp" #include #include #include #include #include #include "color.h" using namespace std; void help(char* prog) { fprintf(stderr, "usage: %s -i file.cnf\n", prog); exit(1); } int main(int argc, char* argv[]) { if(argc < 3) { help(argv[0]); } //Init MPI int world_size; int world_rank; MPI_Init(NULL, NULL); MPI_Comm_size(MPI_COMM_WORLD, &world_size); MPI_Comm_rank(MPI_COMM_WORLD, &world_rank); GSAT* gsat = new GSAT(); gsat->setParameters(argc,argv); gsat->initialize(); if(world_rank == 0) { printf("c nbProcessors: %d\n", world_size); printf("c nbVariables: %d\n",gsat->getNbVariables()); printf("c nbClauses: %d\n",gsat->getNbClauses()); } double startTime = gsat->realTime(); srand(getpid()); bool end = false; bool stop = false; while(!end && !stop){ //Pour eviter que les processeurs effectue tous les meme calculs int fill = rand() % 4 + 2; int h = rand() % 7; end = gsat->start(fill, h); //Affiche calcul if(end) { printf(CYAN); } printf("c [processor:%d][iteration:%5d][fill:%d][heuristic:%d]Satisfied clauses (begin: %d)(end:%d)\n", world_rank, gsat->getNbIterations(), gsat->getHeuristicFill(), gsat->getHeuristicSolve(), gsat->getNbSatisfiedClausesFill(), gsat->getNbSatisfiedClausesSolve()); if(end) { printf(RESET); } //Regarde si quelqu'un a trouver for(int i = 0; i < world_size; i++){ int buff; if(i == world_rank) { buff = end ? 1 : 0; } MPI_Bcast(&buff, 1, MPI_INT, i, MPI_COMM_WORLD); if(i != world_rank && buff && !stop) { stop = true; } } } if(end) { printf("--------------------------------------------------------------------------------------------\n"); printf(GREEN); printf("s %s\n",end?"SATISFIABLE":"NOT FOUND"); printf(YELLOW); printf("c real time : %.4f seconds\n", gsat->realTime() - startTime); printf("c [processor:%d][iteration:%5d][fill:%d][heuristic:%d]Satisfied clauses (begin: %d)(end:%d)\n", world_rank, gsat->getNbIterations(), gsat->getHeuristicFill(), gsat->getHeuristicSolve(), gsat->getNbSatisfiedClausesFill(), gsat->getNbSatisfiedClausesSolve()); printf(RESET); } MPI_Finalize(); }