diff --git a/hostfile b/hostfile new file mode 100644 index 0000000..eedda91 --- /dev/null +++ b/hostfile @@ -0,0 +1,2 @@ +192.168.100.6 +192.168.100.9 \ No newline at end of file diff --git a/kissat-inc/makefile b/kissat-inc/makefile index 37626dd..01f20c5 100644 --- a/kissat-inc/makefile +++ b/kissat-inc/makefile @@ -1,17 +1,17 @@ all: - $(MAKE) -C "/pub/netdisk1/qianyh/Light/kissat-inc/build" + $(MAKE) -C "/home/chenzh/solvers/cloud-sat/kissat-inc/build" kissat: - $(MAKE) -C "/pub/netdisk1/qianyh/Light/kissat-inc/build" kissat + $(MAKE) -C "/home/chenzh/solvers/cloud-sat/kissat-inc/build" kissat tissat: - $(MAKE) -C "/pub/netdisk1/qianyh/Light/kissat-inc/build" tissat + $(MAKE) -C "/home/chenzh/solvers/cloud-sat/kissat-inc/build" tissat clean: - rm -f "/pub/netdisk1/qianyh/Light/kissat-inc"/makefile - -$(MAKE) -C "/pub/netdisk1/qianyh/Light/kissat-inc/build" clean - rm -rf "/pub/netdisk1/qianyh/Light/kissat-inc/build" + rm -f "/home/chenzh/solvers/cloud-sat/kissat-inc"/makefile + -$(MAKE) -C "/home/chenzh/solvers/cloud-sat/kissat-inc/build" clean + rm -rf "/home/chenzh/solvers/cloud-sat/kissat-inc/build" coverage: - $(MAKE) -C "/pub/netdisk1/qianyh/Light/kissat-inc/build" coverage + $(MAKE) -C "/home/chenzh/solvers/cloud-sat/kissat-inc/build" coverage indent: - $(MAKE) -C "/pub/netdisk1/qianyh/Light/kissat-inc/build" indent + $(MAKE) -C "/home/chenzh/solvers/cloud-sat/kissat-inc/build" indent test: - $(MAKE) -C "/pub/netdisk1/qianyh/Light/kissat-inc/build" test + $(MAKE) -C "/home/chenzh/solvers/cloud-sat/kissat-inc/build" test .PHONY: all clean coverage indent kissat test tissat diff --git a/src/clause.hpp b/src/clause.hpp index 382bda5..4d09671 100644 --- a/src/clause.hpp +++ b/src/clause.hpp @@ -54,56 +54,4 @@ struct clause_store { } }; - -struct period_clauses { - int period; - std::atomic refs; - std::vector> cls; - period_clauses(int p = 0) { - refs = 0; - period = p; - } - - void increase_refs(int inc) { - refs += inc; - } - - bool free_clause() { - int ref = refs.fetch_sub(1); - if (ref <= 1) { - if (ref <= 0) puts("**************************========================"); - return true; - } - return false; - } - void release_clause() { - for (int i = 0; i < cls.size(); i++) - cls[i]->free_clause(); - } - void push(shared_ptr c) { - cls.push_back(c); - } -}; - -struct period_queue { - std::deque q; - mutable boost::mutex mtx; - void push(period_clauses * c) { - boost::mutex::scoped_lock lock(mtx); - q.push_back(c); - } - void pop(int assert_period = -1) { - boost::mutex::scoped_lock lock(mtx); - if (assert_period != -1 && q.front()->period != assert_period) printf("c ............false free pos\n"); - q.front()->release_clause(); - q.pop_front(); - } - period_clauses* find(int period) { - boost::mutex::scoped_lock lock(mtx); - int sp = q.front()->period; - if (period - sp >= q.size()) puts("may occur wrong"); - return q[period - sp]; - } -}; - #endif \ No newline at end of file diff --git a/src/light.cpp b/src/light.cpp index c34994a..a358ebe 100644 --- a/src/light.cpp +++ b/src/light.cpp @@ -8,8 +8,7 @@ light::light(): finalResult (0), - winner_period (1e9), - winner_id (-1), + winner_id (1e9), maxtime (5000) { // opt = new paras(); @@ -21,50 +20,6 @@ light::~light() { workers.clear(true); } -void light::configure_from_file(const char* file) { - if (!strcmp(file, "")) { - configure_name = new vec[OPT(threads)]; - configure_val = new vec[OPT(threads)]; - return; - } - assert(false); - // printf("c Get configure file: %s\n", file); - // std::ifstream fin(file); - // char buf[1000]; - // fin.getline(buf, 1000); - // char *p = buf + 6; - // int ws, ss, id = 0; - // p = read_int(p, &ws); - // p = read_int(p, &ss); - // printf("%d %d\n", ws, ss); - // opt->set_para("threads", ws); - // configure_name = new vec[ws]; - // configure_val = new vec[ws]; - // while (fin.getline(buf, 1000)) { - // p = strtok(buf, " "); - // printf("%s\n", p); - // solver_type.push(0); - // while (p) { - // p = strtok(NULL, " "); - // printf("%s\n", p); - // if (!p) break; - // int l = strlen(p), pos = 0; - // for (int i = 1; i < l; i++) - // if (p[i] == '=') pos = i; - // char *name = new char[pos]; - // strncpy(name, p, pos); - // printf("%s\n", name); - // configure_name[id].push(name); - // char *val = p + pos + 1; - // double v = atof(val); - // printf("%.2lf\n", v); - // configure_val[id].push(v); - // } - // printf("out\n"); - // id++; - // } -} - void light::arg_parse(int argc, char **argv) { cmdline::parser parser; @@ -97,6 +52,5 @@ void light::arg_parse(int argc, char **argv) { memcpy(filename, file_string.c_str(), file_string.length()); filename[file_string.length()] = '\0'; - configure_from_file(OPT(config).c_str()); } \ No newline at end of file diff --git a/src/light.hpp b/src/light.hpp index 9c6947a..ac1c590 100644 --- a/src/light.hpp +++ b/src/light.hpp @@ -55,26 +55,18 @@ public: char* filename; char* instance; - - vec *configure_name; - vec *configure_val; int finalResult; - int winner_period, winner_id; + int winner_id; mutable boost::mutex winner_mtx; int maxtime; void update_winner(int id, int period) { - boost::mutex::scoped_lock lock(winner_mtx); - if (period < winner_period || (period == winner_period && id < winner_id)) { - winner_period = period; + boost::mutex::scoped_lock lock(winner_mtx); + if (id < winner_id) { winner_id = id; } } - int get_winner_period() { - boost::mutex::scoped_lock lock(winner_mtx); - return winner_period; - } - + void arg_parse(int argc, char **argv); void init_workers(); void diversity_workers(); @@ -83,7 +75,6 @@ public: int run(); int solve(); void terminate_workers(); - void configure_from_file(const char*); }; #endif \ No newline at end of file diff --git a/src/sharer.cpp b/src/sharer.cpp index 9721a67..bc426cb 100644 --- a/src/sharer.cpp +++ b/src/sharer.cpp @@ -256,37 +256,6 @@ void sharer::do_clause_sharing() { auto clk_ed = std::chrono::high_resolution_clock::now(); share_time += 0.001 * std::chrono::duration_cast(clk_ed - clk_now).count(); } - -int sharer::import_clauses(int id) { - int current_period = producers[id]->get_period() - 1, import_period = current_period - OPT(margin); - if (import_period < 0) return 0; - basesolver *t = producers[id]; - for (int i = 0; i < producers.size(); i++) { - if (i == id) continue; - basesolver *s = producers[i]; - //wait for s reach period $import_period - // printf("c %d start waiting, since import_p is %d, current_p is %d\n", id, import_period, s->get_period()); - - boost::mutex::scoped_lock lock(s->mtx); - while (s->period <= import_period && s->terminate_period > import_period && !s->terminated) { - s->cond.wait(lock); - } - - if (s->terminated) return -1; - if (s->terminate_period <= import_period) return -1; - - period_clauses *pc = s->pq.find(import_period); - if (pc->period != import_period) { - printf("thread %d, now period = %d, import period = %d, import thread %d\n", id, current_period, import_period, i); - puts("*******************************************************"); - } - // printf("c %d finish waiting %d %d\n", id, import_period, s->period_queue[pos]->period); - t->import_clauses_from(pc->cls); - } - t->unfree.push(import_period); - return 1; - // printf("c thread %d, period %d, import finish\n", id, current_period); -} int sharer::sort_clauses(int x) { for (int i = 0; i < cls.size(); i++) { diff --git a/src/sharer.hpp b/src/sharer.hpp index 1f90ca8..2928740 100644 --- a/src/sharer.hpp +++ b/src/sharer.hpp @@ -36,7 +36,6 @@ public: int receive_clauses_from_other_node(std::vector> &clauses, int &transmitter); int sort_clauses(int x); - int import_clauses(int id); private: light* S; diff --git a/src/solve.cpp b/src/solve.cpp index 326ae57..de4d618 100644 --- a/src/solve.cpp +++ b/src/solve.cpp @@ -29,32 +29,18 @@ 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); + + 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; } @@ -163,20 +149,13 @@ void light::diversity_workers() { 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(); + workers[i]->terminate(); } } @@ -211,7 +190,6 @@ int light::solve() { for (int j = 0; j < OPT(threads); j++) { s->producers.push(workers[j]); s->consumers.push(workers[j]); - workers[j]->in_sharer = s; } printf("==============run1============\n"); s->clause_sharing_init(sharing_groups); diff --git a/src/solver_api/basekissat.cpp b/src/solver_api/basekissat.cpp index 85b9ce4..f15ed45 100644 --- a/src/solver_api/basekissat.cpp +++ b/src/solver_api/basekissat.cpp @@ -108,8 +108,6 @@ basekissat::basekissat(int id, light* light) : basesolver(id, light) { if (OPT(share)) { solver -> cbkImportClause = call_back_in; solver -> cbkExportClause = call_back_out; - solver -> cbk_start_new_period = cbk_start_new_period; - solver -> cbk_free_clauses = cbk_free_clauses; solver -> dps = OPT(DPS); solver -> dps_period = OPT(DPS_period); } @@ -119,19 +117,6 @@ basekissat::~basekissat(){ delete solver; } -void basekissat::parse_from_CNF(char* filename) { - int vars, clauses; - vec> clause; - readfile(filename, &vars, &clauses, clause); - maxvar = vars; - kissat_reserve(solver, vars); - for (int i = 1; i <= clauses; i++) { - int l = clause[i].size(); - for (int j = 0; j < l; j++) - add(clause[i][j]); - add(0); - } -} void basekissat::parse_from_MEM(char* instance) { int vars, clauses; @@ -147,17 +132,6 @@ void basekissat::parse_from_MEM(char* instance) { } } -void basekissat::parse_from_PAR(preprocess* pre) { - maxvar = pre->vars; - kissat_reserve(solver, pre->vars); - for (int i = 1; i <= pre->clauses; i++) { - int l = pre->clause[i].size(); - for (int j = 0; j < l; j++) - add(pre->clause[i][j]); - add(0); - } -} - int basekissat::get_conflicts() { return solver->nconflict; } diff --git a/src/solver_api/basekissat.hpp b/src/solver_api/basekissat.hpp index 14a9280..1d1d5eb 100644 --- a/src/solver_api/basekissat.hpp +++ b/src/solver_api/basekissat.hpp @@ -13,8 +13,6 @@ public: int configure(const char* name, int id); int get_conflicts(); - void parse_from_CNF(char* filename); - void parse_from_PAR(preprocess *pre); void parse_from_MEM(char* instance); void exp_clause(void *cl, int lbd); bool imp_clause(shared_ptrcls, void *cl); @@ -25,5 +23,4 @@ public: friend int cbkImportClause(void *, int *, cvec *); friend int cbkExportClause(void *, int *, cvec *); - friend void cbk_free_clauses(void *); }; \ No newline at end of file diff --git a/src/solver_api/basesolver.cpp b/src/solver_api/basesolver.cpp index 265a3b6..26646da 100644 --- a/src/solver_api/basesolver.cpp +++ b/src/solver_api/basesolver.cpp @@ -1,33 +1,6 @@ #include "basesolver.hpp" #include "../sharer.hpp" -int basesolver::get_period() { - boost::mutex::scoped_lock lock(mtx); - return period; -}; -void basesolver::inc_period() { - boost::mutex::scoped_lock lock(mtx); - period++; - if (period % 100 == 0) printf("c %d reach period %d\n", id, period); - cond.notify_all(); -}; - -void basesolver::internal_terminate() { - boost::mutex::scoped_lock lock(mtx); - terminate_period = period; - cond.notify_all(); -} - -void basesolver::external_terminate() { - { - boost::mutex::scoped_lock lock(mtx); - terminated = 1; - cond.notify_all(); - // printf("c thread %d terminated\n", id); - } - terminate(); -} - void basesolver::broaden_export_limit() { ++good_clause_lbd; } @@ -37,23 +10,11 @@ void basesolver::restrict_export_limit() { --good_clause_lbd; } -double basesolver::get_waiting_time() { - return waiting_time; -} - - void basesolver::export_clauses_to(std::vector> &clauses) { shared_ptr cls; - while (export_clause.pop(cls)) { - - // printf("size: %d [", cls->size); - // for(int i=0; isize; i++) { - // printf("%d ", cls->data[i]); - // } - // printf("] \n"); + while (export_clause.pop(cls)) clauses.push_back(cls); - } } void basesolver::import_clauses_from(std::vector> &clauses) { @@ -62,101 +23,9 @@ void basesolver::import_clauses_from(std::vector> &clau } } -void basesolver::select_clauses() { - sharer *share = in_sharer; - cls.clear(); - export_clauses_to(cls); - - for (int i = 0; i < cls.size(); i++) { - int sz = cls[i]->size; - while (sz > bucket.size()) bucket.push(); - if (sz * (bucket[sz - 1].size() + 1) <= OPT(share_lits)) - bucket[sz - 1].push_back(cls[i]); - } - period_clauses *pcls = new period_clauses(period); - int space = OPT(share_lits); - for (int i = 0; i < bucket.size(); i++) { - int clause_num = space / (i + 1); - if (!clause_num) break; - if (clause_num >= bucket[i].size()) { - space -= bucket[i].size() * (i + 1); - for (int j = 0; j < bucket[i].size(); j++) - pcls->push(bucket[i][j]); - bucket[i].clear(); - } - else { - space -= clause_num * (i + 1); - for (int j = 0; j < clause_num; j++) { - pcls->push(bucket[i].back()); - bucket[i].pop_back(); - } - } - } - int percent = (OPT(share_lits) - space) * 100 / OPT(share_lits); - if (percent < 75) broaden_export_limit(); - if (percent > 98) restrict_export_limit(); - //sort finish - pcls->increase_refs(share->producers.size() - 1); - pq.push(pcls); -} - - void basesolver::get_model(vec &model) { model.clear(); for (int i = 1; i <= maxvar; i++) { model.push(val(i)); } -} - -void cbk_start_new_period(void *solver) { - auto clk_st = std::chrono::high_resolution_clock::now(); - basesolver* S = (basesolver *) solver; - sharer *share = S->in_sharer; - int should_free = 1; - - if (S->period >= S->controller->get_winner_period()) { - S->internal_terminate(); - S->terminate(); - return; - } - printf("c thread %d into select %d\n", S->id, S->period); - S->select_clauses(); - // printf("c %d now finish period %d\n", S->id, S->get_period()); - S->inc_period(); - // printf("c thread %d start import at %d\n", S->id, S->period); - should_free = share->import_clauses(S->id); - printf("c thread %d finish import at %d\n", S->id, S->period); - if (should_free == -1) { - S->internal_terminate(); - S->terminate(); - } - auto clk_now = std::chrono::high_resolution_clock::now(); - int solve_time = std::chrono::duration_cast(clk_now - clk_st).count(); - S->waiting_time += 0.001 * solve_time; - // printf("c %d wait for %d.%03ds\n", S->id, solve_time / 1000, solve_time % 1000); - // printf("c %d finish sharing\n", S->id); -} - -void cbk_free_clauses(void *solver) { - basesolver* S = (basesolver *) solver; - sharer *share = S->in_sharer; - if (S->unfree.size()) printf("free %d period\n", S->unfree.size()); - for (int id = 0; id < S->unfree.size(); id++) { - int import_period = S->unfree[id]; - // int current_period = S->get_period() - 1, import_period = current_period - share->margin; - // if (import_period < 0) return; - for (int i = 0; i < share->producers.size(); i++) { - if (i == S->id) continue; - basesolver *s = share->producers[i]; - period_clauses *pc = s->pq.find(import_period); - if (pc->period != import_period) - puts("*******************************************************"); - if (pc->free_clause()) { - s->pq.pop(import_period); - // printf("thread %d enter, %d is free\n", S->id, i); - } - } - } - S->unfree.clear(); -} - +} \ No newline at end of file diff --git a/src/solver_api/basesolver.hpp b/src/solver_api/basesolver.hpp index 5b4cdf0..3654672 100644 --- a/src/solver_api/basesolver.hpp +++ b/src/solver_api/basesolver.hpp @@ -20,8 +20,6 @@ public: virtual int configure(const char* name, int id) = 0; virtual int get_conflicts() = 0; - virtual void parse_from_CNF(char* filename) = 0; - virtual void parse_from_PAR(preprocess* pre) = 0; virtual void parse_from_MEM(char* instance) = 0; virtual void exp_clause(void *cl, int lbd) = 0; virtual bool imp_clause(shared_ptrcls, void *cl) = 0; @@ -30,38 +28,21 @@ public: void import_clauses_from(std::vector> &clauses); void get_model(vec &model); - void select_clauses(); void broaden_export_limit(); void restrict_export_limit(); - double get_waiting_time(); - int get_period(); - void inc_period(); - void internal_terminate(); - void external_terminate(); - double waiting_time = 0; int good_clause_lbd = 0; light * controller; int id; - sharer* in_sharer; vec model; - int terminate_period = 1e9; - int maxvar, period, margin, terminated = 0; - mutable boost::mutex mtx; - boost::condition_variable cond; - period_queue pq; - std::vector> cls; - vec>> bucket; - vec unfree; + int maxvar, terminated = 0; boost::lockfree::spsc_queue, boost::lockfree::capacity<10240000>> import_clause; boost::lockfree::spsc_queue, boost::lockfree::capacity<10240000>> export_clause; basesolver(int sid, light* light) : id(sid), controller(light) { good_clause_lbd = 2; - period = 0; - margin = 0; } ~basesolver() { @@ -69,11 +50,6 @@ public: controller = NULL; } } - friend void cbk_start_new_period(void *); - friend void cbk_free_clauses(void *); }; -void cbk_start_new_period(void *); -void cbk_free_clauses(void *); - #endif \ No newline at end of file