From 2234ad37988349f6a0b7fe4a4b15542cc7de26e4 Mon Sep 17 00:00:00 2001
From: YuhangQ <i@yuhangq.com>
Date: Thu, 13 Apr 2023 16:30:12 +0800
Subject: [PATCH] =?UTF-8?q?=E4=BF=AE=E5=A4=8D=20preprocess=20=E7=9A=84?=
=?UTF-8?q?=E5=86=85=E5=AD=98=E9=94=99=E8=AF=AF?=
MIME-Version: 1.0
Content-Type: text/plain; charset=UTF-8
Content-Transfer-Encoding: 8bit
---
makefile | 2 +-
run.sh | 8 +++--
src/distributed/leader.hpp | 3 ++
src/distributed/worker.hpp | 3 +-
src/preprocess/gauss.cpp | 67 +++++++++++++++++++++++++----------
src/preprocess/preprocess.cpp | 6 +++-
src/preprocess/preprocess.hpp | 1 -
src/preprocess/resolution.cpp | 5 +--
8 files changed, 67 insertions(+), 28 deletions(-)
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 <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++)
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<int> 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;
}