增加SAT模式，改进RS

kissat-inc/makefile

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

kissat-inc/src/bump.c

@@ -54,7 +54,12 @@ rescale_scores (kissat * solver, heap * scores)
 }
 
 void kissat_init_shuffle(kissat * solver, int maxvar) {
-  int seed = GET_OPTION(order_reset);
+  int seed = GET_OPTION(worker_seed);
+  int index = GET_OPTION(worker_index);
+  int number = GET_OPTION(worker_number);
+
+  printf("c index:%d number:%d seed:%d\n", index, number, seed);
+
   if (seed != -1)
   {
     // printf("c init shuffle %d\n", seed);
@@ -69,8 +74,17 @@ void kissat_init_shuffle(kissat * solver, int maxvar) {
       id[i] = id[j];
       id[j] = x;
     }
-    for (int i = 1; i <= maxvar; i++)
+
+    int block_size = maxvar / number;
+    int cursor = index * block_size;
+    for(int i=cursor; i<=maxvar; i++) {
       kissat_activate_literal(solver, kissat_import_literal(solver, id[i]));
+    }
+
+    for (int i = 1; i < cursor ; i++) {
+      kissat_activate_literal(solver, kissat_import_literal(solver, id[i]));
+    }
+      
     free(id);
   }
   else

kissat-inc/src/options.c

@@ -287,8 +287,10 @@ int
 kissat_options_set (options * options, const char *name, int value)
 {
   const opt *o = kissat_options_has (name);
+
   if (!o)
     return 0;
+
   return kissat_options_set_opt (options, o, value);
 }
 

kissat-inc/src/options.h

@@ -55,7 +55,6 @@ OPTION( mabcint, 4, 0, 10, "mab const floor") \
 OPTION( minimizedepth, 1e3, 1, 1e6, "minimization depth") \
 OPTION( modeinit, 1e3, 10, 1e8, "initial mode change interval") \
 OPTION( modeint, 1e3, 10, 1e8, "base mode change interval") \
-OPTION( order_reset, -1, -1, 1e5, "order seed") \
 OPTION( otfs, 1, 0, 1, "on-the-fly strengthening") \
 OPTION( phase, 1, 0, 1, "initial decision phase") \
 OPTION( phasesaving, 1, 0, 1, "enable phase saving") \
@@ -120,6 +119,9 @@ OPTION( walkmaxeff, 100, 1, INT_MAX, "maximum relative efficiency") \
 OPTION( walkmineff, 1e7, 0, INT_MAX, "minimum vivify efficiency") \
 OPTION( walkreleff, 10, 0, 1e3, "relative efficiency in per mille") \
 OPTION( walkrounds, 1, 1, 1e5, "rounds per walking phase") \
+OPTION( worker_index, -1, -1, 1e5, "worker index") \
+OPTION( worker_number, -1, -1, 1e5, "number of workers") \
+OPTION( worker_seed, -1, -1, 1e5, "worker random shuffle seed") \
 OPTION( xors, 1, 0, 1, "extract and eliminate XOR gates") \
 OPTION( xorsbound, 1 ,0 , 1<<13, "minimum elimination bound") \
 OPTION( xorsclslim, 5, 3, 31, "XOR extraction clause size limit") \

run.sh

@@ -27,6 +27,15 @@ INSTANCE=04157f716c1e9606c6a530657bf8f957-Kakuro-easy-125-ext.xml.hg_4.cnf
 
 # make -j 16 && mpirun --bind-to none -np 9 --allow-run-as-root ./light -i $DIR/$INSTANCE --share=1 --threads=16 --times=3600
 
+
+# cd kissat-inc
+# make clean
+# ./configure
+# make -j 64
+# cd ..
+
+# make clean
+
 make -j 16 && mpirun --bind-to none -np 9 --allow-run-as-root ./light -i ./data/WS_500_16_70_10.apx_0.cnf --share=1 --threads=16 --times=3600
 
 #./light -i $DIR/$INSTANCE --share=1 --threads=16 --times=3600

src/light.hpp

@@ -46,7 +46,7 @@ public:
 
     sharer* s;
     std::vector<std::vector<int>> sharing_groups;
-    enum { UNSAT, DEFAULT } worker_type;
+    enum { SAT, UNSAT, DEFAULT } worker_type;
 
     MPI_Request terminal_request;
 

src/sharer.cpp

@@ -235,11 +235,13 @@ void sharer::do_clause_sharing() {
         // 增加 lits 限制
         int percent = sort_clauses(i);
 
-        if (percent < 75) {
+        if(S->worker_type == light::UNSAT) {
-            producers[i]->broaden_export_limit();
+            if (percent < 75) {
-        }
+                producers[i]->broaden_export_limit();
-        else if (percent > 98) {
+            }
-            producers[i]->restrict_export_limit();
+            else if (percent > 98) {
+                producers[i]->restrict_export_limit();
+            }
         }
           
         for (int j = 0; j < consumers.size(); j++) {

src/solve.cpp

@@ -69,39 +69,39 @@ void light::init_workers() {
 
 void light::diversity_workers() {
     for (int i = 0; i < OPT(threads); i++) {
-        // if(worker_type == SAT) {
+        if(worker_type == SAT) {
 
-        //     if (OPT(shuffle)) {
+            if (OPT(shuffle)) {
-        //         if (i) workers[i]->configure("order_reset", (rank - 1) * OPT(threads) + i);
+                workers[i]->configure("worker_index", i);
-        //     }
+                workers[i]->configure("worker_number", OPT(threads));
+                workers[i]->configure("worker_seed", rank);
+            // printf("r1: %d, r2: %d, r3: %d\n", r1, r2, r3);
+            }
 
-        //     workers[i]->configure("stable", 1);
+            workers[i]->configure("stable", 1);
-        //     workers[i]->configure("target", 2);
+            workers[i]->configure("target", 2);
-        //     workers[i]->configure("phase", 1);
+            workers[i]->configure("phase", 1);
-        //     // workers[i]->configure("heuristic", 0);
+            // workers[i]->configure("heuristic", 0);
 
-        //     if (i == 2)
+            if (i == 2)
-        //         workers[i]->configure("stable", 0); 
+                workers[i]->configure("stable", 0); 
-        //     else if (i == 6)
+            else if (i == 6)
-        //         workers[i]->configure("stable", 2); 
+                workers[i]->configure("stable", 2); 
 
-        //     if (i == 7)
+            if (i == 7)
-        //         workers[i]->configure("target", 0);
+                workers[i]->configure("target", 0);
-        //     else if (i == 0 || i == 2 || i == 3 || i == 6)
+            else if (i == 0 || i == 2 || i == 3 || i == 6)
-        //         workers[i]->configure("target", 1);
+                workers[i]->configure("target", 1);
                         
-        //     if (i == 3 || i == 11 || i == 12 || i == 13 || i == 15)
+            if (i == 3 || i == 11 || i == 12 || i == 13 || i == 15)
-        //         workers[i]->configure("phase", 0);
+                workers[i]->configure("phase", 0);
-        // } else 
+        } else if(worker_type == UNSAT) {
-        
-        if(worker_type == UNSAT) {
-
             OPT(share_lits) = 3000;
-
             workers[i]->configure("chrono", 1);
             workers[i]->configure("stable", 0);
             // workers[i]->configure("walkinitially", 0);
             workers[i]->configure("target", 1);
+            
             // workers[i]->configure("phase", 1);
             // workers[i]->configure("heuristic", 0);
             // workers[i]->configure("margin", 1)0;
@@ -119,10 +119,16 @@ void light::diversity_workers() {
                 workers[i]->configure("target", 0);
             else if (i == 14)
                 workers[i]->configure("target", 2);
+                
         } else {
+
             if (OPT(shuffle)) {
-                if (i) workers[i]->configure("order_reset", (rank - 1) * OPT(threads) + i);
+                workers[i]->configure("worker_index", i);
+                workers[i]->configure("worker_number", OPT(threads));
+                workers[i]->configure("worker_seed", rank);
+            // printf("r1: %d, r2: %d, r3: %d\n", r1, r2, r3);
             }
+            
             if (i == 13 || i == 14 || i == 9)
                 workers[i]->configure("tier1", 3);
             else
@@ -273,26 +279,38 @@ void light::seperate_groups() {
     int worker_procs = num_procs - 1;
 
     if(worker_procs >= 8) {
-        int unsat_procs = worker_procs / 4;
+        int sat_procs = worker_procs / 8;
-        int default_procs = worker_procs - unsat_procs;
+        int unsat_procs = sat_procs;
-        // [1, unsat_procs] for unsat
+        int default_procs = worker_procs - sat_procs - unsat_procs;
-        if(rank >= 1 && rank <= unsat_procs) {
+        // [1, sat_procs] for sat
-            worker_type = light::UNSAT;
+        if(rank >= 1 && rank <= sat_procs) {
+            worker_type = light::SAT;
         }
 
         std::vector<int> tmp;
-        for(int i=1; i<=unsat_procs; i++) {
+        for(int i=1; i<=sat_procs; i++) {
             tmp.push_back(i);
         }
         sharing_groups.push_back(tmp);
         
-        // [unsat_procs+1, worker_procs]
+        // [sat_procs+1, sat_procs+unsat_procs] for unsat
-        if(rank >= unsat_procs+1 && rank <= worker_procs) {
+        if(rank >= sat_procs+1 && rank <= sat_procs+unsat_procs) {
+            worker_type = light::UNSAT;
+        }
+
+        tmp.clear();
+        for(int i=sat_procs+1; i<=sat_procs+unsat_procs; i++) {
+            tmp.push_back(i);
+        }
+        sharing_groups.push_back(tmp);
+
+        // [sat_procs+unsat_procs+1, worker_procs]
+        if(rank >= sat_procs+unsat_procs+1 && rank <= worker_procs) {
             worker_type = light::DEFAULT;
         }
 
         tmp.clear();
-        for(int i=unsat_procs+1; i<=worker_procs; i++) {
+        for(int i=sat_procs+unsat_procs+1; i<=worker_procs; i++) {
             tmp.push_back(i);
         }
         sharing_groups.push_back(tmp);
@@ -308,6 +326,7 @@ void light::seperate_groups() {
     }
 }
 
+
 void print_model(vec<int> &model) {
     printf("v");
     for (int i = 0; i < model.size(); i++) {

src/solver_api/basekissat.cpp

@@ -15,9 +15,9 @@ void basekissat::add(int l) {
     kissat_add(solver, l);
 }
 
-void basekissat::configure(const char* name, int val) {
+int basekissat::configure(const char* name, int val) {
     // printf("c %d set %s to %d\n", id, name, val);
-    kissat_set_option(solver, name, val);
+    return kissat_set_option(solver, name, val);
 }
 
 int  basekissat::solve() {

src/solver_api/basekissat.hpp

@@ -10,7 +10,7 @@ public:
     void add(int l);
     int  solve();
     int  val(int l);
-    void configure(const char* name, int id);
+    int configure(const char* name, int id);
 
     int  get_conflicts();
     void parse_from_CNF(char* filename);

src/solver_api/basesolver.hpp

@@ -17,7 +17,7 @@ public:
     virtual int  solve() = 0;
     virtual int  val(int l) = 0;
     virtual void terminate() = 0;
-    virtual void configure(const char* name, int id) = 0;
+    virtual int configure(const char* name, int id) = 0;
     virtual int  get_conflicts() = 0;
 
     virtual void parse_from_CNF(char* filename) = 0;