diff --git a/run.sh b/run.sh index 7ec9af9..190051d 100755 --- a/run.sh +++ b/run.sh @@ -13,10 +13,10 @@ # 04157f716c1e9606c6a530657bf8f957-Kakuro-easy-125-ext.xml.hg_4.cnf DIR=/pub/data/chenzh/data/sat2022 -INSTANCE=03bb7baaa45980753a0e7050ae44755d-atco_enc3_opt1_03_53.cnf +INSTANCE=00aefd1fc30c425075166ca051e57218-barman-pfile10-038.sas.ex.15.cnf -# make -j 16 && mpirun --bind-to none -np 9 --allow-run-as-root valgrind ./light -i $DIR/$INSTANCE --share=1 --threads=16 --times=3600 +make -j 16 && mpirun --bind-to none -np 9 --allow-run-as-root ./light -i $DIR/$INSTANCE --share=1 --threads=16 --times=3600 -make -j 16 && mpirun --bind-to none -np 9 --allow-run-as-root ./light -i ./data/hard1.cnf --share=1 --threads=16 --times=3600 +# make -j 16 && mpirun --bind-to none -np 9 --allow-run-as-root ./light -i ./data/hard1.cnf --share=1 --threads=16 --times=3600 #./light -i $DIR/$INSTANCE --share=1 --threads=16 --times=3600 diff --git a/src/light.cpp b/src/light.cpp index c279c43..c34994a 100644 --- a/src/light.cpp +++ b/src/light.cpp @@ -21,48 +21,49 @@ 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; -// } -// 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::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; @@ -95,4 +96,7 @@ void light::arg_parse(int argc, char **argv) { filename = new char[file_string.size() + 1]; 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 fa9a37d..fb4ed6a 100644 --- a/src/light.hpp +++ b/src/light.hpp @@ -81,7 +81,7 @@ public: int solve(); void terminate_workers(); void print_model(); - + void configure_from_file(const char*); }; #endif \ No newline at end of file diff --git a/src/paras.cpp b/src/paras.cpp index 4dbea49..82e588a 100644 --- a/src/paras.cpp +++ b/src/paras.cpp @@ -11,7 +11,7 @@ void paras::print_change() { "Name", "Type", "Now", "Default", "Comment"); #define PARA(N, T, S, M, D, L, H, C) \ - if (map_int.count(#N)) printf("c %-20s\t %-10s\t %-10d\t %-10s\t %s\n", (#N), (#T), N, (#D), (C)); \ + if (!strcmp(#T, "int")) printf("c %-20s\t %-10s\t %-10d\t %-10s\t %s\n", (#N), (#T), N, (#D), (C)); \ else printf("c %-20s\t %-10s\t %-10f\t %-10s\t %s\n", (#N), (#T), N, (#D), (C)); PARAS #undef PARA diff --git a/src/paras.hpp b/src/paras.hpp index 58048ec..da153a9 100644 --- a/src/paras.hpp +++ b/src/paras.hpp @@ -7,20 +7,22 @@ // name, type, short-name,must-need, default ,low, high, comments #define PARAS \ - PARA( DPS , int , '\0' , false , 0 , 0 , 1 , "DPS/NPS") \ - PARA( DPS_period , int , '\0' , false , 10000 , 1 , 1e8 , "DPS sharing period") \ - PARA( margin , int , '\0' , false , 0 , 0 , 1e3 , "DPS margin") \ - PARA( pakis , int , '\0' , false , 1 , 0 , 1 , "Use pakis diversity") \ - PARA( reset , int , '\0' , false , 0 , 0 , 1 , "Dynamically reseting") \ - PARA( reset_time , int , '\0' , false , 10 , 1 , 1e5 , "Reseting base interval (seconds)") \ - PARA( share , int , '\0' , false , 1 , 0 , 1 , "Sharing learnt clauses") \ - PARA( share_intv , int , '\0' , false , 500000, 0 , 1e9 , "Sharing interval (microseconds)") \ - PARA( share_lits , int , '\0' , false , 1500 , 0 , 1e6 , "Sharing lits (per every #share_intv seconds)") \ - PARA( shuffle , int , '\0' , false , 1 , 0 , 1 , "Use random shuffle") \ - PARA( simplify , int , '\0' , false , 1 , 0 , 1 , "Use Simplify (only preprocess)") \ - PARA( threads , int , '\0' , false , 32 , 1 , 128 , "Thread number") \ - PARA( times , double , '\0' , false , 5000 , 0 , 1e8 , "Cutoff time") \ - PARA( unique , int , '\0' , false , 1 , 0 , 1 , "Whether perform unique checking when receiving clauses from other nodes") + PARA( DPS , int , '\0' , false , 0 , 0 , 1 , "DPS/NPS") \ + PARA( DPS_period , int , '\0' , false , 10000 , 1 , 1e8 , "DPS sharing period") \ + PARA( margin , int , '\0' , false , 0 , 0 , 1e3 , "DPS margin") \ + PARA( pakis , int , '\0' , false , 1 , 0 , 1 , "Use pakis diversity") \ + PARA( reset , int , '\0' , false , 0 , 0 , 1 , "Dynamically reseting") \ + PARA( reset_time , int , '\0' , false , 10 , 1 , 1e5 , "Reseting base interval (seconds)") \ + PARA( share , int , '\0' , false , 1 , 0 , 1 , "Sharing learnt clauses") \ + PARA( share_intv , int , '\0' , false , 500000, 0 , 1e9 , "Sharing interval (microseconds)") \ + PARA( share_lits , int , '\0' , false , 1500 , 0 , 1e6 , "Sharing lits (per every #share_intv seconds)") \ + PARA( share_method , int , '\0' , false , 1 , 0 , 1 , "0 for Circle Propagate/ 1 for Tree Broadcast") \ + PARA( shuffle , int , '\0' , false , 1 , 0 , 1 , "Use random shuffle") \ + PARA( simplify , int , '\0' , false , 1 , 0 , 1 , "Use Simplify (only preprocess)") \ + PARA( threads , int , '\0' , false , 32 , 1 , 128 , "Thread number") \ + PARA( times , double , '\0' , false , 5000 , 0 , 1e8 , "Cutoff time") \ + PARA( unique , int , '\0' , false , 1 , 0 , 1 , "Whether perform unique checking when receiving clauses from other nodes") + // name, short-name, must-need, default, comments diff --git a/src/workers/sharer.cpp b/src/sharer.cpp similarity index 84% rename from src/workers/sharer.cpp rename to src/sharer.cpp index 1ec1fdc..74ddb7f 100644 --- a/src/workers/sharer.cpp +++ b/src/sharer.cpp @@ -1,10 +1,10 @@ -#include "../light.hpp" -#include "basesolver.hpp" +#include "light.hpp" +#include "workers/basesolver.hpp" #include "sharer.hpp" #include "unordered_map" -#include "clause.hpp" +#include "workers/clause.hpp" #include -#include "../distributed/comm_tag.h" +#include "distributed/comm_tag.h" #include int nums = 0; @@ -16,12 +16,12 @@ std::vector> send_data_struct; MPI_Request receive_request; int buf[BUF_SIZE]; -// int num_received_clauses_by_network = 0; -// int num_skip_clauses_by_network = 0; +int num_received_clauses_by_network = 0; +int num_skip_clauses_by_network = 0; -// // 记录子句是否已经导入过 +// 记录子句是否已经导入过 -// std::unordered_map clause_imported; +std::unordered_map clause_imported; void share_clauses_to_next_node(int from, const std::vector> &cls) { @@ -37,7 +37,6 @@ void share_clauses_to_next_node(int from, const std::vectorhash_code()]) continue; send_length += (cls[i]->size + 2); } @@ -48,7 +47,6 @@ void share_clauses_to_next_node(int from, const std::vectorhash_code()]) continue; auto& c = cls[i]; send_buf[index++] = c->size; send_buf[index++] = c->lbd; @@ -99,7 +97,7 @@ bool receive_clauses_from_last_node(std::vector> &claus from = buf[index++]; while(index < count) { - //num_received_clauses_by_network++; + num_received_clauses_by_network++; shared_ptr cl = std::make_shared(buf[index++]); @@ -108,11 +106,11 @@ bool receive_clauses_from_last_node(std::vector> &claus cl->data[i] = buf[index++]; } - // if(clause_imported[cl->hash_code()]) { + if(clause_imported[cl->hash_code()]) { - // num_skip_clauses_by_network++; - // continue; - // } + num_skip_clauses_by_network++; + continue; + } clauses.push_back(cl); } @@ -138,9 +136,9 @@ void sharer::clause_sharing_init() { void sharer::clause_sharing_end() { printf("c sharing nums: %d\nc sharing time: %.2lf\n", nums, share_time); - // printf("c sharing received_num_by_network: %d\n", num_received_clauses_by_network); - // printf("c sharing skip_num_by_network: %d\n", num_skip_clauses_by_network); - // printf("c sharing unique reduce percentage: %.2f%%\n", (double) num_skip_clauses_by_network / num_received_clauses_by_network * 100); + printf("c sharing received_num_by_network: %d\n", num_received_clauses_by_network); + printf("c sharing skip_num_by_network: %d\n", num_skip_clauses_by_network); + printf("c sharing unique reduce percentage: %.2f%%\n", (double) num_skip_clauses_by_network / num_received_clauses_by_network * 100); } void sharer::do_clause_sharing() { @@ -163,9 +161,9 @@ void sharer::do_clause_sharing() { consumers[j]->import_clauses_from(clauses); } - // for (int k = 0; k < clauses.size(); k++) { - // clause_imported[clauses[k]->hash_code()] = true; - // } + for (int k = 0; k < clauses.size(); k++) { + clause_imported[clauses[k]->hash_code()] = true; + } // 传递外部网络传输的子句给下个节点 share_clauses_to_next_node(from, clauses); @@ -177,14 +175,14 @@ void sharer::do_clause_sharing() { producers[i]->export_clauses_to(cls); // 删除掉重复的学习子句 - // int t_size = cls.size(); - // for(int i=0; ihash_code()]) { - // std::swap(cls[i], cls[t_size-1]); - // t_size--; - // } - // } - // cls.resize(t_size); + int t_size = cls.size(); + for(int i=0; ihash_code()]) { + std::swap(cls[i], cls[t_size-1]); + t_size--; + } + } + cls.resize(t_size); //分享当前节点产生的子句 if(cls.size() > 0) share_clauses_to_next_node(rank, cls); @@ -205,9 +203,9 @@ void sharer::do_clause_sharing() { if (producers[i]->id == consumers[j]->id) continue; consumers[j]->import_clauses_from(cls); } - // for (int k = 0; k < cls.size(); k++) { - // clause_imported[cls[k]->hash_code()] = true; - // } + for (int k = 0; k < cls.size(); k++) { + clause_imported[cls[k]->hash_code()] = true; + } } auto clk_ed = std::chrono::high_resolution_clock::now(); @@ -215,7 +213,7 @@ void sharer::do_clause_sharing() { } int sharer::import_clauses(int id) { - int current_period = producers[id]->get_period() - 1, import_period = current_period - margin; + 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++) { @@ -249,13 +247,13 @@ int sharer::sort_clauses(int x) { for (int i = 0; i < cls.size(); i++) { int sz = cls[i]->size; while (sz > bucket[x].size()) bucket[x].push(); - if (sz * (bucket[x][sz - 1].size() + 1) <= share_lits) + if (sz * (bucket[x][sz - 1].size() + 1) <= OPT(share_lits)) bucket[x][sz - 1].push_back(cls[i]); // else // cls[i]->free_clause(); } cls.clear(); - int space = share_lits; + int space = OPT(share_lits); for (int i = 0; i < bucket[x].size(); i++) { int clause_num = space / (i + 1); // printf("%d %d\n", clause_num, bucket[x][i].size()); @@ -274,7 +272,7 @@ int sharer::sort_clauses(int x) { } } } - return (share_lits - space) * 100 / share_lits; + return (OPT(share_lits) - space) * 100 / OPT(share_lits); } // void light::share() { diff --git a/src/sharer.hpp b/src/sharer.hpp new file mode 100644 index 0000000..a4050f1 --- /dev/null +++ b/src/sharer.hpp @@ -0,0 +1,23 @@ +#ifndef _sharer_hpp_INCLUDED +#define _sharer_hpp_INCLUDED +#include "paras.hpp" +#include +#include "utils/vec.hpp" +#include "./workers/clause.hpp" + +class basesolver; +class sharer { +public: + vec>> bucket[64]; + vec producers, consumers; + std::vector> cls; + + void do_clause_sharing(); + void clause_sharing_init(); + void clause_sharing_end(); + + int sort_clauses(int x); + int import_clauses(int id); +}; + +#endif \ No newline at end of file diff --git a/src/solve.cpp b/src/solve.cpp index 783fd5e..64f1ebf 100644 --- a/src/solve.cpp +++ b/src/solve.cpp @@ -1,6 +1,6 @@ #include "light.hpp" #include "workers/basekissat.hpp" -#include "workers/sharer.hpp" +#include "sharer.hpp" #include "paras.hpp" #include #include @@ -121,9 +121,6 @@ void light::terminate_workers() { else workers[i]->terminate(); } - for (int i = 0; i < sharers.size(); i++) { - sharers[i]->set_terminated(); - } } void light::parse_input() { @@ -155,7 +152,7 @@ int light::solve() { // 初始化共享子句类 sharer* s; if(OPT(share)) { - s = new sharer(0, OPT(share_intv), OPT(share_lits), OPT(DPS)); + s = new sharer(); for (int j = 0; j < OPT(threads); j++) { s->producers.push(workers[j]); s->consumers.push(workers[j]); diff --git a/src/workers/basekissat.cpp b/src/workers/basekissat.cpp index defea82..8db8be1 100644 --- a/src/workers/basekissat.cpp +++ b/src/workers/basekissat.cpp @@ -1,5 +1,5 @@ #include "basekissat.hpp" -#include "sharer.hpp" +#include "../sharer.hpp" #include #include diff --git a/src/workers/basesolver.cpp b/src/workers/basesolver.cpp index a26d47d..265a3b6 100644 --- a/src/workers/basesolver.cpp +++ b/src/workers/basesolver.cpp @@ -1,5 +1,5 @@ #include "basesolver.hpp" -#include "sharer.hpp" +#include "../sharer.hpp" int basesolver::get_period() { boost::mutex::scoped_lock lock(mtx); @@ -70,11 +70,11 @@ void basesolver::select_clauses() { 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) <= share->share_lits) + 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 = share->share_lits; + int space = OPT(share_lits); for (int i = 0; i < bucket.size(); i++) { int clause_num = space / (i + 1); if (!clause_num) break; @@ -92,7 +92,7 @@ void basesolver::select_clauses() { } } } - int percent = (share->share_lits - space) * 100 / share->share_lits; + int percent = (OPT(share_lits) - space) * 100 / OPT(share_lits); if (percent < 75) broaden_export_limit(); if (percent > 98) restrict_export_limit(); //sort finish diff --git a/src/workers/clause.hpp b/src/workers/clause.hpp index 8111356..03788eb 100644 --- a/src/workers/clause.hpp +++ b/src/workers/clause.hpp @@ -22,6 +22,8 @@ struct clause_store { } ll __hash(int B, int MOD) { + std::sort(data, data+size); + ll res = 0; ll b = 1; diff --git a/src/workers/sharer.hpp b/src/workers/sharer.hpp deleted file mode 100644 index a71ab5f..0000000 --- a/src/workers/sharer.hpp +++ /dev/null @@ -1,60 +0,0 @@ -#ifndef _sharer_hpp_INCLUDED -#define _sharer_hpp_INCLUDED -#include "../paras.hpp" -#include -#include "../utils/vec.hpp" -#include "clause.hpp" - -class basesolver; -class sharer { -public: - int id; - int share_intv, share_lits, dps; - int margin; - mutable boost::mutex mtx; - boost::condition_variable cond; - int terminated; - int waitings; - vec>> bucket[64]; //need to update - - vec producers, consumers; - std::vector> cls; - sharer(int idx, int intv, int lits, int share_dps = 0) { - share_intv = intv; - share_lits = lits; - dps = share_dps; - id = idx; - waitings = terminated = 0; - } - - void do_clause_sharing(); - void clause_sharing_init(); - void clause_sharing_end(); - - void set_terminated() { - boost::mutex::scoped_lock lock(mtx); - terminated = 1; - cond.notify_one(); - } - bool should_sharing() const { - boost::mutex::scoped_lock lock(mtx); - return waitings == producers.size(); - } - void waiting_for_all_ready() { - boost::mutex::scoped_lock lock(mtx); - while (waitings != producers.size() && !terminated) { - cond.wait(lock); - } - } - void sharing_finish() { - boost::mutex::scoped_lock lock(mtx); - waitings = 0; - // printf("c sharing thread finish sharing\n"); - cond.notify_all(); - } - int sort_clauses(int x); - // void select_clauses(int id); - int import_clauses(int id); -}; - -#endif \ No newline at end of file