同步代码

.gitignore

@@ -2,4 +2,5 @@ build
 .nfs*
 *.o
 myeasylog.log
-light
+light
+exp-result

cal.py

@@ -0,0 +1,267 @@
+#!/usr/bin/python
+# -*- coding: UTF-8 -*-
+
+from multiprocessing import set_forkserver_preload
+import os
+import os.path
+from posixpath import split
+from random import sample
+import re
+import shutil
+from time import monotonic, sleep
+from tokenize import Number
+
+# global limit
+CUTOFF = 5000
+PUNISH = 2 #PAR2
+MEMS_MAX = 61440 # 60G
+
+class states(object):
+    res = "unknown"
+    time = CUTOFF*PUNISH
+    mems = MEMS_MAX
+    mono = False        # only this one can solve
+    best = False        # show the best performance
+    ls_time = 0         # LS_time
+
+class solver(object):
+    def __init__(self, res_dir, name):
+        self.res_dir    = res_dir  # save the results files
+        self.print_name = name     # names want to show
+        self.datas      = dict()   # datas[ins] save the instances
+    def reset(self):
+        # SAT-ins UNSAT-ins solved-ins all-ins
+        self.sat_num = self.unsat_num = self.solved_num = self.all_num = 0
+        self.avg_sat_time = self.avg_unsat_time = self.avg_solved_time = self.avg_all_time = 0.0
+        self.PAR_sat_time = self.PAR_unsat_time = self.PAR_solved_time = self.PAR_all_time = 0.0
+        self.mono_num = 0
+        self.best_num = 0
+    def cal_soln(self, ins_name):
+        self.all_num += 1
+        state = self.datas[ins_name]
+        if(self.datas[ins_name].time > CUTOFF):
+            self.datas[ins_name] = states()
+        if(state.res=="sat"):
+            self.sat_num            += 1
+            self.solved_num         += 1
+            self.avg_sat_time       += state.time
+            self.avg_solved_time    += state.time
+            self.avg_all_time       += state.time
+            self.PAR_sat_time       += state.time
+            self.PAR_solved_time    += state.time
+            self.PAR_all_time       += state.time
+        elif(state.res=="unsat"):
+            self.unsat_num          += 1
+            self.solved_num         += 1
+            self.avg_unsat_time     += state.time
+            self.avg_solved_time    += state.time
+            self.avg_all_time       += state.time
+            self.PAR_unsat_time     += state.time
+            self.PAR_solved_time    += state.time
+            self.PAR_all_time       += state.time
+        else:
+            self.avg_all_time       += CUTOFF
+            self.PAR_all_time       += CUTOFF * PUNISH
+    def deal_avg(self):
+        if(self.sat_num>0):
+            self.avg_sat_time    /= self.sat_num
+            self.PAR_sat_time    /= self.sat_num    
+        if(self.unsat_num>0):
+            self.avg_unsat_time  /= self.unsat_num
+            self.PAR_unsat_time  /= self.unsat_num
+        if(self.solved_num>0):
+            self.avg_solved_time /= self.solved_num
+            self.PAR_solved_time /= self.solved_num
+        if(self.all_num>0):
+            self.avg_all_time    /= self.all_num
+            self.PAR_all_time    /= self.all_num
+    def to_string(self, state):
+        line = ""
+        line += str(state.res) + " "
+        line += str(round(state.time,2))
+        if state.mono:
+            line += "[M]"
+        elif state.best:
+            line += "[B]"
+        # if (state.byCDCL):
+        #     line += "{C}"
+        # elif(state.byLS):
+        #     line += "{L}"
+        line += str()
+        return line.ljust(18)
+
+        return super().to_string(state)
+
+
+class solver_SAT_standard_gnomon(solver):
+    def cal_soln(self, ins_name):
+        if(not ins_name in self.datas):
+            self.datas[ins_name] = states()
+            real_file_path = self.res_dir + "/" + ins_name
+            fstr = open(real_file_path, "r").read()
+                
+            if(not len(re.findall(r"s\s+UNSATISFIABLE", fstr))==0):
+                self.datas[ins_name].res = "unsat"
+            elif(not len(re.findall(r"s\s+SATISFIABLE", fstr))==0):
+                self.datas[ins_name].res = "sat"
+            
+            if(not self.datas[ins_name].res == "unknown"):
+                self.datas[ins_name].time = float(re.findall(r"c process-time:.*seconds", fstr)[0].split()[-2])       
+                if (self.datas[ins_name].time > CUTOFF*PUNISH):
+                    self.datas[ins_name].res="unknown"
+                
+        
+        return super().cal_soln(ins_name)
+    def to_string(self, state):
+        return super().to_string(state)
+
+
+
+
+
+SOLVER_LEN = 20
+SAMPLE_LEN = 20
+NUMBER_LEN = 8
+print_title = True
+class calculater(object):
+    solvers     = []
+    sample_dirs = []    # sample dirs, [sample_dir, sample_name]s
+    def __init__(self, solvers, sample_dirs):
+        self.solvers = solvers
+        self.sample_dirs = sample_dirs
+    def __show_in_mark_down(self, samp_name):
+        global print_title
+        if(print_title):
+            print_title = False
+            title =  "| sample".ljust(SAMPLE_LEN+2)
+            title += " | solver".ljust(SOLVER_LEN+3)
+            title += " | #SAT".ljust(NUMBER_LEN+3)
+            title += " | avg_t".ljust(NUMBER_LEN+3)
+            title += " | #UNSAT".ljust(NUMBER_LEN+3)
+            title += " | avg_t".ljust(NUMBER_LEN+3)
+            title += " | #ALL".ljust(NUMBER_LEN+3)
+            title += " | PAR2_t".ljust(NUMBER_LEN+3)
+            title += " | best".ljust(NUMBER_LEN+3)
+            title += " | mono".ljust(NUMBER_LEN+3)
+            title += " |"
+            print(title)
+
+            split =  "| "  + '-'*(SAMPLE_LEN)
+            split += " | " + '-'*(SOLVER_LEN)
+            split += " | " + '-'*(NUMBER_LEN)
+            split += " | " + '-'*(NUMBER_LEN)
+            split += " | " + '-'*(NUMBER_LEN)
+            split += " | " + '-'*(NUMBER_LEN)
+            split += " | " + '-'*(NUMBER_LEN)
+            split += " | " + '-'*(NUMBER_LEN)
+            split += " | " + '-'*(NUMBER_LEN)
+            split += " | " + '-'*(NUMBER_LEN)
+            split += " |"
+            self.split_line = split
+            print(split)
+
+
+        for slv in self.solvers:
+            line =  "| "  + (samp_name + "("+str(self.sample_ins_ct) + ")").ljust(SAMPLE_LEN)
+            line += " | " + slv.print_name.ljust(SOLVER_LEN)
+            line += " | " + str(slv.sat_num).ljust(NUMBER_LEN)
+            line += " | " + str(round(slv.avg_sat_time,2)).ljust(NUMBER_LEN)
+            line += " | " + str(slv.unsat_num).ljust(NUMBER_LEN)
+            line += " | " + str(round(slv.avg_unsat_time,2)).ljust(NUMBER_LEN)
+            line += " | " + str(slv.solved_num).ljust(NUMBER_LEN)
+            line += " | " + str(round(slv.PAR_all_time,2)).ljust(NUMBER_LEN)
+            line += " | " + str(slv.best_num).ljust(NUMBER_LEN)
+            line += " | " + str(slv.mono_num).ljust(NUMBER_LEN)
+            line += " |"
+            print(line)
+        
+    def cal_and_show(self):
+        for sample in self.sample_dirs:
+            title_line = ""
+            for slv in self.solvers:
+                title_line += slv.print_name.ljust(18)
+            print(title_line)
+            samp_dir  = sample[0]
+            samp_name = sample[1]
+            print_line_ct = 0
+            sample_ins_ct = 0
+            for slv in self.solvers:
+                slv.reset()
+            for ins_name in open(samp_dir):
+                sample_ins_ct += 1
+                ins_name = ins_name.strip()
+                best_time = CUTOFF*PUNISH
+                solved_ct = 0
+                for slv in self.solvers:
+                    slv.cal_soln(ins_name)
+                    best_time = min(slv.datas[ins_name].time, best_time)
+                    if not slv.datas[ins_name].res == "unknown":
+                        solved_ct += 1
+                if(not best_time == CUTOFF*PUNISH):
+                    for slv in self.solvers:
+                        if(slv.datas[ins_name].time == best_time):
+                            slv.datas[ins_name].best = True
+                            slv.best_num += 1
+                            if(solved_ct == 1):
+                                slv.datas[ins_name].mono = True
+                                slv.mono_num += 1    
+
+
+                line = ""
+                no_answer       = True
+                answer_this     = "unknown"
+                all_can_solve   = True
+                have_diff_res   = False
+                for slv in self.solvers:
+                    stt = slv.datas[ins_name]
+                    line += slv.to_string(stt)
+                    if(not stt.res == "unknown"):
+                        no_answer = False
+                        answer_this = stt.res
+                    elif(stt.res == "unknown"):
+                        all_can_solve = False
+                line += ins_name
+                if(not all_can_solve and not no_answer):
+                    have_diff_res = True
+
+                if(True):
+                # if(False):
+                # if(no_answer):
+                # if(all_can_solve):
+                # if(have_diff_res):
+                # if(answer_this == "sat"):
+                # if(self.solvers[-2].datas[ins_name].res != self.solvers[-1].datas[ins_name].res):
+                    print_line_ct += 1
+                    print(line)
+            
+            self.sample_ins_ct = sample_ins_ct
+            for slv in self.solvers:
+                slv.deal_avg() 
+            self.__show_in_mark_down(samp_name)
+            if(print_line_ct>0):
+                print("print line ct = ", print_line_ct)
+            else:
+                print(self.split_line)
+
+
+def gen_samples(dir):
+    samples = []
+    for root, dirs, files in os.walk(dir):
+        for file in files:
+            sample_name = file.strip(".txt")
+            sample_dir = os.path.join(root, file) 
+            # print(sample_dir, sample_name)
+            samples.append([sample_dir, sample_name])
+    return samples
+
+if __name__ == "__main__":
+    solvers = []
+    solvers.append(solver_SAT_standard_gnomon("./exp-result","light-cloud-circle"))
+    # solvers.append(solver_SAT_standard_gnomon("/pub/data/chenzh/res/huawei_sat/kissat-mab","origin-mab"))
+    # solvers.append(solver_SAT_standard_gnomon("/pub/data/chenzh/res/huawei_simp/kissat-mab","preprocess-mab"))
+    samples = []
+    samples.append(["/pub/data/chenzh/data/sat2022/all.txt", "dump_sat"])
+    clt = calculater(solvers, samples)
+    clt.cal_and_show()
+
+

makefile

@@ -6,7 +6,7 @@ OBJECTS := $(addprefix build/,$(SOURCES:%=%.o))
 
 # 声明编译器和编译选项
 CXX := mpicxx
-CXXFLAGS := -O0 -Wall -Wextra -MMD -MP -g
+CXXFLAGS := -O3 -Wall -Wextra -MMD -MP -flto
 
 LIBS := -Wl,-Bstatic -lkissat -L kissat-inc/build -I kissat-inc/ \
 	    -lm4ri -L m4ri-20140914/.libs -I m4ri-20140914/ \

run.sh

@@ -4,4 +4,4 @@
 
 #valgrind
 
-make -j 16 && mpirun -np 9 --allow-run-as-root ./light -i data/WS_500_16_70_10.apx_0.cnf --share=1 --threads=32 --times=1000
+make -j 16 && mpirun -np 9 --allow-run-as-root ./light -i /pub/data/chenzh/data/sat2022/0205e0724a8a912dde9ad7dfba2aee0b-003-23-80.cnf --share=1 --threads=32 --times=3600

run_solvers.sh

@@ -0,0 +1,61 @@
+#!/bin/bash
+
+SEND_THREAD_NUM=1
+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
+
+instance1="/pub/data/chenzh/data/sat2022"
+
+res_sat1="./exp-result"
+
+res_no="./unused"
+#####################################################
+
+ulimit -t 3600
+
+all_datas=($instance1)
+res_dir=($res_sat1)
+for((i=0;i<${#all_datas[*]};i++))
+do
+	instance=${all_datas[$i]}
+	res_solver_ins=${res_dir[$i]}
+	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/qianyh/projects/Light
+			mpirun -np 9 --allow-run-as-root ./light -i $instance/$file --share=1 --threads=32 --times=$CUTOFF_TIME
+			echo >&6
+		} >$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<96;i++))
+# do
+# 	read -u 6
+# 	{
+# 		cd /home/chenzh/solvers/sota/kissat-MAB/build
+# 		./kissat /home/chenzh/data/hard_cnfs/49.cnf
+# 		echo >&6
+# 	} >$res_solver_ins/$i &
+# done
+
+exit 0

src/distributed/leader.hpp

@@ -103,14 +103,14 @@ void leader_main(light* S, int num_procs, int rank) {
             if(is_sat) {
                 res = 10;
                 printf("c [leader] received model size: %d\n", pre->vars);
-                printf("c SAT!!!!!!\n");
+                // printf("c SAT!!!!!!\n");
 
                 MPI_Send(NULL, 0, MPI_INT, status.MPI_SOURCE, MODEL_REPORT_TAG, MPI_COMM_WORLD);
                 sol = new int[pre->vars];
                 MPI_Recv(sol, pre->vars, MPI_INT, status.MPI_SOURCE, MODEL_REPORT_TAG, MPI_COMM_WORLD, MPI_STATUS_IGNORE);
             } else {
                 res = 20;
-                printf("c UNSAT!!!!!!\n");
+                // printf("s UNSATISFIABLE\n");
             }
             break;
         }
@@ -119,18 +119,19 @@ void leader_main(light* S, int num_procs, int rank) {
     MPI_Barrier(MPI_COMM_WORLD);
 
     if(res == 10) {
-        printf("s SAT\n");
+        printf("s SATISFIABLE\n");
         for (int i = 1; i <= pre->orivars; i++)
             if (pre->mapto[i]) pre->mapval[i] = (sol[abs(pre->mapto[i])-1] > 0 ? 1 : -1) * (pre->mapto[i] > 0 ? 1 : -1);
 
         pre->get_complete_model();
+        printf("v ");
         for (int i = 1; i <= pre->orivars; i++) {
             printf("%d ", i * pre->mapval[i]);
         }
         printf("\n");
         delete []sol;
     } else if(res == 20) {
-        printf("s UNSAT\n");
+        printf("s UNSATISFIABLE\n");
     } else {
         printf("s UNKNOWN\n");
     }

src/paras.hpp

@@ -10,10 +10,10 @@
     PARA( DPS        , int    , '\0'  ,  false   , 0     , 0  , 1   , "DPS/NPS") \
     PARA( DPS_period , int    , '\0'  ,  false   , 10000 , 1  , 1e8 , "DPS sharing period") \
     PARA( margin     , int    , '\0'  ,  false   , 0     , 0  , 1e3 , "DPS margin") \
-    PARA( pakis      , int    , '\0'  ,  false   , 0     , 0  , 1   , "Use pakis diversity") \
+    PARA( pakis      , int    , '\0'  ,  false   , 1     , 0  , 1   , "Use pakis diversity") \
     PARA( reset      , int    , '\0'  ,  false   , 0     , 0  , 1   , "Dynamically reseting") \
     PARA( reset_time , int    , '\0'  ,  false   , 10    , 1  , 1e5 , "Reseting base interval (seconds)") \
-    PARA( share      , int    , '\0'  ,  false   , 0     , 0  , 1   , "Sharing learnt clauses") \
+    PARA( share      , int    , '\0'  ,  false   , 1     , 0  , 1   , "Sharing learnt clauses") \
     PARA( share_intv , int    , '\0'  ,  false   , 500000, 0  , 1e9 , "Sharing interval (microseconds)") \
     PARA( share_lits , int    , '\0'  ,  false   , 1500  , 0  , 1e6 , "Sharing lits (per every #share_intv seconds)") \
     PARA( shuffle    , int    , '\0'  ,  false   , 1     , 0  , 1   , "Use random shuffle") \

src/workers/sharer.cpp

@@ -33,7 +33,7 @@ void share_clauses_to_next_node(const vec<clause_store *> &cls) {
             std::swap(send_data_struct[i], send_data_struct[send_data_struct.size()-1]);
             send_data_struct.pop_back();
 
-            printf("c [worker] free send request, now: %d\n", send_data_struct.size());
+            //printf("c [worker] free send request, now: %d\n", send_data_struct.size());
         }
     }
 
@@ -73,7 +73,7 @@ void share_clauses_to_next_node(const vec<clause_store *> &cls) {
 
     send_data_struct.push_back(std::make_pair(send_request, send_buf));
 
-    printf("c [worker] send clauses: %d\n", send_length);
+    //printf("c [worker] send clauses: %d\n", send_length);
 }
 
 bool receive_clauses_from_last_node(vec<clause_store*> &clauses) {
@@ -137,7 +137,7 @@ void sharer::do_clause_sharing() {
     ++nums;
     auto clk_now = std::chrono::high_resolution_clock::now();
     int solve_time = std::chrono::duration_cast<std::chrono::milliseconds>(clk_now - clk_st).count();
-    printf("c [worker] round %d, time: %d.%d\n",  nums, solve_time / 1000, solve_time % 1000);
+    //printf("c [worker] round %d, time: %d.%d\n",  nums, solve_time / 1000, solve_time % 1000);
     // printf("start sharing %d\n", sq->share_intv);
     for (int i = 0; i < producers.size(); i++) {
         cls.clear();
@@ -146,7 +146,7 @@ void sharer::do_clause_sharing() {
         //printf("c size %d\n", sq->cls.size());
         int number = cls.size();
 
-        printf("c [worker] thread-%d: get %d exported clauses\n", i, number);
+        //printf("c [worker] thread-%d: get %d exported clauses\n", i, number);
 
         //分享当前节点产生的子句
         if(cls.size() > 0) share_clauses_to_next_node(cls);