diff --git a/light b/light-v4-3 similarity index 72% rename from light rename to light-v4-3 index d995133..c6c3eb3 100755 Binary files a/light and b/light-v4-3 differ diff --git a/light.o b/light.o deleted file mode 100644 index 819f023..0000000 Binary files a/light.o and /dev/null differ diff --git a/main.o b/main.o deleted file mode 100644 index 98b5cd6..0000000 Binary files a/main.o and /dev/null differ diff --git a/preprocess/binary.cpp b/preprocess/binary.cpp index 2767c60..59dd68c 100644 --- a/preprocess/binary.cpp +++ b/preprocess/binary.cpp @@ -17,8 +17,9 @@ bool preprocess::preprocess_binary() { clause[i][j] = tolit(clause[i][j]); } } + printf("c sz %d\n", clause[1].size()); nlit = (vars << 1) + 2; - for (int i = 1; i <= vars; i++) f[i] = i, val[i] = 1, varval[i] = color[i] = 0; + for (int i = 1; i <= vars; i++) f[i] = i, val[i] = 1, varval[i] = color[i] = resseen[tolit(i)] = resseen[tolit(-i)] = 0; for (int i = 1; i <= clauses; i++) clause_delete[i] = 0; int len = 0; for (int i = 1; i <= clauses; i++) { @@ -131,6 +132,7 @@ bool preprocess::preprocess_binary() { } if (t == 0) return false; if (t != l) simplify = 1, l = t; + t = 0; for (int j = 0; j < l; j++) { if (resseen[a[j]] == i) continue; @@ -141,7 +143,6 @@ bool preprocess::preprocess_binary() { if (resseen[negative(a[j])] == i && !clause_delete[i]) { clause_delete[i] = 1, simplify = 1; } - for (int j = 0; j < l; j++) resseen[a[j]] = 0; if (l == 1) { @@ -171,7 +172,7 @@ bool preprocess::preprocess_binary() { for (int j = 0; j < l; j++) clause[i].push(a[j]); } - + for (int i = 1; i <= vars; i++) { int x = find(i); if (varval[i] && x != i) { @@ -190,9 +191,8 @@ bool preprocess::preprocess_binary() { } else varval[i] = varval[f[i]] * val[i]; } - break; } - // printf("c turns: %d\n", turn); + printf("c turns: %d\n", turn); for (int i = 1; i <= clauses; i++) { if (clause_delete[i]) continue; diff --git a/preprocess/binary.o b/preprocess/binary.o deleted file mode 100644 index 908f5b0..0000000 Binary files a/preprocess/binary.o and /dev/null differ diff --git a/preprocess/card.o b/preprocess/card.o deleted file mode 100644 index 811a98f..0000000 Binary files a/preprocess/card.o and /dev/null differ diff --git a/preprocess/gauss.o b/preprocess/gauss.o deleted file mode 100644 index 10471f3..0000000 Binary files a/preprocess/gauss.o and /dev/null differ diff --git a/preprocess/preprocess.cpp b/preprocess/preprocess.cpp index 842b35b..abf0d5b 100644 --- a/preprocess/preprocess.cpp +++ b/preprocess/preprocess.cpp @@ -161,15 +161,6 @@ void preprocess::get_complete_model() { } } -void preprocess::write_cnf() { - for (int i = 1; i <= clauses; i++) { - int l = clause[i].size(); - for (int j = 0; j < l; j++) - printf("%d ", clause[i][j]); - puts("0"); - } -} - int preprocess::do_preprocess(char* filename) { readfile(filename); preprocess_init(); @@ -190,6 +181,8 @@ int preprocess::do_preprocess(char* filename) { clause.clear(true); return 0; } + + if (vars <= 1e5 && clauses <= 1e6) { res = preprocess_card(); if (!res) { @@ -213,6 +206,8 @@ int preprocess::do_preprocess(char* filename) { resolution.clear(true); return 0; } + + res = preprocess_binary(); if (!res) { release(); diff --git a/preprocess/preprocess.hpp b/preprocess/preprocess.hpp index 4937833..e32ae22 100644 --- a/preprocess/preprocess.hpp +++ b/preprocess/preprocess.hpp @@ -43,13 +43,14 @@ public: int clauses; vec> clause, res_clause; void readfile(const char *file); + void write_cnf(); void release(); int maxlen, orivars, oriclauses, res_clauses, resolutions; int *f, nlit, *a, *val, *color, *varval, *q, *seen, *resseen, *clean, *mapto, *mapfrom, *mapval; // HashMap* C; vec *occurp, *occurn, clause_delete, nxtc, resolution; - + int find(int x); bool res_is_empty(int var); void update_var_clause_label(); @@ -64,7 +65,6 @@ public: vec> mat; vec *occur; vec cdel; - void write_cnf(); int check_card(int id); int preprocess_card(); int search_almost_one(); diff --git a/preprocess/preprocess.o b/preprocess/preprocess.o deleted file mode 100644 index 3b37c02..0000000 Binary files a/preprocess/preprocess.o and /dev/null differ diff --git a/preprocess/propagation.o b/preprocess/propagation.o deleted file mode 100644 index f5cccfd..0000000 Binary files a/preprocess/propagation.o and /dev/null differ diff --git a/preprocess/resolution.o b/preprocess/resolution.o deleted file mode 100644 index 18e32c6..0000000 Binary files a/preprocess/resolution.o and /dev/null differ diff --git a/solve.o b/solve.o deleted file mode 100644 index d31c326..0000000 Binary files a/solve.o and /dev/null differ diff --git a/testLight/cal_solver.py b/testLight/cal_solver.py index 1c258c0..4307326 100644 --- a/testLight/cal_solver.py +++ b/testLight/cal_solver.py @@ -268,11 +268,17 @@ if __name__ == "__main__": solvers = [] - solvers.append(solver_SAT_standard_gnomon("/pub/data/chenzh/res/sota/p-mcomsps","p-mcomsps")) - solvers.append(solver_SAT_standard_gnomon("/pub/data/chenzh/res/sota/treengeling","treengeling")) + # solvers.append(solver_SAT_standard_gnomon("/pub/data/chenzh/res/sota/p-mcomsps","p-mcomsps")) + # solvers.append(solver_SAT_standard_gnomon("/pub/data/chenzh/res/sota/treengeling","treengeling")) + # solvers.append(solver_SAT_standard_gnomon("/pub/data/chenzh/res/sota/pakis","pakis")) + solvers.append(solver_SAT_standard_gnomon("/pub/data/chenzh/res/sota/pakis22","pakis22")) + solvers.append(solver_SAT_standard_gnomon("/pub/data/chenzh/res/sota/NPS","NPS")) + # solvers.append(solver_SAT_standard_gnomon("/pub/data/chenzh/res/sota/pakis-mab","pakis-mab")) # solvers.append(solver_SAT_standard_gnomon("/pub/data/chenzh/res/light/v3--1-preprocess","preprocess")) solvers.append(solver_SAT_standard_gnomon("/pub/data/chenzh/res/light/v4-1-preprocess","pre")) solvers.append(solver_SAT_standard_gnomon("/pub/data/chenzh/res/light/v4-1-nps","sharing-nps")) + # solvers.append(solver_SAT_standard_gnomon("/pub/data/chenzh/res/light/v4-2-nps-rp","sharing-nps-rp")) + # solvers.append(solver_SAT_standard_gnomon("/pub/data/chenzh/res/light/v4-2-nps-p","sharing-nps-p")) # solvers.append(solver_SAT_standard_gnomon("/pub/data/chenzh/res/light/v4-dps","sharing-dps")) # append_all_solvers_in_dir(solvers, "/pub/data/chenzh/res/light/") diff --git a/testLight/nohup.out b/testLight/nohup.out index e447686..abbf051 100644 Binary files a/testLight/nohup.out and b/testLight/nohup.out differ diff --git a/testLight/run4-1.sh b/testLight/run4-1.sh index 2c51600..a7ae40e 100755 --- a/testLight/run4-1.sh +++ b/testLight/run4-1.sh @@ -21,6 +21,7 @@ res2="/pub/data/chenzh/res/light/v4-1-preprocess" res3="/pub/data/chenzh/res/light/v1-1-origin" res4="/pub/data/chenzh/res/light/v2-preprocess" res5="/pub/data/chenzh/res/light/v3--1-preprocess" +res6="/pub/data/chenzh/res/light/v4-2-nps-rp" res_no="/pub/data/chenzh/res/unused" ##################################################### @@ -29,6 +30,23 @@ for((i=0;i<${#all_datas[*]};i++)) do instance=${all_datas[$i]} + res_solver_ins=$res6 + if [ ! -d "$res_solver_ins" ]; then + mkdir -p $res_solver_ins + fi + for dir_file in `cat $instance/vbs.txt` + do + file=$dir_file + echo $file + touch $res_solver_ins/$file + read -u 6 + { + cd /home/chenzh/solvers/Light + time ./light-v4-2 $instance/$file --share=1 --pakis=1 + echo >&6 + } >$res_solver_ins/$file 2>>$res_solver_ins/$file & + done + # res_solver_ins=$res5 # if [ ! -d "$res_solver_ins" ]; then # mkdir -p $res_solver_ins @@ -79,22 +97,22 @@ do # } >$res_solver_ins/$file 2>>$res_solver_ins/$file & # done - res_solver_ins=$res2 - if [ ! -d "$res_solver_ins" ]; then - mkdir -p $res_solver_ins - fi - for dir_file in `cat $instance/vbs111.txt` - do - file=$dir_file - echo $file - touch $res_solver_ins/$file - read -u 6 - { - cd /home/chenzh/solvers/Light - time ./light-v4-1 $instance/$file --simplify=1 - echo >&6 - } >$res_solver_ins/$file 2>>$res_solver_ins/$file & - done + # res_solver_ins=$res2 + # if [ ! -d "$res_solver_ins" ]; then + # mkdir -p $res_solver_ins + # fi + # for dir_file in `cat $instance/vbs.txt` + # do + # file=$dir_file + # echo $file + # touch $res_solver_ins/$file + # read -u 6 + # { + # cd /home/chenzh/solvers/Light + # time ./light-v4-1 $instance/$file --simplify=1 + # echo >&6 + # } >$res_solver_ins/$file 2>>$res_solver_ins/$file & + # done # res_solver_ins=$res1 # if [ ! -d "$res_solver_ins" ]; then diff --git a/testLight/run4-2.sh b/testLight/run4-2.sh index ad42958..4a35f3d 100755 --- a/testLight/run4-2.sh +++ b/testLight/run4-2.sh @@ -21,6 +21,7 @@ res2="/pub/data/chenzh/res/light/v4-1-preprocess" res3="/pub/data/chenzh/res/light/v1-1-origin" res4="/pub/data/chenzh/res/light/v2-preprocess" res5="/pub/data/chenzh/res/light/v3--1-preprocess" +res6="/pub/data/chenzh/res/light/v4-2-nps-rp" res_no="/pub/data/chenzh/res/unused" ##################################################### @@ -29,6 +30,23 @@ for((i=0;i<${#all_datas[*]};i++)) do instance=${all_datas[$i]} + res_solver_ins=$res6 + if [ ! -d "$res_solver_ins" ]; then + mkdir -p $res_solver_ins + fi + for dir_file in `cat $instance/vbs.txt` + do + file=$dir_file + echo $file + touch $res_solver_ins/$file + read -u 6 + { + cd /home/chenzh/solvers/Light + time ./light-v4-2 $instance/$file --share=1 --pakis=1 + echo >&6 + } >$res_solver_ins/$file 2>>$res_solver_ins/$file & + done + # res_solver_ins=$res5 # if [ ! -d "$res_solver_ins" ]; then # mkdir -p $res_solver_ins @@ -79,22 +97,22 @@ do # } >$res_solver_ins/$file 2>>$res_solver_ins/$file & # done - res_solver_ins=$res2 - if [ ! -d "$res_solver_ins" ]; then - mkdir -p $res_solver_ins - fi - for dir_file in `cat $instance/vbs.txt` - do - file=$dir_file - echo $file - touch $res_solver_ins/$file - read -u 6 - { - cd /home/chenzh/solvers/Light - time ./light-v4-1 $instance/$file --simplify=1 - echo >&6 - } >$res_solver_ins/$file 2>>$res_solver_ins/$file & - done + # res_solver_ins=$res2 + # if [ ! -d "$res_solver_ins" ]; then + # mkdir -p $res_solver_ins + # fi + # for dir_file in `cat $instance/vbs.txt` + # do + # file=$dir_file + # echo $file + # touch $res_solver_ins/$file + # read -u 6 + # { + # cd /home/chenzh/solvers/Light + # time ./light-v4-1 $instance/$file --simplify=1 + # echo >&6 + # } >$res_solver_ins/$file 2>>$res_solver_ins/$file & + # done # res_solver_ins=$res1 # if [ ! -d "$res_solver_ins" ]; then diff --git a/testLight/run5-1.sh b/testLight/run5-1.sh index 943338f..f64b490 100755 --- a/testLight/run5-1.sh +++ b/testLight/run5-1.sh @@ -22,6 +22,7 @@ res3="/pub/data/chenzh/res/light/v1-1-origin" res4="/pub/data/chenzh/res/light/v2-preprocess" res5="/pub/data/chenzh/res/light/v3--1-preprocess" res6="/pub/data/chenzh/res/light/v4-1-nps" +res7="/pub/data/chenzh/res/light/v4-2-nps-p2" res_no="/pub/data/chenzh/res/unused" ##################################################### @@ -30,7 +31,7 @@ for((i=0;i<${#all_datas[*]};i++)) do instance=${all_datas[$i]} - res_solver_ins=$res6 + res_solver_ins=$res7 if [ ! -d "$res_solver_ins" ]; then mkdir -p $res_solver_ins fi @@ -42,12 +43,30 @@ do read -u 6 { cd /home/chenzh/solvers/Light - time ./light-v4-1 $instance/$file --share=1 + time ./light-v4-2 $instance/$file --share=1 --shuffle=0 --pakis=1 echo >&6 } >$res_solver_ins/$file 2>>$res_solver_ins/$file & done + # res_solver_ins=$res6 + # if [ ! -d "$res_solver_ins" ]; then + # mkdir -p $res_solver_ins + # fi + # for dir_file in `cat $instance/vbs.txt` + # do + # file=$dir_file + # echo $file + # touch $res_solver_ins/$file + # read -u 6 + # { + # cd /home/chenzh/solvers/Light + # time ./light-v4-1 $instance/$file --share=1 + # echo >&6 + # } >$res_solver_ins/$file 2>>$res_solver_ins/$file & + # done + + # res_solver_ins=$res5 # if [ ! -d "$res_solver_ins" ]; then # mkdir -p $res_solver_ins diff --git a/testLight/run5-2.sh b/testLight/run5-2.sh index 1ffe09f..6c18088 100755 --- a/testLight/run5-2.sh +++ b/testLight/run5-2.sh @@ -22,19 +22,20 @@ res3="/pub/data/chenzh/res/light/v1-1-origin" res4="/pub/data/chenzh/res/light/v2-preprocess" res5="/pub/data/chenzh/res/light/v3--1-preprocess" res6="/pub/data/chenzh/res/light/v4-1-nps" +res7="/pub/data/chenzh/res/light/v4-2-nps-p2" res_no="/pub/data/chenzh/res/unused" ##################################################### -all_datas=($instance_20) +all_datas=($instance_22) for((i=0;i<${#all_datas[*]};i++)) do instance=${all_datas[$i]} - res_solver_ins=$res6 + res_solver_ins=$res7 if [ ! -d "$res_solver_ins" ]; then mkdir -p $res_solver_ins fi - for dir_file in `cat $instance/vbs.txt` + for dir_file in `cat $instance/all.txt` do file=$dir_file echo $file @@ -42,12 +43,30 @@ do read -u 6 { cd /home/chenzh/solvers/Light - time ./light-v4-1 $instance/$file --share=1 + time ./light-v4-2 $instance/$file --share=1 --shuffle=0 --pakis=1 echo >&6 } >$res_solver_ins/$file 2>>$res_solver_ins/$file & done + # res_solver_ins=$res6 + # if [ ! -d "$res_solver_ins" ]; then + # mkdir -p $res_solver_ins + # fi + # for dir_file in `cat $instance/vbs.txt` + # do + # file=$dir_file + # echo $file + # touch $res_solver_ins/$file + # read -u 6 + # { + # cd /home/chenzh/solvers/Light + # time ./light-v4-1 $instance/$file --share=1 + # echo >&6 + # } >$res_solver_ins/$file 2>>$res_solver_ins/$file & + # done + + # res_solver_ins=$res5 # if [ ! -d "$res_solver_ins" ]; then # mkdir -p $res_solver_ins diff --git a/testLight/run6-1.sh b/testLight/run6-1.sh new file mode 100755 index 0000000..e6520b7 --- /dev/null +++ b/testLight/run6-1.sh @@ -0,0 +1,150 @@ +#!/bin/bash + +SEND_THREAD_NUM=4 +tmp_fifofile="/tmp/$$.fifo" # 脚本运行的当前进程ID号作为文件名 +mkfifo "$tmp_fifofile" # 新建一个随机fifo管道文件 +exec 6<>"$tmp_fifofile" # 定义文件描述符6指向这个fifo管道文件 +rm $tmp_fifofile +for i in $(seq 1 $SEND_THREAD_NUM) +do + echo # for循环 往 fifo管道文件中写入 $SEND_THREAD_NUM 个空行 +done >&6 + +# CUTOFF_TIME=3600 +instance_20="/pub/data/chenzh/data/sat2020" +instance_21="/pub/data/chenzh/data/sat2021" +instance_22="/pub/data/chenzh/data/sat2022" + + +res1="/pub/data/chenzh/res/light/v1-origin" +res2="/pub/data/chenzh/res/light/v4-1-preprocess" +res3="/pub/data/chenzh/res/light/v1-1-origin" +res4="/pub/data/chenzh/res/light/v2-preprocess" +res5="/pub/data/chenzh/res/light/v3--1-preprocess" +res6="/pub/data/chenzh/res/light/v4-2-dps-r" +res_no="/pub/data/chenzh/res/unused" +##################################################### + +all_datas=($instance_21) +for((i=0;i<${#all_datas[*]};i++)) +do + instance=${all_datas[$i]} + + res_solver_ins=$res6 + if [ ! -d "$res_solver_ins" ]; then + mkdir -p $res_solver_ins + fi + for dir_file in `cat $instance/vbs.txt` + do + file=$dir_file + echo $file + touch $res_solver_ins/$file + read -u 6 + { + cd /home/chenzh/solvers/Light + time ./light-v4-2 $instance/$file --share=1 --DPS=1 + echo >&6 + } >$res_solver_ins/$file 2>>$res_solver_ins/$file & + done + + # res_solver_ins=$res5 + # if [ ! -d "$res_solver_ins" ]; then + # mkdir -p $res_solver_ins + # fi + # for dir_file in `cat $instance/vbs.txt` + # do + # file=$dir_file + # echo $file + # touch $res_solver_ins/$file + # read -u 6 + # { + # cd /home/chenzh/solvers/Light + # time ./light-v3--1 $instance/$file --share=1 --threads=31 + # echo >&6 + # } >$res_solver_ins/$file 2>>$res_solver_ins/$file & + # done + # res_solver_ins=$res4 + # if [ ! -d "$res_solver_ins" ]; then + # mkdir -p $res_solver_ins + # fi + # for dir_file in `cat $instance/vbs.txt` + # do + # file=$dir_file + # echo $file + # touch $res_solver_ins/$file + # read -u 6 + # { + # cd /home/chenzh/solvers/Light + # time ./light-v2 $instance/$file --share=1 --threads=31 + # echo >&6 + # } >$res_solver_ins/$file 2>>$res_solver_ins/$file & + # done + + # res_solver_ins=$res3 + # if [ ! -d "$res_solver_ins" ]; then + # mkdir -p $res_solver_ins + # fi + # for dir_file in `cat $instance/vbs.txt` + # do + # file=$dir_file + # echo $file + # touch $res_solver_ins/$file + # read -u 6 + # { + # cd /home/chenzh/solvers/Light + # time ./light-v1-1 $instance/$file --simplify=0 --reset=1 + # echo >&6 + # } >$res_solver_ins/$file 2>>$res_solver_ins/$file & + # done + + # res_solver_ins=$res2 + # if [ ! -d "$res_solver_ins" ]; then + # mkdir -p $res_solver_ins + # fi + # for dir_file in `cat $instance/vbs.txt` + # do + # file=$dir_file + # echo $file + # touch $res_solver_ins/$file + # read -u 6 + # { + # cd /home/chenzh/solvers/Light + # time ./light-v4-1 $instance/$file --simplify=1 + # echo >&6 + # } >$res_solver_ins/$file 2>>$res_solver_ins/$file & + # done + + # res_solver_ins=$res1 + # if [ ! -d "$res_solver_ins" ]; then + # mkdir -p $res_solver_ins + # fi + # for dir_file in `cat $instance/vbs.txt` + # do + # file=$dir_file + # echo $file + # touch $res_solver_ins/$file + # read -u 6 + # { + # cd /home/chenzh/solvers/Light + # time ./light-v1 $instance/$file --simplify=0 + # echo >&6 + # } >$res_solver_ins/$file 2>>$res_solver_ins/$file & + # done +done + +res_solver_ins=$res_no +if [ ! -d "$res_solver_ins" ]; then + mkdir -p $res_solver_ins +fi +for((i=0;i<4;i++)) +do + read -u 6 + { + cd /home/chenzh/solvers/Light + time ./light-v1 /home/chenzh/data/hard_cnfs/49.cnf + echo >&6 + } >$res_solver_ins/$i 2>>$res_solver_ins/$i & +done + + +exit 0 diff --git a/testLight/run6-2.sh b/testLight/run6-2.sh new file mode 100755 index 0000000..04a5764 --- /dev/null +++ b/testLight/run6-2.sh @@ -0,0 +1,150 @@ +#!/bin/bash + +SEND_THREAD_NUM=4 +tmp_fifofile="/tmp/$$.fifo" # 脚本运行的当前进程ID号作为文件名 +mkfifo "$tmp_fifofile" # 新建一个随机fifo管道文件 +exec 6<>"$tmp_fifofile" # 定义文件描述符6指向这个fifo管道文件 +rm $tmp_fifofile +for i in $(seq 1 $SEND_THREAD_NUM) +do + echo # for循环 往 fifo管道文件中写入 $SEND_THREAD_NUM 个空行 +done >&6 + +# CUTOFF_TIME=3600 +instance_20="/pub/data/chenzh/data/sat2020" +instance_21="/pub/data/chenzh/data/sat2021" +instance_22="/pub/data/chenzh/data/sat2022" + + +res1="/pub/data/chenzh/res/light/v1-origin" +res2="/pub/data/chenzh/res/light/v4-1-preprocess" +res3="/pub/data/chenzh/res/light/v1-1-origin" +res4="/pub/data/chenzh/res/light/v2-preprocess" +res5="/pub/data/chenzh/res/light/v3--1-preprocess" +res6="/pub/data/chenzh/res/light/v4-2-dps-r" +res_no="/pub/data/chenzh/res/unused" +##################################################### + +all_datas=($instance_20) +for((i=0;i<${#all_datas[*]};i++)) +do + instance=${all_datas[$i]} + + res_solver_ins=$res6 + if [ ! -d "$res_solver_ins" ]; then + mkdir -p $res_solver_ins + fi + for dir_file in `cat $instance/vbs.txt` + do + file=$dir_file + echo $file + touch $res_solver_ins/$file + read -u 6 + { + cd /home/chenzh/solvers/Light + time ./light-v4-2 $instance/$file --share=1 --DPS=1 + echo >&6 + } >$res_solver_ins/$file 2>>$res_solver_ins/$file & + done + + # res_solver_ins=$res5 + # if [ ! -d "$res_solver_ins" ]; then + # mkdir -p $res_solver_ins + # fi + # for dir_file in `cat $instance/vbs.txt` + # do + # file=$dir_file + # echo $file + # touch $res_solver_ins/$file + # read -u 6 + # { + # cd /home/chenzh/solvers/Light + # time ./light-v3--1 $instance/$file --share=1 --threads=31 + # echo >&6 + # } >$res_solver_ins/$file 2>>$res_solver_ins/$file & + # done + # res_solver_ins=$res4 + # if [ ! -d "$res_solver_ins" ]; then + # mkdir -p $res_solver_ins + # fi + # for dir_file in `cat $instance/vbs.txt` + # do + # file=$dir_file + # echo $file + # touch $res_solver_ins/$file + # read -u 6 + # { + # cd /home/chenzh/solvers/Light + # time ./light-v2 $instance/$file --share=1 --threads=31 + # echo >&6 + # } >$res_solver_ins/$file 2>>$res_solver_ins/$file & + # done + + # res_solver_ins=$res3 + # if [ ! -d "$res_solver_ins" ]; then + # mkdir -p $res_solver_ins + # fi + # for dir_file in `cat $instance/vbs.txt` + # do + # file=$dir_file + # echo $file + # touch $res_solver_ins/$file + # read -u 6 + # { + # cd /home/chenzh/solvers/Light + # time ./light-v1-1 $instance/$file --simplify=0 --reset=1 + # echo >&6 + # } >$res_solver_ins/$file 2>>$res_solver_ins/$file & + # done + + # res_solver_ins=$res2 + # if [ ! -d "$res_solver_ins" ]; then + # mkdir -p $res_solver_ins + # fi + # for dir_file in `cat $instance/vbs.txt` + # do + # file=$dir_file + # echo $file + # touch $res_solver_ins/$file + # read -u 6 + # { + # cd /home/chenzh/solvers/Light + # time ./light-v4-1 $instance/$file --simplify=1 + # echo >&6 + # } >$res_solver_ins/$file 2>>$res_solver_ins/$file & + # done + + # res_solver_ins=$res1 + # if [ ! -d "$res_solver_ins" ]; then + # mkdir -p $res_solver_ins + # fi + # for dir_file in `cat $instance/vbs.txt` + # do + # file=$dir_file + # echo $file + # touch $res_solver_ins/$file + # read -u 6 + # { + # cd /home/chenzh/solvers/Light + # time ./light-v1 $instance/$file --simplify=0 + # echo >&6 + # } >$res_solver_ins/$file 2>>$res_solver_ins/$file & + # done +done + +res_solver_ins=$res_no +if [ ! -d "$res_solver_ins" ]; then + mkdir -p $res_solver_ins +fi +for((i=0;i<4;i++)) +do + read -u 6 + { + cd /home/chenzh/solvers/Light + time ./light-v1 /home/chenzh/data/hard_cnfs/49.cnf + echo >&6 + } >$res_solver_ins/$i 2>>$res_solver_ins/$i & +done + + +exit 0 diff --git a/testLight/run7-1.sh b/testLight/run7-1.sh new file mode 100755 index 0000000..0bc3a6a --- /dev/null +++ b/testLight/run7-1.sh @@ -0,0 +1,150 @@ +#!/bin/bash + +SEND_THREAD_NUM=4 +tmp_fifofile="/tmp/$$.fifo" # 脚本运行的当前进程ID号作为文件名 +mkfifo "$tmp_fifofile" # 新建一个随机fifo管道文件 +exec 6<>"$tmp_fifofile" # 定义文件描述符6指向这个fifo管道文件 +rm $tmp_fifofile +for i in $(seq 1 $SEND_THREAD_NUM) +do + echo # for循环 往 fifo管道文件中写入 $SEND_THREAD_NUM 个空行 +done >&6 + +# CUTOFF_TIME=3600 +instance_20="/pub/data/chenzh/data/sat2020" +instance_21="/pub/data/chenzh/data/sat2021" +instance_22="/pub/data/chenzh/data/sat2022" + + +res1="/pub/data/chenzh/res/light/v1-origin" +res2="/pub/data/chenzh/res/light/v4-1-preprocess" +res3="/pub/data/chenzh/res/light/v1-1-origin" +res4="/pub/data/chenzh/res/light/v2-preprocess" +res5="/pub/data/chenzh/res/light/v3--1-preprocess" +res6="/pub/data/chenzh/res/light/v4-2-dps2-r" +res_no="/pub/data/chenzh/res/unused" +##################################################### + +all_datas=($instance_21) +for((i=0;i<${#all_datas[*]};i++)) +do + instance=${all_datas[$i]} + + res_solver_ins=$res6 + if [ ! -d "$res_solver_ins" ]; then + mkdir -p $res_solver_ins + fi + for dir_file in `cat $instance/vbs.txt` + do + file=$dir_file + echo $file + touch $res_solver_ins/$file + read -u 6 + { + cd /home/chenzh/solvers/Light + time ./light-v4-2 $instance/$file --share=1 --DPS=1 --DPS_period=20000 --share_lits=3000 + echo >&6 + } >$res_solver_ins/$file 2>>$res_solver_ins/$file & + done + + # res_solver_ins=$res5 + # if [ ! -d "$res_solver_ins" ]; then + # mkdir -p $res_solver_ins + # fi + # for dir_file in `cat $instance/vbs.txt` + # do + # file=$dir_file + # echo $file + # touch $res_solver_ins/$file + # read -u 6 + # { + # cd /home/chenzh/solvers/Light + # time ./light-v3--1 $instance/$file --share=1 --threads=31 + # echo >&6 + # } >$res_solver_ins/$file 2>>$res_solver_ins/$file & + # done + # res_solver_ins=$res4 + # if [ ! -d "$res_solver_ins" ]; then + # mkdir -p $res_solver_ins + # fi + # for dir_file in `cat $instance/vbs.txt` + # do + # file=$dir_file + # echo $file + # touch $res_solver_ins/$file + # read -u 6 + # { + # cd /home/chenzh/solvers/Light + # time ./light-v2 $instance/$file --share=1 --threads=31 + # echo >&6 + # } >$res_solver_ins/$file 2>>$res_solver_ins/$file & + # done + + # res_solver_ins=$res3 + # if [ ! -d "$res_solver_ins" ]; then + # mkdir -p $res_solver_ins + # fi + # for dir_file in `cat $instance/vbs.txt` + # do + # file=$dir_file + # echo $file + # touch $res_solver_ins/$file + # read -u 6 + # { + # cd /home/chenzh/solvers/Light + # time ./light-v1-1 $instance/$file --simplify=0 --reset=1 + # echo >&6 + # } >$res_solver_ins/$file 2>>$res_solver_ins/$file & + # done + + # res_solver_ins=$res2 + # if [ ! -d "$res_solver_ins" ]; then + # mkdir -p $res_solver_ins + # fi + # for dir_file in `cat $instance/vbs.txt` + # do + # file=$dir_file + # echo $file + # touch $res_solver_ins/$file + # read -u 6 + # { + # cd /home/chenzh/solvers/Light + # time ./light-v4-1 $instance/$file --simplify=1 + # echo >&6 + # } >$res_solver_ins/$file 2>>$res_solver_ins/$file & + # done + + # res_solver_ins=$res1 + # if [ ! -d "$res_solver_ins" ]; then + # mkdir -p $res_solver_ins + # fi + # for dir_file in `cat $instance/vbs.txt` + # do + # file=$dir_file + # echo $file + # touch $res_solver_ins/$file + # read -u 6 + # { + # cd /home/chenzh/solvers/Light + # time ./light-v1 $instance/$file --simplify=0 + # echo >&6 + # } >$res_solver_ins/$file 2>>$res_solver_ins/$file & + # done +done + +res_solver_ins=$res_no +if [ ! -d "$res_solver_ins" ]; then + mkdir -p $res_solver_ins +fi +for((i=0;i<4;i++)) +do + read -u 6 + { + cd /home/chenzh/solvers/Light + time ./light-v1 /home/chenzh/data/hard_cnfs/49.cnf + echo >&6 + } >$res_solver_ins/$i 2>>$res_solver_ins/$i & +done + + +exit 0 diff --git a/testLight/run7-2.sh b/testLight/run7-2.sh new file mode 100755 index 0000000..4e48633 --- /dev/null +++ b/testLight/run7-2.sh @@ -0,0 +1,150 @@ +#!/bin/bash + +SEND_THREAD_NUM=4 +tmp_fifofile="/tmp/$$.fifo" # 脚本运行的当前进程ID号作为文件名 +mkfifo "$tmp_fifofile" # 新建一个随机fifo管道文件 +exec 6<>"$tmp_fifofile" # 定义文件描述符6指向这个fifo管道文件 +rm $tmp_fifofile +for i in $(seq 1 $SEND_THREAD_NUM) +do + echo # for循环 往 fifo管道文件中写入 $SEND_THREAD_NUM 个空行 +done >&6 + +# CUTOFF_TIME=3600 +instance_20="/pub/data/chenzh/data/sat2020" +instance_21="/pub/data/chenzh/data/sat2021" +instance_22="/pub/data/chenzh/data/sat2022" + + +res1="/pub/data/chenzh/res/light/v1-origin" +res2="/pub/data/chenzh/res/light/v4-1-preprocess" +res3="/pub/data/chenzh/res/light/v1-1-origin" +res4="/pub/data/chenzh/res/light/v2-preprocess" +res5="/pub/data/chenzh/res/light/v3--1-preprocess" +res6="/pub/data/chenzh/res/light/v4-2-dps2-r" +res_no="/pub/data/chenzh/res/unused" +##################################################### + +all_datas=($instance_20) +for((i=0;i<${#all_datas[*]};i++)) +do + instance=${all_datas[$i]} + + res_solver_ins=$res6 + if [ ! -d "$res_solver_ins" ]; then + mkdir -p $res_solver_ins + fi + for dir_file in `cat $instance/vbs.txt` + do + file=$dir_file + echo $file + touch $res_solver_ins/$file + read -u 6 + { + cd /home/chenzh/solvers/Light + time ./light-v4-2 $instance/$file --share=1 --DPS=1 --DPS_period=20000 --share_lits=3000 + echo >&6 + } >$res_solver_ins/$file 2>>$res_solver_ins/$file & + done + + # res_solver_ins=$res5 + # if [ ! -d "$res_solver_ins" ]; then + # mkdir -p $res_solver_ins + # fi + # for dir_file in `cat $instance/vbs.txt` + # do + # file=$dir_file + # echo $file + # touch $res_solver_ins/$file + # read -u 6 + # { + # cd /home/chenzh/solvers/Light + # time ./light-v3--1 $instance/$file --share=1 --threads=31 + # echo >&6 + # } >$res_solver_ins/$file 2>>$res_solver_ins/$file & + # done + # res_solver_ins=$res4 + # if [ ! -d "$res_solver_ins" ]; then + # mkdir -p $res_solver_ins + # fi + # for dir_file in `cat $instance/vbs.txt` + # do + # file=$dir_file + # echo $file + # touch $res_solver_ins/$file + # read -u 6 + # { + # cd /home/chenzh/solvers/Light + # time ./light-v2 $instance/$file --share=1 --threads=31 + # echo >&6 + # } >$res_solver_ins/$file 2>>$res_solver_ins/$file & + # done + + # res_solver_ins=$res3 + # if [ ! -d "$res_solver_ins" ]; then + # mkdir -p $res_solver_ins + # fi + # for dir_file in `cat $instance/vbs.txt` + # do + # file=$dir_file + # echo $file + # touch $res_solver_ins/$file + # read -u 6 + # { + # cd /home/chenzh/solvers/Light + # time ./light-v1-1 $instance/$file --simplify=0 --reset=1 + # echo >&6 + # } >$res_solver_ins/$file 2>>$res_solver_ins/$file & + # done + + # res_solver_ins=$res2 + # if [ ! -d "$res_solver_ins" ]; then + # mkdir -p $res_solver_ins + # fi + # for dir_file in `cat $instance/vbs.txt` + # do + # file=$dir_file + # echo $file + # touch $res_solver_ins/$file + # read -u 6 + # { + # cd /home/chenzh/solvers/Light + # time ./light-v4-1 $instance/$file --simplify=1 + # echo >&6 + # } >$res_solver_ins/$file 2>>$res_solver_ins/$file & + # done + + # res_solver_ins=$res1 + # if [ ! -d "$res_solver_ins" ]; then + # mkdir -p $res_solver_ins + # fi + # for dir_file in `cat $instance/vbs.txt` + # do + # file=$dir_file + # echo $file + # touch $res_solver_ins/$file + # read -u 6 + # { + # cd /home/chenzh/solvers/Light + # time ./light-v1 $instance/$file --simplify=0 + # echo >&6 + # } >$res_solver_ins/$file 2>>$res_solver_ins/$file & + # done +done + +res_solver_ins=$res_no +if [ ! -d "$res_solver_ins" ]; then + mkdir -p $res_solver_ins +fi +for((i=0;i<4;i++)) +do + read -u 6 + { + cd /home/chenzh/solvers/Light + time ./light-v1 /home/chenzh/data/hard_cnfs/49.cnf + echo >&6 + } >$res_solver_ins/$i 2>>$res_solver_ins/$i & +done + + +exit 0 diff --git a/testLight/run7_1.sh b/testLight/run8-1.sh similarity index 94% rename from testLight/run7_1.sh rename to testLight/run8-1.sh index 184b453..10d5229 100755 --- a/testLight/run7_1.sh +++ b/testLight/run8-1.sh @@ -21,9 +21,7 @@ res2="/pub/data/chenzh/res/light/v1-preprocess-2" res3="/pub/data/chenzh/res/light/v1-1-origin" res4="/pub/data/chenzh/res/light/v2-preprocess" res5="/pub/data/chenzh/res/light/v3--1-preprocess" -res6="/pub/data/chenzh/res/light/v4-nps" -res7="/pub/data/chenzh/res/light/v4-dps" -res8="/pub/data/chenzh/res/light/v4-dps-2w" +res6="/pub/data/chenzh/res/light/v4-1-nps2" res_no="/pub/data/chenzh/res/unused" ##################################################### @@ -31,8 +29,9 @@ all_datas=($instance_21 $instance_20) for((i=0;i<${#all_datas[*]};i++)) do instance=${all_datas[$i]} - - res_solver_ins=$res8 + + + res_solver_ins=$res6 if [ ! -d "$res_solver_ins" ]; then mkdir -p $res_solver_ins fi @@ -44,7 +43,7 @@ do read -u 6 { cd /home/chenzh/solvers/Light - time ./light-v4 $instance/$file --share=1 --DPS=1 --DPS_period=20000 + time ./light-v4-2 $instance/$file --share=1 echo >&6 } >$res_solver_ins/$file 2>>$res_solver_ins/$file & done diff --git a/testLight/run7_2.sh b/testLight/run8-2.sh similarity index 93% rename from testLight/run7_2.sh rename to testLight/run8-2.sh index 758a7c3..8dccbd5 100755 --- a/testLight/run7_2.sh +++ b/testLight/run8-2.sh @@ -21,9 +21,7 @@ res2="/pub/data/chenzh/res/light/v1-preprocess-2" res3="/pub/data/chenzh/res/light/v1-1-origin" res4="/pub/data/chenzh/res/light/v2-preprocess" res5="/pub/data/chenzh/res/light/v3--1-preprocess" -res6="/pub/data/chenzh/res/light/v4-nps" -res7="/pub/data/chenzh/res/light/v4-dps" -res8="/pub/data/chenzh/res/light/v4-dps-2w" +res6="/pub/data/chenzh/res/light/v4-1-nps2" res_no="/pub/data/chenzh/res/unused" ##################################################### @@ -31,12 +29,13 @@ all_datas=($instance_22) for((i=0;i<${#all_datas[*]};i++)) do instance=${all_datas[$i]} - - res_solver_ins=$res8 + + + res_solver_ins=$res6 if [ ! -d "$res_solver_ins" ]; then mkdir -p $res_solver_ins fi - for dir_file in `cat $instance/vbs.txt` + for dir_file in `cat $instance/all.txt` do file=$dir_file echo $file @@ -44,7 +43,7 @@ do read -u 6 { cd /home/chenzh/solvers/Light - time ./light-v4 $instance/$file --share=1 --DPS=1 --DPS_period=20000 + time ./light-v4-2 $instance/$file --share=1 echo >&6 } >$res_solver_ins/$file 2>>$res_solver_ins/$file & done diff --git a/utils/hashmap.o b/utils/hashmap.o deleted file mode 100644 index bbde904..0000000 Binary files a/utils/hashmap.o and /dev/null differ diff --git a/utils/paras.o b/utils/paras.o deleted file mode 100644 index 6638c09..0000000 Binary files a/utils/paras.o and /dev/null differ diff --git a/utils/parse.cpp b/utils/parse.cpp index 9c1a0ae..e0e7c19 100644 --- a/utils/parse.cpp +++ b/utils/parse.cpp @@ -87,3 +87,14 @@ void preprocess::readfile(const char *file) { } delete []data; } + +void preprocess::write_cnf() { + printf("p cnf %d %d\n", vars, clauses); + for (int i = 1; i <= clauses; i++) { + int l = clause[i].size(); + for (int j = 0; j < l; j++) { + printf("%d ", clause[i][j]); + } + puts("0"); + } +} diff --git a/utils/parse.o b/utils/parse.o deleted file mode 100644 index 7ae9cca..0000000 Binary files a/utils/parse.o and /dev/null differ diff --git a/workers/basekissat.o b/workers/basekissat.o deleted file mode 100644 index 4129673..0000000 Binary files a/workers/basekissat.o and /dev/null differ diff --git a/workers/sharer.o b/workers/sharer.o deleted file mode 100644 index 25a7b28..0000000 Binary files a/workers/sharer.o and /dev/null differ