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

增加sat-unsat模式

Browse Source
This commit is contained in:
YuhangQ 2023-04-19 06:05:55 +00:00
parent 9038ce048b
commit 3a310fe9ff
5 changed files with 104 additions and 61 deletions
Show Stats Download Patch File Download Diff File Expand all files Collapse all files

4
run.sh
View File

@ -22,8 +22,8 @@
DIR=/pub/data/chenzh/data/sat2022
INSTANCE=04157f716c1e9606c6a530657bf8f957-Kakuro-easy-125-ext.xml.hg_4.cnf
make -j 16 && mpirun --bind-to none -np 5 --allow-run-as-root ./light -i $DIR/$INSTANCE --share=1 --threads=4 --times=3600
# make -j 16 && mpirun --bind-to none -np 5 --allow-run-as-root ./light -i $DIR/$INSTANCE --share=1 --threads=4 --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 4 --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

8
src/main.cpp
View File

@ -36,21 +36,21 @@ int main(int argc, char **argv) {
// [1, sat_procs] for sat
if(rank >= 1 && rank <= sat_procs) {
S->worker_type = Light::SAT;
S->worker_type = light::SAT;
if(S->next_node > sat_procs) {
S->next_node = 1;
}
}
// [sat_procs+1, sat_procs+unsat_procs] for unsat
if(rank >= sat_procs+1 && rank <= sat_procs+unsat_procs) {
S->worker_type = Light::UNSAT;
S->worker_type = light::UNSAT;
if(S->next_node > sat_procs+unsat_procs) {
S->next_node = sat_procs+1;
}
}
// [sat_procs+unsat_procs+1, worker_procs]
if(rank >= sat_procs+unsat_procs+1 && rank <= worker_procs) {
S->worker_type = Light::DEFAULT;
S->worker_type = light::DEFAULT;
if(S->next_node > worker_procs) {
S->next_node = sat_procs+unsat_procs+1;
}
@ -58,7 +58,7 @@ int main(int argc, char **argv) {
} else {
// 总线程太小就跑默认策略
S->worker_type = Light::DEFAULT;
S->worker_type = light::DEFAULT;
S->next_node = rank + 1;
if(S->next_node > worker_procs) {
S->next_node = 1;

18
src/sharer.cpp
View File

@ -160,14 +160,14 @@ void sharer::do_clause_sharing() {
auto clk_now = std::chrono::high_resolution_clock::now();
int solve_time = std::chrono::duration_cast<std::chrono::milliseconds>(clk_now - clk_st).count();
printf("c [node-%d] round %d, time: %d.%d\n", rank, nums, solve_time / 1000, solve_time % 1000);
printf("c node%d(%d)round %d, time: %d.%d\n", rank, S->worker_type, nums, solve_time / 1000, solve_time % 1000);
// 导入外部网络传输的子句
std::vector<shared_ptr<clause_store>> clauses;
int transmitter;
int from = receive_clauses_from_last_node(clauses, transmitter);
if(from != -1 && clauses.size() > 0) {
printf("c [node-%d] get %d exported clauses from node-%d\n", rank, clauses.size(), transmitter);
printf("c node%d(%d) get %d exported clauses from node-%d\n", rank, S->worker_type, clauses.size(), transmitter);
// printf("c [node-%d] sharing unique reduce percentage: %.2f%%\n", rank, (double) num_skip_clauses_by_network / num_received_clauses_by_network * 100);
for (int j = 0; j < consumers.size(); j++) {
@ -205,12 +205,14 @@ void sharer::do_clause_sharing() {
// 增加 lits 限制
int percent = sort_clauses(i);
// if (percent < 75) {
// producers[i]->broaden_export_limit();
// }
// else if (percent > 98) {
// producers[i]->restrict_export_limit();
// }
if(S->worker_type == light::UNSAT) {
if (percent < 75) {
producers[i]->broaden_export_limit();
}
else if (percent > 98) {
producers[i]->restrict_export_limit();
}
}
for (int j = 0; j < consumers.size(); j++) {
if (producers[i]->id == consumers[j]->id) continue;

4
src/sharer.hpp
View File

@ -12,7 +12,7 @@ public:
vec<basesolver *> producers, consumers;
std::vector<shared_ptr<clause_store>> cls;
sharer(int next_node):next_node(next_node) {}
sharer(light *S):S(S) {}
void do_clause_sharing();
void clause_sharing_init();
@ -22,7 +22,7 @@ public:
int import_clauses(int id);
private:
int next_node;
light* S;
};
#endif

69
src/solve.cpp
View File

@ -74,23 +74,60 @@ void light::diversity_workers() {
MPI_Comm_rank(MPI_COMM_WORLD, &rank);
for (int i = 0; i < OPT(threads); i++) {
/**
* sat_group [1, num_procs/2]
* unsat_group [num_procs/2+1, num_procs-1]
*/
// if(rank <= num_procs / 2) {
// workers[i]->configure("sat", 1);
// OPT(share_lits) = 1500;
// } else {
// workers[i]->configure("unsat", 1);
// OPT(share_lits) = 3000;
// }
if(worker_type == SAT) {
if (OPT(shuffle)) {
if (i) workers[i]->configure("order_reset", i);
}
workers[i]->configure("stable", 1);
workers[i]->configure("target", 2);
workers[i]->configure("phase", 1);
workers[i]->configure("heuristic", 0);
if (i == 2)
workers[i]->configure("stable", 0);
else if (i == 6)
workers[i]->configure("stable", 2);
if (i == 7)
workers[i]->configure("target", 0);
else if (i == 0 || i == 2 || i == 3 || i == 6)
workers[i]->configure("target", 1);
if (i == 3 || i == 11 || i == 12 || i == 13 || i == 15)
workers[i]->configure("phase", 0);
} else if(worker_type == UNSAT) {
OPT(share_lits) = 3000;
workers[i]->configure("chrono", 1);
workers[i]->configure("stable", 0);
// workers[i]->configure("walkinitially", 0);
workers[i]->configure("target", 1);
// workers[i]->configure("phase", 1);
workers[i]->configure("heuristic", 0);
// workers[i]->configure("margin", 1)0;
if (i == 0 || i == 1 || i == 7 || i == 8 || i == 11 || i == 15)
workers[i]->configure("heuristic", 1);
if (i == 3 || i == 6 || i == 8 || i == 11 || i == 12 || i == 13)
workers[i]->configure("chrono", 0);
if (i == 2)
workers[i]->configure("stable", 1);
if (i == 9)
workers[i]->configure("target", 0);
else if (i == 14)
workers[i]->configure("target", 2);
} else {
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);
@ -126,6 +163,10 @@ 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]);
}
@ -169,7 +210,7 @@ int light::solve() {
int sol_thd = 0, intv_time = OPT(reset_time);// 初始化共享子句类
if(OPT(share)) {
s = new sharer();
s = new sharer(this);
for (int j = 0; j < OPT(threads); j++) {
s->producers.push(workers[j]);
s->consumers.push(workers[j]);