YuhangQ/cloud-sat
1
0
Fork 0
Code Issues Pull Requests Packages Projects Releases Wiki Activity

修改了 option 为全局量

Browse Source
This commit is contained in:
YuhangQ 2023-04-18 15:22:11 +08:00
parent 35faa6c1ec
commit f0b131ba22
12 changed files with 133 additions and 167 deletions
Show Stats Download Patch File Download Diff File Expand all files Collapse all files

6
run.sh
View File

@ -13,10 +13,10 @@
# 04157f716c1e9606c6a530657bf8f957-Kakuro-easy-125-ext.xml.hg_4.cnf # 04157f716c1e9606c6a530657bf8f957-Kakuro-easy-125-ext.xml.hg_4.cnf
DIR=/pub/data/chenzh/data/sat2022 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 #./light -i $DIR/$INSTANCE --share=1 --threads=16 --times=3600

88
src/light.cpp
View File

@ -21,48 +21,49 @@ light::~light() {
workers.clear(true); workers.clear(true);
} }
// void light::configure_from_file(const char* file) { void light::configure_from_file(const char* file) {
// if (!strcmp(file, "")) { if (!strcmp(file, "")) {
// configure_name = new vec<char*>[OPT(threads)]; configure_name = new vec<char*>[OPT(threads)];
// configure_val = new vec<double>[OPT(threads)]; configure_val = new vec<double>[OPT(threads)];
// return; return;
// } }
// printf("c Get configure file: %s\n", file); assert(false);
// std::ifstream fin(file); // printf("c Get configure file: %s\n", file);
// char buf[1000]; // std::ifstream fin(file);
// fin.getline(buf, 1000); // char buf[1000];
// char *p = buf + 6; // fin.getline(buf, 1000);
// int ws, ss, id = 0; // char *p = buf + 6;
// p = read_int(p, &ws); // int ws, ss, id = 0;
// p = read_int(p, &ss); // p = read_int(p, &ws);
// printf("%d %d\n", ws, ss); // p = read_int(p, &ss);
// opt->set_para("threads", ws); // printf("%d %d\n", ws, ss);
// configure_name = new vec<char*>[ws]; // opt->set_para("threads", ws);
// configure_val = new vec<double>[ws]; // configure_name = new vec<char*>[ws];
// while (fin.getline(buf, 1000)) { // configure_val = new vec<double>[ws];
// p = strtok(buf, " "); // while (fin.getline(buf, 1000)) {
// printf("%s\n", p); // p = strtok(buf, " ");
// solver_type.push(0); // printf("%s\n", p);
// while (p) { // solver_type.push(0);
// p = strtok(NULL, " "); // while (p) {
// printf("%s\n", p); // p = strtok(NULL, " ");
// if (!p) break; // printf("%s\n", p);
// int l = strlen(p), pos = 0; // if (!p) break;
// for (int i = 1; i < l; i++) // int l = strlen(p), pos = 0;
// if (p[i] == '=') pos = i; // for (int i = 1; i < l; i++)
// char *name = new char[pos]; // if (p[i] == '=') pos = i;
// strncpy(name, p, pos); // char *name = new char[pos];
// printf("%s\n", name); // strncpy(name, p, pos);
// configure_name[id].push(name); // printf("%s\n", name);
// char *val = p + pos + 1; // configure_name[id].push(name);
// double v = atof(val); // char *val = p + pos + 1;
// printf("%.2lf\n", v); // double v = atof(val);
// configure_val[id].push(v); // printf("%.2lf\n", v);
// } // configure_val[id].push(v);
// printf("out\n"); // }
// id++; // printf("out\n");
// } // id++;
// } // }
}
void light::arg_parse(int argc, char **argv) { void light::arg_parse(int argc, char **argv) {
cmdline::parser parser; cmdline::parser parser;
@ -95,4 +96,7 @@ void light::arg_parse(int argc, char **argv) {
filename = new char[file_string.size() + 1]; filename = new char[file_string.size() + 1];
memcpy(filename, file_string.c_str(), file_string.length()); memcpy(filename, file_string.c_str(), file_string.length());
filename[file_string.length()] = '\0'; filename[file_string.length()] = '\0';
configure_from_file(OPT(config).c_str());
} }

2
src/light.hpp
View File

@ -81,7 +81,7 @@ public:
int solve(); int solve();
void terminate_workers(); void terminate_workers();
void print_model(); void print_model();
void configure_from_file(const char*);
}; };
#endif #endif

2
src/paras.cpp
View File

@ -11,7 +11,7 @@ void paras::print_change() {
"Name", "Type", "Now", "Default", "Comment"); "Name", "Type", "Now", "Default", "Comment");
#define PARA(N, T, S, M, D, L, H, C) \ #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)); else printf("c %-20s\t %-10s\t %-10f\t %-10s\t %s\n", (#N), (#T), N, (#D), (C));
PARAS PARAS
#undef PARA #undef PARA

30
src/paras.hpp
View File

@ -7,20 +7,22 @@
// name, type, short-name,must-need, default ,low, high, comments // name, type, short-name,must-need, default ,low, high, comments
#define PARAS \ #define PARAS \
PARA( DPS , int , '\0' , false , 0 , 0 , 1 , "DPS/NPS") \ PARA( DPS , int , '\0' , false , 0 , 0 , 1 , "DPS/NPS") \
PARA( DPS_period , int , '\0' , false , 10000 , 1 , 1e8 , "DPS sharing period") \ PARA( DPS_period , int , '\0' , false , 10000 , 1 , 1e8 , "DPS sharing period") \
PARA( margin , int , '\0' , false , 0 , 0 , 1e3 , "DPS margin") \ PARA( margin , int , '\0' , false , 0 , 0 , 1e3 , "DPS margin") \
PARA( pakis , int , '\0' , false , 1 , 0 , 1 , "Use pakis diversity") \ PARA( pakis , int , '\0' , false , 1 , 0 , 1 , "Use pakis diversity") \
PARA( reset , int , '\0' , false , 0 , 0 , 1 , "Dynamically reseting") \ PARA( reset , int , '\0' , false , 0 , 0 , 1 , "Dynamically reseting") \
PARA( reset_time , int , '\0' , false , 10 , 1 , 1e5 , "Reseting base interval (seconds)") \ 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 , int , '\0' , false , 1 , 0 , 1 , "Sharing learnt clauses") \
PARA( share_intv , int , '\0' , false , 500000, 0 , 1e9 , "Sharing interval (microseconds)") \ 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_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( share_method , int , '\0' , false , 1 , 0 , 1 , "0 for Circle Propagate/ 1 for Tree Broadcast") \
PARA( simplify , int , '\0' , false , 1 , 0 , 1 , "Use Simplify (only preprocess)") \ PARA( shuffle , int , '\0' , false , 1 , 0 , 1 , "Use random shuffle") \
PARA( threads , int , '\0' , false , 32 , 1 , 128 , "Thread number") \ PARA( simplify , int , '\0' , false , 1 , 0 , 1 , "Use Simplify (only preprocess)") \
PARA( times , double , '\0' , false , 5000 , 0 , 1e8 , "Cutoff time") \ PARA( threads , int , '\0' , false , 32 , 1 , 128 , "Thread number") \
PARA( unique , int , '\0' , false , 1 , 0 , 1 , "Whether perform unique checking when receiving clauses from other nodes") 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 // name, short-name, must-need, default, comments

70
src/workers/sharer.cpp → src/sharer.cpp
View File

@ -1,10 +1,10 @@
#include "../light.hpp" #include "light.hpp"
#include "basesolver.hpp" #include "workers/basesolver.hpp"
#include "sharer.hpp" #include "sharer.hpp"
#include "unordered_map" #include "unordered_map"
#include "clause.hpp" #include "workers/clause.hpp"
#include <unistd.h> #include <unistd.h>
#include "../distributed/comm_tag.h" #include "distributed/comm_tag.h"
#include <boost/thread/thread.hpp> #include <boost/thread/thread.hpp>
int nums = 0; int nums = 0;
@ -16,12 +16,12 @@ std::vector<std::pair<MPI_Request*, int*>> send_data_struct;
MPI_Request receive_request; MPI_Request receive_request;
int buf[BUF_SIZE]; int buf[BUF_SIZE];
// int num_received_clauses_by_network = 0; int num_received_clauses_by_network = 0;
// int num_skip_clauses_by_network = 0; int num_skip_clauses_by_network = 0;
// // 记录子句是否已经导入过 // 记录子句是否已经导入过
// std::unordered_map<int, bool> clause_imported; std::unordered_map<int, bool> clause_imported;
void share_clauses_to_next_node(int from, const std::vector<shared_ptr<clause_store>> &cls) { void share_clauses_to_next_node(int from, const std::vector<shared_ptr<clause_store>> &cls) {
@ -37,7 +37,6 @@ void share_clauses_to_next_node(int from, const std::vector<shared_ptr<clause_st
// 初始化发送数据 // 初始化发送数据
for(int i=0; i<cls.size(); i++) { for(int i=0; i<cls.size(); i++) {
//if(clause_imported[cls[i]->hash_code()]) continue;
send_length += (cls[i]->size + 2); send_length += (cls[i]->size + 2);
} }
@ -48,7 +47,6 @@ void share_clauses_to_next_node(int from, const std::vector<shared_ptr<clause_st
send_buf[index++] = from; send_buf[index++] = from;
for(int i=0; i<cls.size(); i++) { for(int i=0; i<cls.size(); i++) {
// if(clause_imported[cls[i]->hash_code()]) continue;
auto& c = cls[i]; auto& c = cls[i];
send_buf[index++] = c->size; send_buf[index++] = c->size;
send_buf[index++] = c->lbd; send_buf[index++] = c->lbd;
@ -99,7 +97,7 @@ bool receive_clauses_from_last_node(std::vector<shared_ptr<clause_store>> &claus
from = buf[index++]; from = buf[index++];
while(index < count) { while(index < count) {
//num_received_clauses_by_network++; num_received_clauses_by_network++;
shared_ptr<clause_store> cl = std::make_shared<clause_store>(buf[index++]); shared_ptr<clause_store> cl = std::make_shared<clause_store>(buf[index++]);
@ -108,11 +106,11 @@ bool receive_clauses_from_last_node(std::vector<shared_ptr<clause_store>> &claus
cl->data[i] = buf[index++]; cl->data[i] = buf[index++];
} }
// if(clause_imported[cl->hash_code()]) { if(clause_imported[cl->hash_code()]) {
// num_skip_clauses_by_network++; num_skip_clauses_by_network++;
// continue; continue;
// } }
clauses.push_back(cl); clauses.push_back(cl);
} }
@ -138,9 +136,9 @@ void sharer::clause_sharing_init() {
void sharer::clause_sharing_end() { void sharer::clause_sharing_end() {
printf("c sharing nums: %d\nc sharing time: %.2lf\n", nums, share_time); 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 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 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 unique reduce percentage: %.2f%%\n", (double) num_skip_clauses_by_network / num_received_clauses_by_network * 100);
} }
void sharer::do_clause_sharing() { void sharer::do_clause_sharing() {
@ -163,9 +161,9 @@ void sharer::do_clause_sharing() {
consumers[j]->import_clauses_from(clauses); consumers[j]->import_clauses_from(clauses);
} }
// for (int k = 0; k < clauses.size(); k++) { for (int k = 0; k < clauses.size(); k++) {
// clause_imported[clauses[k]->hash_code()] = true; clause_imported[clauses[k]->hash_code()] = true;
// } }
// 传递外部网络传输的子句给下个节点 // 传递外部网络传输的子句给下个节点
share_clauses_to_next_node(from, clauses); share_clauses_to_next_node(from, clauses);
@ -177,14 +175,14 @@ void sharer::do_clause_sharing() {
producers[i]->export_clauses_to(cls); producers[i]->export_clauses_to(cls);
// 删除掉重复的学习子句 // 删除掉重复的学习子句
// int t_size = cls.size(); int t_size = cls.size();
// for(int i=0; i<t_size; i++) { for(int i=0; i<t_size; i++) {
// if(clause_imported[cls[i]->hash_code()]) { if(clause_imported[cls[i]->hash_code()]) {
// std::swap(cls[i], cls[t_size-1]); std::swap(cls[i], cls[t_size-1]);
// t_size--; t_size--;
// } }
// } }
// cls.resize(t_size); cls.resize(t_size);
//分享当前节点产生的子句 //分享当前节点产生的子句
if(cls.size() > 0) share_clauses_to_next_node(rank, cls); 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; if (producers[i]->id == consumers[j]->id) continue;
consumers[j]->import_clauses_from(cls); consumers[j]->import_clauses_from(cls);
} }
// for (int k = 0; k < cls.size(); k++) { for (int k = 0; k < cls.size(); k++) {
// clause_imported[cls[k]->hash_code()] = true; clause_imported[cls[k]->hash_code()] = true;
// } }
} }
auto clk_ed = std::chrono::high_resolution_clock::now(); 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 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; if (import_period < 0) return 0;
basesolver *t = producers[id]; basesolver *t = producers[id];
for (int i = 0; i < producers.size(); i++) { 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++) { for (int i = 0; i < cls.size(); i++) {
int sz = cls[i]->size; int sz = cls[i]->size;
while (sz > bucket[x].size()) bucket[x].push(); 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]); bucket[x][sz - 1].push_back(cls[i]);
// else // else
// cls[i]->free_clause(); // cls[i]->free_clause();
} }
cls.clear(); cls.clear();
int space = share_lits; int space = OPT(share_lits);
for (int i = 0; i < bucket[x].size(); i++) { for (int i = 0; i < bucket[x].size(); i++) {
int clause_num = space / (i + 1); int clause_num = space / (i + 1);
// printf("%d %d\n", clause_num, bucket[x][i].size()); // 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() { // void light::share() {

23
src/sharer.hpp Normal file
View File

@ -0,0 +1,23 @@
#ifndef _sharer_hpp_INCLUDED
#define _sharer_hpp_INCLUDED
#include "paras.hpp"
#include <boost/thread.hpp>
#include "utils/vec.hpp"
#include "./workers/clause.hpp"
class basesolver;
class sharer {
public:
vec<std::vector<shared_ptr<clause_store>>> bucket[64];
vec<basesolver *> producers, consumers;
std::vector<shared_ptr<clause_store>> cls;
void do_clause_sharing();
void clause_sharing_init();
void clause_sharing_end();
int sort_clauses(int x);
int import_clauses(int id);
};
#endif

7
src/solve.cpp
View File

@ -1,6 +1,6 @@
#include "light.hpp" #include "light.hpp"
#include "workers/basekissat.hpp" #include "workers/basekissat.hpp"
#include "workers/sharer.hpp" #include "sharer.hpp"
#include "paras.hpp" #include "paras.hpp"
#include <unistd.h> #include <unistd.h>
#include <chrono> #include <chrono>
@ -121,9 +121,6 @@ void light::terminate_workers() {
else else
workers[i]->terminate(); workers[i]->terminate();
} }
for (int i = 0; i < sharers.size(); i++) {
sharers[i]->set_terminated();
}
} }
void light::parse_input() { void light::parse_input() {
@ -155,7 +152,7 @@ int light::solve() {
// 初始化共享子句类 // 初始化共享子句类
sharer* s; sharer* s;
if(OPT(share)) { 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++) { for (int j = 0; j < OPT(threads); j++) {
s->producers.push(workers[j]); s->producers.push(workers[j]);
s->consumers.push(workers[j]); s->consumers.push(workers[j]);

2
src/workers/basekissat.cpp
View File

@ -1,5 +1,5 @@
#include "basekissat.hpp" #include "basekissat.hpp"
#include "sharer.hpp" #include "../sharer.hpp"
#include <thread> #include <thread>
#include <condition_variable> #include <condition_variable>

8
src/workers/basesolver.cpp
View File

@ -1,5 +1,5 @@
#include "basesolver.hpp" #include "basesolver.hpp"
#include "sharer.hpp" #include "../sharer.hpp"
int basesolver::get_period() { int basesolver::get_period() {
boost::mutex::scoped_lock lock(mtx); boost::mutex::scoped_lock lock(mtx);
@ -70,11 +70,11 @@ void basesolver::select_clauses() {
for (int i = 0; i < cls.size(); i++) { for (int i = 0; i < cls.size(); i++) {
int sz = cls[i]->size; int sz = cls[i]->size;
while (sz > bucket.size()) bucket.push(); 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]); bucket[sz - 1].push_back(cls[i]);
} }
period_clauses *pcls = new period_clauses(period); 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++) { for (int i = 0; i < bucket.size(); i++) {
int clause_num = space / (i + 1); int clause_num = space / (i + 1);
if (!clause_num) break; 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 < 75) broaden_export_limit();
if (percent > 98) restrict_export_limit(); if (percent > 98) restrict_export_limit();
//sort finish //sort finish

2
src/workers/clause.hpp
View File

@ -22,6 +22,8 @@ struct clause_store {
} }
ll __hash(int B, int MOD) { ll __hash(int B, int MOD) {
std::sort(data, data+size);
ll res = 0; ll res = 0;
ll b = 1; ll b = 1;

60
src/workers/sharer.hpp
View File

@ -1,60 +0,0 @@
#ifndef _sharer_hpp_INCLUDED
#define _sharer_hpp_INCLUDED
#include "../paras.hpp"
#include <boost/thread.hpp>
#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<std::vector<shared_ptr<clause_store>>> bucket[64]; //need to update
vec<basesolver *> producers, consumers;
std::vector<shared_ptr<clause_store>> 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