diff --git a/light b/light new file mode 100755 index 0000000..d995133 Binary files /dev/null and b/light differ diff --git a/light-v4-1 b/light-v4-1 index 827deb8..0610ae4 100755 Binary files a/light-v4-1 and b/light-v4-1 differ diff --git a/light.o b/light.o new file mode 100644 index 0000000..819f023 Binary files /dev/null and b/light.o differ diff --git a/main.o b/main.o new file mode 100644 index 0000000..98b5cd6 Binary files /dev/null and b/main.o differ diff --git a/preprocess/binary.o b/preprocess/binary.o new file mode 100644 index 0000000..908f5b0 Binary files /dev/null and b/preprocess/binary.o differ diff --git a/preprocess/card.o b/preprocess/card.o new file mode 100644 index 0000000..811a98f Binary files /dev/null and b/preprocess/card.o differ diff --git a/preprocess/gauss.o b/preprocess/gauss.o new file mode 100644 index 0000000..10471f3 Binary files /dev/null and b/preprocess/gauss.o differ diff --git a/preprocess/preprocess.o b/preprocess/preprocess.o new file mode 100644 index 0000000..3b37c02 Binary files /dev/null and b/preprocess/preprocess.o differ diff --git a/preprocess/propagation.o b/preprocess/propagation.o new file mode 100644 index 0000000..f5cccfd Binary files /dev/null and b/preprocess/propagation.o differ diff --git a/preprocess/resolution.o b/preprocess/resolution.o new file mode 100644 index 0000000..18e32c6 Binary files /dev/null and b/preprocess/resolution.o differ diff --git a/solve.cpp b/solve.cpp index 11c5aae..32c3212 100644 --- a/solve.cpp +++ b/solve.cpp @@ -55,7 +55,44 @@ void light::init_workers() { void light::diversity_workers() { for (int i = 0; i < OPT(threads); i++) { - if (i) workers[i]->configure("order_reset", i); + if (OPT(shuffle)) { + if (i) workers[i]->configure("order_reset", i); + } + if (OPT(pakis)) { + if (i == 13 || i == 14 || i == 20 || i == 21) + workers[i]->configure("tier1", 3); + else + workers[i]->configure("tier1", 2); + + if (i == 3 || i == 4 || i == 6 || i == 8 || i == 11 || i == 12 || i == 13 || i == 14 || i == 16 || i == 18 || i == 23) + workers[i]->configure("chrono", 0); + else + workers[i]->configure("chrono", 1); + + if (i == 2 || i == 23) + workers[i]->configure("stable", 0); + else if (i == 6 || i == 16) + workers[i]->configure("stable", 2); + else + workers[i]->configure("stable", 1); + + if (i == 10 || i == 22) + workers[i]->configure("walkinitially", 1); + else + workers[i]->configure("walkinitially", 0); + + if (i == 7 || i == 8 || i == 9 || i == 17 || i == 18 || i == 19 || i == 20) + workers[i]->configure("target", 0); + else if (i == 0 || i == 2 || i == 3 || i == 4 || i == 5 || i == 6 || i == 10 || i == 23) + workers[i]->configure("target", 1); + else + workers[i]->configure("target", 2); + + if (i == 4 || i == 5 || i == 8 || i == 9 || i == 12 || i == 13 || i == 15 || i == 18 || i == 19) + workers[i]->configure("phase", 0); + else + workers[i]->configure("phase", 1); + } } } @@ -119,7 +156,14 @@ int light::solve() { for (int i = 0; i < OPT(threads); i++) { pthread_join(ptr[i], NULL); - } + } + auto clk_now = std::chrono::high_resolution_clock::now(); + double solve_time = std::chrono::duration_cast(clk_now - clk_sol_st).count(); + solve_time = 0.001 * solve_time; + printf("c solve time: %.2lf\n", solve_time); + for (int i = 0; i < OPT(threads); i++) { + printf("c thread %d waiting time: %.2lf\n", i, workers[i]->get_waiting_time()); + } delete []ptr; return result; } diff --git a/solve.o b/solve.o new file mode 100644 index 0000000..d31c326 Binary files /dev/null and b/solve.o differ diff --git a/testLight/cal_solver.py b/testLight/cal_solver.py index 7437800..1c258c0 100644 --- a/testLight/cal_solver.py +++ b/testLight/cal_solver.py @@ -268,15 +268,18 @@ if __name__ == "__main__": solvers = [] - 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-nps","sharing-nps")) - solvers.append(solver_SAT_standard_gnomon("/pub/data/chenzh/res/light/v4-dps","sharing-dps")) + 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/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-dps","sharing-dps")) # append_all_solvers_in_dir(solvers, "/pub/data/chenzh/res/light/") samples = [] samples.append(["/pub/data/chenzh/data/sat2020/vbs.txt", "vbs"]) samples.append(["/pub/data/chenzh/data/sat2021/vbs.txt", "vbs"]) - samples.append(["/pub/data/chenzh/data/sat2022/all.txt", "all"]) + # samples.append(["/pub/data/chenzh/data/sat2022/all.txt", "all"]) clt = calculater(solvers, samples) clt.cal_and_show() diff --git a/testLight/nohup.out b/testLight/nohup.out index 00dae28..e447686 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 new file mode 100755 index 0000000..2c51600 --- /dev/null +++ b/testLight/run4-1.sh @@ -0,0 +1,132 @@ +#!/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" +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=$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/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=$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/run4-2.sh b/testLight/run4-2.sh new file mode 100755 index 0000000..ad42958 --- /dev/null +++ b/testLight/run4-2.sh @@ -0,0 +1,132 @@ +#!/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" +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=$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/run4.sh b/testLight/run4-3.sh similarity index 96% rename from testLight/run4.sh rename to testLight/run4-3.sh index a96b602..6d72265 100755 --- a/testLight/run4.sh +++ b/testLight/run4-3.sh @@ -17,7 +17,7 @@ instance_22="/pub/data/chenzh/data/sat2022" res1="/pub/data/chenzh/res/light/v1-origin" -res2="/pub/data/chenzh/res/light/v1-preprocess" +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" @@ -91,7 +91,7 @@ do read -u 6 { cd /home/chenzh/solvers/Light - time ./light-v1 $instance/$file --simplify=1 + time ./light-v4-1 $instance/$file --simplify=1 echo >&6 } >$res_solver_ins/$file 2>>$res_solver_ins/$file & done diff --git a/testLight/run5.sh b/testLight/run5-1.sh similarity index 96% rename from testLight/run5.sh rename to testLight/run5-1.sh index 39016bc..943338f 100755 --- a/testLight/run5.sh +++ b/testLight/run5-1.sh @@ -21,11 +21,11 @@ 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" +res6="/pub/data/chenzh/res/light/v4-1-nps" res_no="/pub/data/chenzh/res/unused" ##################################################### -all_datas=($instance_21 $instance_20 $instance_22) +all_datas=($instance_21) for((i=0;i<${#all_datas[*]};i++)) do instance=${all_datas[$i]} @@ -42,7 +42,7 @@ do read -u 6 { cd /home/chenzh/solvers/Light - time ./light-v4 $instance/$file --share=1 + time ./light-v4-1 $instance/$file --share=1 echo >&6 } >$res_solver_ins/$file 2>>$res_solver_ins/$file & done diff --git a/testLight/run5-2.sh b/testLight/run5-2.sh new file mode 100755 index 0000000..1ffe09f --- /dev/null +++ b/testLight/run5-2.sh @@ -0,0 +1,151 @@ +#!/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/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-1-nps" +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-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 + # 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 $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/run5-3.sh b/testLight/run5-3.sh new file mode 100755 index 0000000..3b67ac7 --- /dev/null +++ b/testLight/run5-3.sh @@ -0,0 +1,151 @@ +#!/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/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-1-nps" +res_no="/pub/data/chenzh/res/unused" +##################################################### + +all_datas=($instance_22) +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/all.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 + # 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 $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/utils/hashmap.o b/utils/hashmap.o new file mode 100644 index 0000000..bbde904 Binary files /dev/null and b/utils/hashmap.o differ diff --git a/utils/paras.hpp b/utils/paras.hpp index 1c7ed7d..a7604fd 100644 --- a/utils/paras.hpp +++ b/utils/paras.hpp @@ -9,11 +9,13 @@ PARA( DPS , int , 0 , 0 , 1 , "DPS/NPS") \ PARA( DPS_period , int , 10000 , 1 , 1e6 , "DPS sharing period") \ PARA( mode , int , 0 , 0 , 2 , "SAT=1, UNSAT=2") \ + PARA( pakis , int , 0 , 0 , 1 , "Use pakis diversity") \ PARA( reset , int , 0 , 0 , 1 , "Dynamically reseting") \ PARA( reset_time , int , 10 , 1 , 1e5 , "Reseting base interval (seconds)") \ PARA( share , int , 0 , 0 , 1 , "Sharing learnt clauses") \ PARA( share_intv , int , 500000, 0 , 1e9 , "Sharing interval (microseconds)") \ PARA( share_lits , int , 1500 , 0 , 1e6 , "Sharing lits (per every #share_intv seconds)") \ + PARA( shuffle , int , 1 , 0 , 1 , "Use random shuffle") \ PARA( simplify , int , 1 , 0 , 1 , "Use Simplify (only preprocess)") \ PARA( times , double , 5000 , 0 , 1e8 , "Cutoff time") \ PARA( threads , int , 32 , 1 , 128 , "Thread number") \ diff --git a/utils/paras.o b/utils/paras.o new file mode 100644 index 0000000..6638c09 Binary files /dev/null and b/utils/paras.o differ diff --git a/utils/parse.o b/utils/parse.o new file mode 100644 index 0000000..7ae9cca Binary files /dev/null and b/utils/parse.o differ diff --git a/workers/basekissat.cpp b/workers/basekissat.cpp index 7e820d4..0b99d81 100644 --- a/workers/basekissat.cpp +++ b/workers/basekissat.cpp @@ -15,7 +15,7 @@ void basekissat::add(int l) { kissat_add(solver, l); } -void basekissat::configure(char* name, int id) { +void basekissat::configure(const char* name, int id) { kissat_set_option(solver, name, id); } @@ -100,18 +100,21 @@ void kissat_wait_sharing(void *solver) { // printf("c %d start wait with number %d\n", S->id, s->waitings); } if (s->should_sharing()) s->cond.notify_one(); - boost::mutex::scoped_lock lock(s->mtx); while (s->waitings > 0) { s->cond.wait(lock); } - - // auto clk_now = std::chrono::high_resolution_clock::now(); - // int solve_time = std::chrono::duration_cast(clk_now - clk_st).count(); + auto clk_now = std::chrono::high_resolution_clock::now(); + int solve_time = std::chrono::duration_cast(clk_now - clk_st).count(); + S->waiting_time += 0.001 * solve_time; // printf("c %d wait for %d.%03ds\n", S->id, solve_time / 1000, solve_time % 1000); // printf("c %d finish sharing\n", S->id); } +double basekissat::get_waiting_time() { + return waiting_time; +} + basekissat::basekissat(int id, light* light) : basesolver(id, light) { good_clause_lbd = 2; // outexport.open("export.txt"); diff --git a/workers/basekissat.hpp b/workers/basekissat.hpp index 1fe78dc..b7bfb13 100644 --- a/workers/basekissat.hpp +++ b/workers/basekissat.hpp @@ -9,7 +9,7 @@ public: void add(int l); int solve(); int val(int l); - void configure(char* name, int id); + void configure(const char* name, int id); // int get_reset_data(); // void reset(); int get_conflicts(); @@ -22,10 +22,12 @@ public: void import_clauses_from(vec &clauses); void broaden_export_limit(); void restrict_export_limit(); + double get_waiting_time(); basekissat(int id, light *light); ~basekissat(); int x1 = 0, x2 = 0; + double waiting_time = 0; kissat* solver; int good_clause_lbd = 0; diff --git a/workers/basekissat.o b/workers/basekissat.o new file mode 100644 index 0000000..4129673 Binary files /dev/null and b/workers/basekissat.o differ diff --git a/workers/basesolver.hpp b/workers/basesolver.hpp index 0858f91..9b3f287 100644 --- a/workers/basesolver.hpp +++ b/workers/basesolver.hpp @@ -15,7 +15,7 @@ public: virtual int solve() = 0; virtual int val(int l) = 0; virtual void terminate() = 0; - virtual void configure(char* name, int id) = 0; + virtual void configure(const char* name, int id) = 0; virtual int get_conflicts() = 0; virtual void parse_from_CNF(char* filename) = 0; @@ -27,6 +27,7 @@ public: virtual void import_clauses_from(vec &clauses) = 0; virtual void broaden_export_limit() = 0; virtual void restrict_export_limit() = 0; + virtual double get_waiting_time() = 0; light * controller; int id; sharer* in_sharer; diff --git a/workers/sharer.cpp b/workers/sharer.cpp index 0997af6..0581889 100644 --- a/workers/sharer.cpp +++ b/workers/sharer.cpp @@ -9,6 +9,7 @@ void * share_worker(void *arg) { int nums = 0; sharer * sq = (sharer *)arg; auto clk_st = std::chrono::high_resolution_clock::now(); + double share_time = 0; while (true) { ++nums; if (sq->dps) { @@ -55,11 +56,14 @@ void * share_worker(void *arg) { sq->cls[k]->free_clause(); } } + auto clk_ed = std::chrono::high_resolution_clock::now(); + share_time += 0.001 * std::chrono::duration_cast(clk_ed - clk_now).count(); + if (sq->dps) { sq->sharing_finish(); } } - printf("c sharing nums: %d\n", nums); + printf("c sharing nums: %d\nc sharing time: %.2lf\n", nums, share_time); // if (terminated) puts("terminated set to 1"); return NULL; } diff --git a/workers/sharer.o b/workers/sharer.o new file mode 100644 index 0000000..25a7b28 Binary files /dev/null and b/workers/sharer.o differ