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

fixed v2 bug

Browse Source
This commit is contained in:
iHaN-o 2022-09-17 17:21:16 +08:00
parent a011f8ed53
commit 50258db84d
4 changed files with 48 additions and 45 deletions
Show Stats Download Patch File Download Diff File Expand all files Collapse all files

BIN
light
View File

Binary file not shown.

BIN
light-v2 Executable file
View File

Binary file not shown.

93
preprocess.cpp
View File

@ -110,14 +110,15 @@ bool preprocess::preprocess_resolution() {
for (int i = 1; i <= vars; i++) {
occurn[i].clear();
occurp[i].clear();
resseen[i] = resseen[i + vars] = clean[i] = seen[i] = 0;
resseen[i - 1] = resseen[i + vars - 1] = clean[i] = seen[i] = 0;
}
for (int i = 1; i <= clauses; i++) {
int l = clause[i].size();
clause_delete[i] = 0;
for (int j = 0; j < l; j++)
for (int j = 0; j < l; j++) {
if (clause[i][j] > 0) occurp[abs(clause[i][j])].push(i);
else occurn[abs(clause[i][j])].push(i);
}
}
for (int i = 1; i <= vars; i++)
if (occurn[i].size() == 0 && occurp[i].size() == 0) clean[i] = 1;
@ -204,12 +205,13 @@ bool preprocess::preprocess_resolution() {
}
return true;
}
int count = 0;
void preprocess::update_var_clause_label() {
++count;
int remain_var = 0;
for (int i = 1; i <= vars; i++) color[i] = 0;
for (int i = 1; i <= clauses; i++) {
if (clause_delete[i]) continue;
if (clause_delete[i]) {continue;}
int l = clause[i].size();
for (int j = 0; j < l; j++) {
if (color[abs(clause[i][j])] == 0) color[abs(clause[i][j])] = ++remain_var;
@ -243,48 +245,49 @@ bool preprocess::preprocess_binary() {
C = new HashMap();
for (int i = 1; i <= clauses; i++) {
int l = clause[i].size();
for (int j = 0; j < l; j++)
for (int j = 0; j < l; j++) {
clause[i][j] = tolit(clause[i][j]);
}
}
nlit = (vars << 1) + 2;
for (int i = 1; i <= vars; i++) f[i] = i, val[i] = 1, color[i] = 0;
for (int i = 1; i <= clauses; i++) clause_delete[i] = 0;
int len = 0;
for (int i = 1; i <= clauses; i++) {
if (clause[i].size() != 2) continue;
nxtc[++len] = i;
ll id1 = mapv(clause[i][0], clause[i][1]),
id2 = mapv(clause[i][1], clause[i][0]);
C->insert(id1, i);
C->insert(id2, i);
}
// int len = 0;
// for (int i = 1; i <= clauses; i++) {
// if (clause[i].size() != 2) continue;
// nxtc[++len] = i;
// ll id1 = mapv(clause[i][0], clause[i][1]),
// id2 = mapv(clause[i][1], clause[i][0]);
// C->insert(id1, i);
// C->insert(id2, i);
// }
for (int k = 1; k <= len; k++) {
int i = nxtc[k];
if (clause[i].size() != 2 || clause_delete[i]) continue;
int r = C->get(mapv(negative(clause[i][0]), negative(clause[i][1])), 0);
if (r) {
clause_delete[r] = clause_delete[i] = 1;
int u = toiidx(clause[i][0]), v = toiidx(clause[i][1]);
int fa = find(u), fb = find(v);
int sig = sign(clause[i][0]) * sign(clause[i][1]) * (-1);
//sig == 1 : a = b -1 : a = -b
if (fa != fb) {
if (fa < fb) {
f[fa] = fb;
val[fa] = sig / (val[u] * val[v]);
}
else if (fa > fb) {
f[fb] = fa;
val[fb] = sig / (val[u] * val[v]);
}
}
else if (sig != val[u] * val[v])
return false;
}
}
// for (int k = 1; k <= len; k++) {
// int i = nxtc[k];
// if (clause[i].size() != 2 || clause_delete[i]) continue;
// int r = C->get(mapv(negative(clause[i][0]), negative(clause[i][1])), 0);
// if (r) {
// clause_delete[r] = clause_delete[i] = 1;
// int u = toiidx(clause[i][0]), v = toiidx(clause[i][1]);
// int fa = find(u), fb = find(v);
// int sig = sign(clause[i][0]) * sign(clause[i][1]) * (-1);
// //sig == 1 : a = b -1 : a = -b
// if (fa != fb) {
// if (fa < fb) {
// f[fa] = fb;
// val[fa] = sig / (val[u] * val[v]);
// }
// else if (fa > fb) {
// f[fb] = fa;
// val[fb] = sig / (val[u] * val[v]);
// }
// }
// else if (sig != val[u] * val[v])
// return false;
// }
// }
for (int i = 1; i <= vars; i++) find(i);
// for (int i = 1; i <= vars; i++) find(i);
for (int i = 1; i <= clauses; i++) {
if (clause_delete[i]) continue;
@ -319,12 +322,12 @@ bool preprocess::preprocess_binary() {
}
update_var_clause_label();
for (int i = 1; i <= orivars; i++) {
if (mapval[i]) continue;
int v = mapto[i], fa = find(v);
if (color[fa]) mapto[i] = color[fa] * val[v];
else {puts("why happened"); mapval[i] = val[v], mapto[i] = 0;}
}
// for (int i = 1; i <= orivars; i++) {
// if (mapval[i]) continue;
// int v = mapto[i], fa = find(v);
// if (color[fa]) mapto[i] = color[fa] * val[v];
// else {puts("why happened"); mapval[i] = val[v], mapto[i] = 0;}
// }
return true;
}

BIN
preprocess.o
View File

Binary file not shown.