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

修复 preprocess 的内存错误

Browse Source
This commit is contained in:
YuhangQ 2023-04-13 16:30:12 +08:00
parent a01d4cc744
commit 1d40219028
8 changed files with 67 additions and 28 deletions
Show Stats Download Patch File Download Diff File Expand all files Collapse all files

2
makefile
View File

@ -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/ \

8
run.sh
View File

@ -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
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

3
src/distributed/leader.hpp
View File

@ -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;

3
src/distributed/worker.hpp
View File

@ -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;
}

67
src/preprocess/gauss.cpp
View File

@ -1,9 +1,11 @@
#include "preprocess.hpp"
#include <algorithm>
#include <set>
#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<int> xids;
std::set<int> 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<int>& v = scc[xids[j]];
for (std::set<int>::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<int>::iterator it = xids.begin(); it != xids.end(); it++) {
if (*it != id_max) {
vec<int>& 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++)

4
src/preprocess/preprocess.cpp
View File

@ -33,6 +33,9 @@ void preprocess::preprocess_init() {
}
void preprocess::release() {
// release with some error
return;
delete []f;
delete []val;
delete []color;
@ -44,6 +47,7 @@ void preprocess::release() {
nxtc.clear(true);
delete []resseen;
delete []a;
delete []mapfrom;
delete []abstract;
for (int i = 0; i <= vars; i++)

1
src/preprocess/preprocess.hpp
View File

@ -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))

3
src/preprocess/resolution.cpp
View File

@ -51,6 +51,7 @@ bool preprocess::preprocess_resolution() {
q[++r] = i, clean[i] = 1;
}
}
printf("c len %d\n", r);
int now_turn = 0, seen_flag = 0;
vec<int> vars;
@ -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;
}