#include "light.hpp" #include "workers/basekissat.hpp" #include "workers/sharer.hpp" #include "paras.hpp" #include #include #include #include #include "mpi.h" auto clk_st = std::chrono::high_resolution_clock::now(); char* worker_sign = ""; std::atomic terminated; int result = 0; int winner_conf; void * read_worker(void *arg) { basesolver * sq = (basesolver *)arg; // if (worker_sign == "") // sq->parse_from_PAR(sq->controller->pre); // else // sq->parse_from_CNF(worker_sign); sq->parse_from_MEM(sq->controller->instance); return NULL; } void * solve_worker(void *arg) { basesolver * sq = (basesolver *)arg; while (!terminated) { int res = sq->solve(); if (OPT(DPS)) { //printf("c %d solved, res is %d\n", sq->id, res); if (res) { terminated = 1; result = res; //printf("c %d solved 1\n", sq->id); sq->internal_terminate(); //printf("c %d solved 2\n", sq->id); sq->controller->update_winner(sq->id, sq->period); //printf("c %d solved 3\n", sq->id); if (res == 10) sq->get_model(sq->model); } //printf("c %d really solved, period is %d\n", sq->id, sq->period); } else { if (res && !terminated) { //printf("c result: %d, winner is %d, winner run %d confs\n", res, sq->id, sq->get_conflicts()); terminated = 1; sq->controller->terminate_workers(); result = res; sq->controller->update_winner(sq->id, 0); winner_conf = sq->get_conflicts(); if (res == 10) sq->get_model(sq->model); } //printf("get result %d with res %d\n", sq->id, res); } } return NULL; } void light::init_workers() { terminated = 0; for (int i = 0; i < OPT(threads); i++) { basekissat* kissat = new basekissat(i, this); workers.push(kissat); } } void light::diversity_workers() { for (int i = 0; i < OPT(threads); i++) { if (OPT(shuffle)) { if (i) workers[i]->configure("order_reset", i); } if (OPT(pakis)) { if (i == 13 || i == 14 || i == 9) workers[i]->configure("tier1", 3); else workers[i]->configure("tier1", 2); if (i == 3 || i == 6 || i == 8 || i == 11 || i == 12 || i == 13 || i == 14 || i == 15) workers[i]->configure("chrono", 0); else workers[i]->configure("chrono", 1); if (i == 2 || i == 15) workers[i]->configure("stable", 0); else if (i == 6 || i == 14) workers[i]->configure("stable", 2); else workers[i]->configure("stable", 1); if (i == 10) workers[i]->configure("walkinitially", 1); else workers[i]->configure("walkinitially", 0); if (i == 7 || i == 8 || i == 9 || i == 11) workers[i]->configure("target", 0); else if (i == 0 || i == 2 || i == 3 || i == 4 || i == 5 || i == 6 || i == 10) workers[i]->configure("target", 1); else workers[i]->configure("target", 2); if (i == 4 || i == 5 || i == 8 || i == 9 || i == 12 || i == 13 || i == 15) workers[i]->configure("phase", 0); else workers[i]->configure("phase", 1); } for (int j = 0; j < configure_name[i].size(); j++) { workers[i]->configure(configure_name[i][j], configure_val[i][j]); } } } void light::terminate_workers() { // printf("c controller reach limit\n"); for (int i = 0; i < OPT(threads); i++) { if (OPT(share) == 1 && OPT(DPS) == 1) workers[i]->external_terminate(); else workers[i]->terminate(); } for (int i = 0; i < sharers.size(); i++) { sharers[i]->set_terminated(); } } void light::parse_input() { pthread_t *ptr = new pthread_t[OPT(threads)]; for (int i = 0; i < OPT(threads); i++) { pthread_create(&ptr[i], NULL, read_worker, workers[i]); } for (int i = 0; i < OPT(threads); i++) { pthread_join(ptr[i], NULL); } delete []ptr; } int light::solve() { //printf("c -----------------solve start----------------------\n"); pthread_t *ptr = new pthread_t[OPT(threads)]; for (int i = 0; i < OPT(threads); i++) { pthread_create(&ptr[i], NULL, solve_worker, workers[i]); } thread_inf unimprove[OPT(threads)]; auto clk_sol_st = std::chrono::high_resolution_clock::now(); int pre_time = std::chrono::duration_cast(clk_sol_st - clk_st).count(); int sol_thd = 0, intv_time = OPT(reset_time); // 初始化共享子句类 sharer* s; if(OPT(share)) { s = new sharer(0, OPT(share_intv), OPT(share_lits), OPT(DPS)); for (int j = 0; j < OPT(threads); j++) { s->producers.push(workers[j]); s->consumers.push(workers[j]); workers[j]->in_sharer = s; } s->clause_sharing_init(); } while (!terminated) { usleep(500000); if(OPT(share)) s->do_clause_sharing(); int flag; // when getting terminate signal if(MPI_Test(&terminal_request, &flag, MPI_STATUS_IGNORE) == MPI_SUCCESS && flag == 1) { terminated = 1; terminate_workers(); } auto clk_now = std::chrono::high_resolution_clock::now(); int solve_time = std::chrono::duration_cast(clk_now - clk_st).count(); if (solve_time >= OPT(times)) { terminated = 1; terminate_workers(); } } if(OPT(share)) s->clause_sharing_end(); // printf("ending solve\n"); // terminate_workers(); //important, need combine nps/dps !!!!!!!!!!!!!!!! for (int i = 0; i < OPT(threads); i++) { pthread_join(ptr[i], NULL); } // printf("ending join\n"); if (result == 10) workers[winner_id]->model.copyTo(model); auto clk_now = std::chrono::high_resolution_clock::now(); double solve_time = std::chrono::duration_cast(clk_now - clk_sol_st).count(); solve_time = 0.001 * solve_time; // printf("c solve time: %.2lf\nwinner is %d, period is %d\n", solve_time, winner_id, winner_period); // for (int i = 0; i < OPT(threads); i++) { // printf("c thread %d waiting time: %.2lf\n", i, workers[i]->get_waiting_time()); // } delete []ptr; return result; } int light::run() { init_workers(); diversity_workers(); parse_input(); int res = solve(); return res; } void print_model(vec &model) { printf("v"); for (int i = 0; i < model.size(); i++) { printf(" %d", model[i]); } puts(" 0"); }