同步代码

experiment/cal.py

@@ -104,15 +104,24 @@ class solver_SAT_standard_gnomon(solver):
                 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"):
 
-                timestr = re.findall(r"real\s+(\d+\.\d+)", fstr)[-1]
+                if "mallob" in self.print_name:
+                    timestr = re.findall(r"real.*m.*s", fstr)[-1]
+                    minute = int(timestr.split('m')[0].split()[-1])
+                    second = float(timestr.split('m')[-1].split('s')[0])
+                    self.datas[ins_name].time = minute * 60 + second
+                else:
+                    timestr = re.findall(r"real\s+(\d+\.\d+)", fstr)[-1]
+                    self.datas[ins_name].time = float(timestr)
 
                 # timestr = re.findall(r"real.*m.*s", fstr)[-1]
                 # minute = int(timestr.split('m')[0].split()[-1])
                 # second = float(timestr.split('m')[-1].split('s')[0])
-                self.datas[ins_name].time = float(timestr)
+                
                 if (self.datas[ins_name].time > CUTOFF*PUNISH):
                     self.datas[ins_name].res="unknown"
                 # confstr = re.findall(r"c conflicts:.*per second", fstr)[-1]
@@ -205,6 +214,7 @@ class calculater(object):
             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
@@ -223,7 +233,6 @@ class calculater(object):
                                 slv.datas[ins_name].mono = True
                                 slv.mono_num += 1    
 
-
                 line = ""
                 no_answer       = True
                 answer_this     = "unknown"
@@ -241,12 +250,12 @@ class calculater(object):
                 if(not all_can_solve and not no_answer):
                     have_diff_res = True
 
-                # if(True):
+                if(True):
-                if(False):
+                # if(False):
                 # if(no_answer):
                 # if(all_can_solve):
                 # if(have_diff_res):
-                # if(have_diff_res and answer_this == "sat"):
+                # if(have_diff_res):
                 # if(self.solvers[-2].datas[ins_name].res != self.solvers[-1].datas[ins_name].res):
                     print_line_ct += 1
                     print(line)
@@ -274,23 +283,33 @@ def gen_samples(dir):
 if __name__ == "__main__":
     solvers = []
     # solvers.append(solver_SAT_standard_gnomon("/pub/netdisk1/qianyh/aws-batch-comp-infrastructure-sample/docker/runner/exp-result","mallob"))
-    solvers.append(solver_SAT_standard_gnomon("./light-3m-v3-tree","light-3m-v3-tree"))
+
-    solvers.append(solver_SAT_standard_gnomon("./light-3m-v3-circle","light-3m-v3-circle"))
+    # solvers.append(solver_SAT_standard_gnomon("./atest/light-07a2-result","light-07a2"))
-    solvers.append(solver_SAT_standard_gnomon("./light-3m-v2-tree","light-3m-v2-tree"))
+    # solvers.append(solver_SAT_standard_gnomon("./atest/light-6380-result","light-6380"))
-    solvers.append(solver_SAT_standard_gnomon("./light-3m-v2-circle","light-3m-v2-circle"))
+    # solvers.append(solver_SAT_standard_gnomon("./atest/light-a55a-result","light-a55a"))
-    # solvers.append(solver_SAT_standard_gnomon("./light-3m-new-tree","light-3m-new-tree"))
+    # solvers.append(solver_SAT_standard_gnomon("./atest/light-b883-result","light-b883"))
-    # solvers.append(solver_SAT_standard_gnomon("./light-3m-new-circle","light-3m-new-circle"))
+
-    solvers.append(solver_SAT_standard_gnomon("./light-3m-no-pre","light-3m-no-pre"))
+    solvers.append(solver_SAT_standard_gnomon("./cloud-node8-v1-circle","cloud-cr"))
-    solvers.append(solver_SAT_standard_gnomon("./light-3m","light-3m"))
+    # solvers.append(solver_SAT_standard_gnomon("/pub/netdisk1/qianyh/aws-batch-comp-infrastructure-sample/docker/runner/exp-result","mallob"))
-    solvers.append(solver_SAT_standard_gnomon("./light-no-bug","light-no-bug"))
+    # solvers.append(solver_SAT_standard_gnomon("./light-3m-v4-tree","v4-tree"))
-    solvers.append(solver_SAT_standard_gnomon("./light-circle","light-circle"))
+    # solvers.append(solver_SAT_standard_gnomon("./light-3m-v4-circle","v4-ccle"))
-    solvers.append(solver_SAT_standard_gnomon("./light-circle-unique","light-circle-unique"))
+    # solvers.append(solver_SAT_standard_gnomon("./light-3m-v3-tree","3-tree"))
-    solvers.append(solver_SAT_standard_gnomon("./first_version","bug-cloud"))
+    # solvers.append(solver_SAT_standard_gnomon("./light-3m-v3-circle","3-ccle"))
+    # solvers.append(solver_SAT_standard_gnomon("./light-3m-v2-tree","v2-tree"))
+    # solvers.append(solver_SAT_standard_gnomon("./light-3m-v2-circle","v2-ccle"))
+    # solvers.append(solver_SAT_standard_gnomon("./light-3m-new-tree","new-tree"))
+    # solvers.append(solver_SAT_standard_gnomon("./light-3m-new-circle","new-ccle"))
+    # solvers.append(solver_SAT_standard_gnomon("./light-3m-no-pre","no-pre"))
+    # solvers.append(solver_SAT_standard_gnomon("./light-3m","light-3m"))
+    # solvers.append(solver_SAT_standard_gnomon("./light-no-bug","light-nb"))
+    # solvers.append(solver_SAT_standard_gnomon("./light-circle","light-cr"))
+    # solvers.append(solver_SAT_standard_gnomon("./light-circle-unique","light-cu"))
+    # solvers.append(solver_SAT_standard_gnomon("./first_version","bug-c"))
     
     # 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/vbs.txt", "dump_sat"])
+    samples.append(["/pub/netdisk1/qianyh/aws-batch-comp-infrastructure-sample/docker/runner/sat2022/satvbs.txt", "dump_sat"])
     # samples.append(["./nohup.log", "dump_sat"])
     clt = calculater(solvers, samples)
     clt.cal_and_show()

hostfile

@@ -1,2 +1,5 @@
-192.168.100.6
+192.168.100.6 slots=9
-192.168.100.9
+192.168.100.7 slots=8
+192.168.100.9 slots=8
+192.168.100.10 slots=8
+192.168.100.12 slots=8

kissat-inc/makefile

@@ -1,17 +1,17 @@
 all:
-	$(MAKE) -C "/home/chenzh/solvers/cloud-sat/kissat-inc/build"
+	$(MAKE) -C "/pub/netdisk1/qianyh/Light/kissat-inc/build"
 kissat:
-	$(MAKE) -C "/home/chenzh/solvers/cloud-sat/kissat-inc/build" kissat
+	$(MAKE) -C "/pub/netdisk1/qianyh/Light/kissat-inc/build" kissat
 tissat:
-	$(MAKE) -C "/home/chenzh/solvers/cloud-sat/kissat-inc/build" tissat
+	$(MAKE) -C "/pub/netdisk1/qianyh/Light/kissat-inc/build" tissat
 clean:
-	rm -f "/home/chenzh/solvers/cloud-sat/kissat-inc"/makefile
+	rm -f "/pub/netdisk1/qianyh/Light/kissat-inc"/makefile
-	-$(MAKE) -C "/home/chenzh/solvers/cloud-sat/kissat-inc/build" clean
+	-$(MAKE) -C "/pub/netdisk1/qianyh/Light/kissat-inc/build" clean
-	rm -rf "/home/chenzh/solvers/cloud-sat/kissat-inc/build"
+	rm -rf "/pub/netdisk1/qianyh/Light/kissat-inc/build"
 coverage:
-	$(MAKE) -C "/home/chenzh/solvers/cloud-sat/kissat-inc/build" coverage
+	$(MAKE) -C "/pub/netdisk1/qianyh/Light/kissat-inc/build" coverage
 indent:
-	$(MAKE) -C "/home/chenzh/solvers/cloud-sat/kissat-inc/build" indent
+	$(MAKE) -C "/pub/netdisk1/qianyh/Light/kissat-inc/build" indent
 test:
-	$(MAKE) -C "/home/chenzh/solvers/cloud-sat/kissat-inc/build" test
+	$(MAKE) -C "/pub/netdisk1/qianyh/Light/kissat-inc/build" test
 .PHONY: all clean coverage indent kissat test tissat

mpitutorial

@@ -0,0 +1 @@
+Subproject commit dc1dd4f6b508fe97963844cb5adc3f9cd822f57c

run.sh

@@ -6,19 +6,9 @@
 
 #make -j 16 && mpirun --bind-to none -np 9 --allow-run-as-root ./light -i /pub/data/chenzh/data/sat2022/0205e0724a8a912dde9ad7dfba2aee0b-003-23-80.cnf --share=1 --threads=32 --times=3600
 
-# 这个200s 退出了
-# 03bb7baaa45980753a0e7050ae44755d-atco_enc3_opt1_03_53.cnf
 
-# preprocess 占了特别大内存
+# 退出慢
-
+# 0823bc5f954c6366702877556f0d3680-linked_list_swap_contents_safety_unwind66.cnf
-
-
-# 有BUG
-# 04157f716c1e9606c6a530657bf8f957-Kakuro-easy-125-ext.xml.hg_4.cnf
-
-
-#每次都有BUG
-# 3d2a6e5c2f8f58dee79fd50444009625-cfi-rigid-z2-0088-03-or_2_shuffle_all.cnf
 
 
 # cd kissat-inc
@@ -30,10 +20,10 @@
 
 # 这个存在问题
 DIR=/pub/data/chenzh/data/sat2022
-INSTANCE=3d2a6e5c2f8f58dee79fd50444009625-cfi-rigid-z2-0088-03-or_2_shuffle_all.cnf
+INSTANCE=807133f4461a11e39a390dfcf67a4fc6-summle_X11113_steps8_I1-2-2-4-4-8-25-100.cnf
 
-# make -j 16 && mpirun --bind-to none -np 9 --allow-run-as-root ./light -i $DIR/$INSTANCE --shuffle=1 --share=1 --threads=16 --times=3600 --share_method=1
+# make -j 16 && mpirun --mca btl_tcp_if_include 192.168.100.0/24 --bind-to none -np 65 --hostfile hostfile --allow-run-as-root  ./light -i $DIR/$INSTANCE --share=1 --threads=16 --times=1000 --share_method=0
 
-make -j 16 && mpirun --bind-to none -np 9 --allow-run-as-root ./light -i ./data/hard1.cnf --share=1 --threads=16 --times=10
+make -j 16 && mpirun --bind-to none -np 9 --allow-run-as-root valgrind ./light -i $DIR/$INSTANCE --share=1 --threads=16 --times=1000 --share_method=0
 
 #./light -i $DIR/$INSTANCE --share=1 --threads=16 --times=3600

src/clause.hpp

@@ -9,6 +9,7 @@ using std::shared_ptr;
 struct clause_store {
     int size, lbd;
     int *data;
+    int delete1;
     std::atomic<int> refs;
     clause_store(int sz) {
         //printf("c new clause_store\n");
@@ -16,6 +17,8 @@ struct clause_store {
         data = (int*) malloc(sizeof(int) * sz);
         lbd = 0;
         refs = 1;
+
+        delete1 = 0;
     }
     void increase_refs(int inc) {
         refs += inc;
@@ -46,12 +49,15 @@ struct clause_store {
         //     free(data);
         //     return true;
         // }
+
         return false;
     }
     ~clause_store() {
-        //printf("c free clause_store\n");
+        // printf("c free clause_store\n");
         free(data);
+        delete1 = 1;
     }
+
 };
 
 #endif

src/sharer.cpp

@@ -56,6 +56,7 @@ void sharer::share_clauses_to_other_node(int from, const std::vector<shared_ptr<
     }
 
     assert(index == send_length);
+    assert(send_length <= BUF_SIZE);
 
     // 调用 MPI 发送共享子句
 
@@ -80,7 +81,7 @@ void sharer::share_clauses_to_other_node(int from, const std::vector<shared_ptr<
         // 环形传递
         MPI_Isend(send_buf.get(), send_length, MPI_INT, next_node, SHARE_CLAUSES_TAG, MPI_COMM_WORLD, send_request);
         send_data_struct.push_back(std::make_pair(send_request, send_buf));
-    }    
+    }
 
     // printf("c [worker] send clauses: %d\n", send_length);
 
@@ -117,6 +118,8 @@ int sharer::receive_clauses_from_other_node(std::vector<shared_ptr<clause_store>
     int count;
     MPI_Get_count(&status, MPI_INT, &count);
 
+    // /printf("================= %d\n", count);
+
     transmitter = status.MPI_SOURCE;
 
     from = buf[index++];
@@ -168,7 +171,6 @@ void sharer::clause_sharing_init(std::vector<std::vector<int>> &sharing_groups)
     }
 
     MPI_Irecv(buf, BUF_SIZE, MPI_INT, MPI_ANY_SOURCE, SHARE_CLAUSES_TAG, MPI_COMM_WORLD, &receive_request);
-
 }
 
 void sharer::clause_sharing_end() {
@@ -194,7 +196,21 @@ void sharer::do_clause_sharing() {
     int from;
 
     int received_lits = 0;
-    while((from = receive_clauses_from_other_node(clauses, transmitter)) != -1 &&clauses.size() > 0) {
+    while((from = receive_clauses_from_other_node(clauses, transmitter)) != -1 && clauses.size() > 0) {
+
+        for(auto &c : clauses) {
+            for(int j=0; j<c->size; j++) {
+                if(abs(c->data[j]) > 30438) {
+                    printf("FUCK!!!!    outner");
+                    printf("clasue: [ ");
+                    for(int j=0; j<c->size; j++) {
+                        printf("%d " , c->data[j]);
+                    }
+                    printf("]\n");
+                    exit(-1);
+                }
+            }
+        }
 
         for (int j = 0; j < consumers.size(); j++) {
             consumers[j]->import_clauses_from(clauses);
@@ -211,6 +227,11 @@ void sharer::do_clause_sharing() {
 
     printf("c node%d(%d) get %d exported lits from network\n", rank, S->worker_type, received_lits);
 
+
+    // for (int j = 0; j < consumers.size(); j++) {
+    //     consumers[j]->import_clause.size();
+    // }
+
     for (int i = 0; i < producers.size(); i++) {
         cls.clear();
         producers[i]->export_clauses_to(cls);
@@ -235,6 +256,20 @@ void sharer::do_clause_sharing() {
         // 增加 lits 限制
         int percent = sort_clauses(i);
 
+        for(auto &c : cls) {
+            for(int j=0; j<c->size; j++) {
+                if(abs(c->data[j]) > 30438) {
+                    printf("FUCK!!!!    inner");
+                    printf("clasue: [ ");
+                    for(int j=0; j<c->size; j++) {
+                        printf("%d " , c->data[j]);
+                    }
+                    printf("]\n");
+                    exit(-1);
+                }
+            }
+        }
+
         if(S->worker_type != light::SAT) {
             if (percent < 75) {
                 producers[i]->broaden_export_limit();

src/solve.cpp

@@ -259,13 +259,15 @@ void light::seperate_groups() {
     // split distribute nodes to groups(SAT MODE、UNSAT MODE、DEFAULT MODE)
     int worker_procs = num_procs - 1;
 
+    // assert(worker_procs == 64);
+
     if(worker_procs >= 8) {
         int sat_procs = 0;
-        int unsat_procs = 2;
+        int unsat_procs = worker_procs / 4;
         int default_procs = worker_procs - sat_procs - unsat_procs;
 
         std::vector<int> tmp;
-        // [1, sat_procs] for sat
+        // //[1, sat_procs] for sat
         // if(rank >= 1 && rank <= sat_procs) {
         //     worker_type = light::SAT;
         // }

src/solver_api/basekissat.cpp

@@ -65,7 +65,7 @@ void call_back_out(void *solver, int lbd, cvec *c) {
     }
 }
 
-bool basekissat::imp_clause(shared_ptr<clause_store>cls, void *cl) {
+bool basekissat::imp_clause(shared_ptr<clause_store> cls, void *cl) {
     cvec *c = (cvec *) cl;
     for (int i = 0; i < cls->size; i++) {
         // S->outimport << cls->data[i] << std::endl;
@@ -73,7 +73,10 @@ bool basekissat::imp_clause(shared_ptr<clause_store>cls, void *cl) {
 
         assert(eidx > 0);
 
-        if (eidx >= SIZE_STACK(solver->import)) printf("c wrong %d   sizeo_stack %d\n", eidx, SIZE_STACK(solver->import));
+        if (eidx >= SIZE_STACK(solver->import)) { 
+            printf("c wrong %d   sizeo_stack %d\n", eidx, SIZE_STACK(solver->import));
+            printf("delete: %d\n", cls->delete1);
+        }
         import *import = &PEEK_STACK (solver->import, eidx);
 
         if (import->eliminated) return false;
@@ -88,8 +91,10 @@ bool basekissat::imp_clause(shared_ptr<clause_store>cls, void *cl) {
 
 int call_back_in(void *solver, int *lbd, cvec *c) {
     basekissat* S = (basekissat *) solver;
-    shared_ptr<clause_store> cls = NULL;
+    shared_ptr<clause_store> cls;
+
     if (S->import_clause.pop(cls) == false) return -1;
+
     *lbd = cls->lbd;
     bool res = S->imp_clause(cls, c); 
     if (!S->solver->dps) {

src/solver_api/basesolver.cpp

@@ -13,8 +13,9 @@ void basesolver::restrict_export_limit() {
 void basesolver::export_clauses_to(std::vector<shared_ptr<clause_store>> &clauses) {
     shared_ptr<clause_store> cls;
     
-    while (export_clause.pop(cls)) 
+    while (export_clause.pop(cls)) {
         clauses.push_back(cls);
+    }
 }
 
 void basesolver::import_clauses_from(std::vector<shared_ptr<clause_store>> &clauses) {

src/solver_api/basesolver.hpp

@@ -5,6 +5,7 @@
 #include "../utils/vec.hpp"
 #include "../clause.hpp"
 #include <fstream>
+#include <atomic>
 #include <iostream>
 #include <boost/thread.hpp>
 #include <boost/thread/thread.hpp>
@@ -38,8 +39,8 @@ public:
 
     int maxvar, terminated = 0;
 
-    boost::lockfree::spsc_queue<shared_ptr<clause_store>, boost::lockfree::capacity<10240000>> import_clause;
+    boost::lockfree::spsc_queue<shared_ptr<clause_store>, boost::lockfree::capacity<102400000>> import_clause;
-    boost::lockfree::spsc_queue<shared_ptr<clause_store>, boost::lockfree::capacity<10240000>> export_clause;
+    boost::lockfree::spsc_queue<shared_ptr<clause_store>, boost::lockfree::capacity<102400000>> export_clause;
 
     basesolver(int sid, light* light) : id(sid), controller(light) {
         good_clause_lbd = 2;

src/worker.hpp

@@ -16,6 +16,7 @@ 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 have no need to start\n", rank);
         MPI_Barrier(MPI_COMM_WORLD);