diff --git a/makefile b/makefile index bc306e2..8c2be03 100644 --- a/makefile +++ b/makefile @@ -6,7 +6,7 @@ OBJECTS := $(addprefix build/,$(SOURCES:%=%.o)) # 声明编译器和编译选项 CXX := mpicxx -CXXFLAGS := -O3 -Wall -Wextra -MMD -MP -march=native -mtune=native +CXXFLAGS := -O3 -Wall -Wextra -MMD -MP -march=native -mtune=native -g LIBS := -Wl,-Bstatic -lkissat -L kissat-inc/build -I kissat-inc/ \ -lm4ri -L m4ri-20140914/.libs -I m4ri-20140914/ \ diff --git a/run.sh b/run.sh index 6ccbce9..550d5b4 100755 --- a/run.sh +++ b/run.sh @@ -12,7 +12,9 @@ # preprocess 占了特别大内存 # 04157f716c1e9606c6a530657bf8f957-Kakuro-easy-125-ext.xml.hg_4.cnf -DIR=/pub/data/chenzh/data/sat2022/ -INSTANCE=01813075a2ddb68ae1fc655ca003437e-sha256__zeroOut_12__freeIn_16__seed_1.cnf +DIR=/pub/data/chenzh/data/sat2022 +INSTANCE=eede03732955f620b5291f9dcf9f95df-tseitin_n200_d3.cnf -make -j 16 && mpirun --bind-to none -np 8 --allow-run-as-root ./light -i $DIR/$INSTANCE --share=1 --threads=16 --times=3600 \ No newline at end of file +make -j 16 && mpirun --bind-to none -np 9 --allow-run-as-root ./light -i $DIR/$INSTANCE --share=1 --threads=16 --times=3600 + +#./light -i $DIR/$INSTANCE --share=1 --threads=16 --times=3600 diff --git a/src/distributed/leader.hpp b/src/distributed/leader.hpp index 72a4a1c..555941a 100644 --- a/src/distributed/leader.hpp +++ b/src/distributed/leader.hpp @@ -29,8 +29,11 @@ void leader_main(light* S, int num_procs, int rank) { MPI_Send(&start, 1, MPI_INT, i, START_TAG, MPI_COMM_WORLD); } + + // preprocess 证明了UNSAT 则不需要启动云计算 if(!start) { + MPI_Barrier(MPI_COMM_WORLD); printf("c [leader] UNSAT!!!!!! by preprocess\n"); printf("s UNSATISFIABLE\n"); return; diff --git a/src/distributed/worker.hpp b/src/distributed/worker.hpp index 3ebeff0..4060efd 100644 --- a/src/distributed/worker.hpp +++ b/src/distributed/worker.hpp @@ -17,7 +17,8 @@ void worker_main(light* S, int num_procs, int rank) { int start; MPI_Recv(&start, 1, MPI_INT, 0, START_TAG, MPI_COMM_WORLD, MPI_STATUS_IGNORE); if(!start) { - printf("c [worker%d] I has no need to start\n", rank); + printf("c [worker%d] I have no need to start\n", rank); + MPI_Barrier(MPI_COMM_WORLD); return; } diff --git a/src/preprocess/gauss.cpp b/src/preprocess/gauss.cpp index ebb394b..16063b3 100644 --- a/src/preprocess/gauss.cpp +++ b/src/preprocess/gauss.cpp @@ -1,9 +1,11 @@ #include "preprocess.hpp" #include +#include #include "m4ri/m4ri.h" #define MAX_XOR 6 bool cmpvar(int x, int y) { + if (abs(x) == abs(y)) return x > y; return abs(x) < abs(y); } @@ -34,7 +36,7 @@ int preprocess::search_xors() { } } for (int i = 1; i <= clauses; i++) { - if (nxtc[i] || clause_delete[i]) continue; + if (nxtc[i]) continue; nxtc[i] = 1; int l = clause[i].size(); if (l <= 2 || l > MAX_XOR) continue; @@ -54,12 +56,12 @@ int preprocess::search_xors() { xorsp.push(i); for (int j = 0; j < occurp[mino_id].size(); j++) { int o = occurp[mino_id][j]; - if (!clause_delete[o] && !nxtc[o] && clause[o].size() == l && abstract[o] == abstract[i]) + if (!nxtc[o] && clause[o].size() == l && abstract[o] == abstract[i]) xorsp.push(o); } for (int j = 0; j < occurn[mino_id].size(); j++) { int o = occurn[mino_id][j]; - if (!clause_delete[o] && !nxtc[o] && clause[o].size() == l && abstract[o] == abstract[i]) + if (!nxtc[o] && clause[o].size() == l && abstract[o] == abstract[i]) xorsp.push(o); } if (xorsp.size() < 2 * required_num) continue; @@ -74,7 +76,7 @@ int preprocess::search_xors() { int o = xorsp[j], dup_v; bool xor_sign = true; for (int k = 0; k < clause[o].size(); k++) { - if (!seen[abs(clause[o][k])]) goto Next; + if (seen[abs(clause[o][k])] != i) goto Next; if (clause[o][k] < 0) xor_sign = !xor_sign; } dup_v = cal_dup_val(o); @@ -90,6 +92,24 @@ int preprocess::search_xors() { xors.push(xorgate(i, 0, l)); if (rhs[1] == 2 * required_num) xors.push(xorgate(i, 1, l)); + // if (rhs[0] == 2 * required_num && rhs[1] == 2 * required_num) { + // printf("%d %d\n", rhs[0], rhs[1]); + // for (int j = 0; j < xorsp.size(); j++) { + // int o = xorsp[j]; + // for (int k = 0; k < clause[o].size(); k++) { + // printf("%d ", clause[o][k]); + // } + // printf(" ---------- %d\n", o); + // } + // } + // int a = abs(clause[i][0]) - 1; + // int b = abs(clause[i][1]) - 1; + // int c = abs(clause[i][2]) - 1; + // if (a > b) std::swap(a, b); + // if (a > c) std::swap(a, c); + // if (b > c) std::swap(b, c); + // printf("%d %d %d ", a, b, c); + // puts(""); } return xors.size(); } @@ -103,14 +123,14 @@ int preprocess::ecc_var() { scc_id.growTo(vars + 1, -1); scc.clear(); //sort(xors.data, xors.data + xors.sz, cmpxorgate); - vec xids; + std::set xids; for (int i = 0; i < xors.size(); i++) { int x = xors[i].c; xids.clear(); for (int j = 0; j < clause[x].size(); j++) if (scc_id[abs(clause[x][j])] != -1) - xids.push(scc_id[abs(clause[x][j])]); + xids.insert(scc_id[abs(clause[x][j])]); if (xids.size() == 0) { scc.push(); @@ -120,7 +140,7 @@ int preprocess::ecc_var() { } } else if (xids.size() == 1) { - int id = xids[0]; + int id = *xids.begin(); for (int j = 0; j < clause[x].size(); j++) { if (scc_id[abs(clause[x][j])] == -1) { scc_id[abs(clause[x][j])] = id; @@ -130,12 +150,13 @@ int preprocess::ecc_var() { } else { int id_max = -1; int sz_max = 0; - for (int j = 0; j < xids.size(); j++) - if (scc[xids[j]].size() > sz_max) - sz_max = scc[xids[j]].size(), id_max = xids[j]; - for (int j = 0; j < xids.size(); j++) { - if (xids[j] != id_max) { - vec& v = scc[xids[j]]; + for (std::set::iterator it = xids.begin(); it != xids.end(); it++) { + if (scc[*it].size() > sz_max) + sz_max = scc[*it].size(), id_max = *it; + } + for (std::set::iterator it = xids.begin(); it != xids.end(); it++) { + if (*it != id_max) { + vec& v = scc[*it]; for (int k = 0; k < v.size(); k++) { scc_id[v[k]] = id_max; scc[id_max].push(v[k]); @@ -221,7 +242,15 @@ int preprocess::gauss_elimination() { clause[clauses].push(-p); clause[clauses].push(-q); } - else if (rhs) {return false;} + else if (rhs) { + // for (int row = 0; row < xor_scc[i].size(); row++) { + // int k = xors[xor_scc[i][row]].c; + // for (int j = 0; j < clause[k].size(); j++) + // printf("%d ", clause[k][j]); + // printf("-------- %d %d %d\n", xor_scc[i][row], k, xors[xor_scc[i][row]].rhs); + // } + return false; + } NextRow:; } } @@ -230,15 +259,15 @@ int preprocess::gauss_elimination() { bool preprocess::preprocess_gauss() { int nxors = search_xors(); - // printf("c [GE] XORs: %d (time: 0.00)\n", nxors); + printf("c [GE] XORs: %d (time: 0.00)\n", nxors); if (!nxors) return true; int nvarscc = ecc_var(); - // printf("c [GE] VAR SCC: %d\n", nvarscc); + printf("c [GE] VAR SCC: %d\n", nvarscc); int nxorscc = ecc_xor(); - // printf("c [GE] XOR SCCs: %d (time: 0.00)\n", nxorscc); + printf("c [GE] XOR SCCs: %d (time: 0.00)\n", nxorscc); int res = gauss_elimination(); - // printf("c [GE] unary xor: %d, bin xor: %d, bin added\n", gauss_eli_unit, gauss_eli_binary); - // if (!res) {printf("c [GE] UNSAT\n");} + printf("c [GE] unary xor: %d, bin xor: %d, bin added\n", gauss_eli_unit, gauss_eli_binary); + if (!res) {printf("c [GE] UNSAT\n");} xors.clear(true); scc_id.clear(true); for (int i = 0; i < scc.size(); i++) diff --git a/src/preprocess/preprocess.cpp b/src/preprocess/preprocess.cpp index 52746a1..2fd3c07 100644 --- a/src/preprocess/preprocess.cpp +++ b/src/preprocess/preprocess.cpp @@ -33,6 +33,9 @@ void preprocess::preprocess_init() { } void preprocess::release() { + // release with some error + return; + delete []f; delete []val; delete []color; @@ -44,7 +47,8 @@ void preprocess::release() { nxtc.clear(true); delete []resseen; delete []a; - delete []mapfrom; + + delete []mapfrom; delete []abstract; for (int i = 0; i <= vars; i++) occurp[i].clear(true), occurn[i].clear(true); diff --git a/src/preprocess/preprocess.hpp b/src/preprocess/preprocess.hpp index 62374fa..49ef65e 100644 --- a/src/preprocess/preprocess.hpp +++ b/src/preprocess/preprocess.hpp @@ -3,7 +3,6 @@ #include "../utils/hashmap.hpp" #include "../utils/vec.hpp" - typedef long long ll; #define mapv(a, b) (1ll * (a) * nlit + (ll)(b)) diff --git a/src/preprocess/resolution.cpp b/src/preprocess/resolution.cpp index 8a762f8..1140521 100644 --- a/src/preprocess/resolution.cpp +++ b/src/preprocess/resolution.cpp @@ -51,7 +51,8 @@ bool preprocess::preprocess_resolution() { q[++r] = i, clean[i] = 1; } } - + printf("c len %d\n", r); + int now_turn = 0, seen_flag = 0; vec vars; while (l <= r) { @@ -91,7 +92,7 @@ bool preprocess::preprocess_resolution() { int op = 0, on = 0; for (int j = 0; j < occurp[i].size(); j++) op += 1 - clause_delete[occurp[i][j]]; for (int j = 0; j < occurn[i].size(); j++) on += 1 - clause_delete[occurn[i][j]]; - if (op * on > op + on) continue; + if (op * on > op + on) { continue;} if (res_is_empty(i)) { q[++r] = i, clean[i] = 1; }