预处理解出不启动worer，到达时间限制自动退出。

docker/run_solver.sh

@@ -1,3 +1,3 @@
 #!/bin/bash
 
-mpirun --host worker1,worker2,worker3 /light -i ./files/class_1_easy_10_0.cnf
+mpirun --host localhost,worker1,worker2,worker3 /light -i ./files/class_1_easy_10_0.cnf

run.sh

@@ -1,3 +1,3 @@
 #!/bin/bash
 
-make -j 16 && mpirun -np 4 --allow-run-as-root ./light -i data/class_1_easy_10_0.cnf --share=1 --threads=4
+make -j 16 && mpirun -q -np 4 --allow-run-as-root ./light -i data/class_1_easy_10_0.cnf --share=1 --threads=4 --times=1

src/distributed/comm_tag.h

@@ -3,4 +3,5 @@
 
 const int TERMINATE_TAG = 0;
 const int SOLVED_REPORT_TAG = 1;
-const int MODEL_REPORT_TAG = 2;
+const int MODEL_REPORT_TAG = 2;
+const int START_TAG = 3;

src/distributed/leader.hpp

@@ -11,11 +11,33 @@
 #include "../paras.hpp"
 #include "heartbeat.h"
 
-preprocess* do_simplify(light* S, std::stringstream &ss) {
-    auto pre = new preprocess();
 
+
+void leader_main(light* S, int num_procs, int rank) {
+
+    auto clk_st = std::chrono::high_resolution_clock::now();
+
+    S->opt->print_change();
+
+    printf("c [leader] preprocess(simplify) input data\n");
+
+    // 进行化简    
+    auto pre = new preprocess();
     char *filename = const_cast<char*>(S->opt->instance.c_str());
-    pre->do_preprocess(filename);
+    int start = pre->do_preprocess(filename);
+
+    // 给每个 worker 发布是否启动计算流程的信息
+    for(int i=1; i<num_procs; i++) {
+        MPI_Send(&start, 1, MPI_INT, i, START_TAG, MPI_COMM_WORLD);
+    }
+
+    // preprocess 证明了UNSAT 则不需要启动云计算
+    if(!start) {
+        printf("UNSAT!!!!!! by preprocess\n");
+        return;
+    }
+
+    std::stringstream ss;
 
     ss << "p cnf " << pre->vars << " " << pre->clause.size() << std::endl;
     for (int i = 1; i <= pre->clauses; i++) {
@@ -25,18 +47,6 @@ preprocess* do_simplify(light* S, std::stringstream &ss) {
         ss << "0" << std::endl;
     }
 
-    return pre;
-}
-
-void leader_main(light* S, int num_procs, int rank) {
-
-    S->opt->print_change();
-
-    printf("c [leader] preprocess(simplify) input data\n");
-
-    //read file
-    std::stringstream ss;
-    preprocess* pre = do_simplify(S, ss);
     const auto& str_ref = ss.str();
     char* cstr = const_cast<char *>(str_ref.c_str());
 
@@ -44,6 +54,8 @@ void leader_main(light* S, int num_procs, int rank) {
 
     int cnf_length = str_ref.size();
 
+    MPI_Barrier(MPI_COMM_WORLD);
+
     MPI_Bcast(&cnf_length, 1, MPI_INT, 0, MPI_COMM_WORLD);
 
     MPI_Barrier(MPI_COMM_WORLD);
@@ -63,8 +75,16 @@ void leader_main(light* S, int num_procs, int rank) {
 
     // waiting for results:
     while(true) {
-        int flag;
+        
+        // 检测时间是否超限
+        auto clk_now = std::chrono::high_resolution_clock::now();
+        int solve_time = std::chrono::duration_cast<std::chrono::seconds>(clk_now - clk_st).count();
+        if (solve_time >= S->opt->times) {
+            printf("c [leader] solve time out\n");
+            break;
+        }
 
+        int flag;
         // check if problem solved
         if(MPI_Test(&solved, &flag, &status) == MPI_SUCCESS && flag == 1) {
 
@@ -99,18 +119,4 @@ void leader_main(light* S, int num_procs, int rank) {
             break;
         }
     }
-
-
-    // printf("[leader] hand out simplified cnf ...\n");
-
-    // HeartBeat *hb = new HeartBeat(num_procs); 
-
-    // printf("[leader] waiting for connection...\n");
-    // hb->waiting_all();
-
-    // for(int i=1; i<=10; i++) {
-    //     printf("[leader] check: %d\n", i);
-    //     hb->update();
-    //     std::this_thread::sleep_for(std::chrono::seconds(1));
-    // }
 }

src/distributed/worker.hpp

@@ -11,6 +11,16 @@
 
 void worker_main(light* S, int num_procs, int rank) {
 
+    auto clk_st = std::chrono::high_resolution_clock::now();
+
+    // 阻塞接收初始化信号
+    int start;
+    MPI_Recv(&start, 1, MPI_INT, 0, START_TAG, MPI_COMM_WORLD, MPI_STATUS_IGNORE);
+    if(!start) {
+        printf("c worker%d has no need to start\n", rank);
+        return;
+    }
+
     // 监听 terminate 信号
     MPI_Irecv(NULL, 0, MPI_INT, 0, TERMINATE_TAG, MPI_COMM_WORLD, &S->terminal_request);
 
@@ -18,6 +28,8 @@ void worker_main(light* S, int num_procs, int rank) {
     
     int cnf_length;
 
+    MPI_Barrier(MPI_COMM_WORLD);
+
     MPI_Bcast(&cnf_length, 1, MPI_INT, 0, MPI_COMM_WORLD);
 
     MPI_Barrier(MPI_COMM_WORLD);
@@ -28,17 +40,6 @@ void worker_main(light* S, int num_procs, int rank) {
 
     MPI_Barrier(MPI_COMM_WORLD);
 
-    // std::this_thread::sleep_for(std::chrono::seconds(1));
-
-    // time_t now = time(NULL);
-    // MPI_Send(&now, 1, MPI_INT, 0, 0, MPI_COMM_WORLD);
-
-    // int buf[2];
-    // MPI_Recv(buf, 2, MPI_INT, 0, 0, MPI_COMM_WORLD, MPI_STATUS_IGNORE);
-    // int next = buf[0], last = buf[1];
-
-    // printf("my %d next: %d last: %d\n", rank, next, last);
-
     int res = S->run();
 
     MPI_Request solved_request, model_request;
@@ -53,6 +54,13 @@ void worker_main(light* S, int num_procs, int rank) {
 
             int flag;
 
+            auto clk_now = std::chrono::high_resolution_clock::now();
+            int solve_time = std::chrono::duration_cast<std::chrono::seconds>(clk_now - clk_st).count();
+            if (solve_time >= S->opt->times) {
+                printf("c [worker%d] solve time out\n", rank);
+                break;
+            }
+
             // when getting terminate signal
             if(MPI_Test(&S->terminal_request, &flag, MPI_STATUS_IGNORE) == MPI_SUCCESS && flag == 1) {