version 1.1 (add dynamically reseting)

build.sh

@@ -0,0 +1,5 @@
+cd /home/chenzh/solvers/Light/solvers/kissat-inc;
+./configure && make;
+cd ..;
+cd ..;
+make clean; make;

light.cpp

@@ -16,8 +16,8 @@ light::light():
 }
 
 light::~light() {
-    for (int i = 0; i < solvers.size(); i++) delete(solvers[i]);
+    for (int i = 0; i < workers.size(); i++) delete(workers[i]);
-    solvers.clear(true);
+    workers.clear(true);
 }
 
 void light::arg_parse(int argc, char **argv) {

light.hpp

@@ -10,6 +10,14 @@ typedef long long ll;
 
 class basesolver;
 
+struct thread_inf{
+    int id, inf;
+    bool operator < ( const thread_inf &other ) const
+	{
+		return inf > other.inf;
+	}
+};
+
 struct light
 {
 public:
@@ -19,7 +27,7 @@ public:
     char *filename;
     paras *opt;
     preprocess *pre;
-    vec<basesolver *> solvers;
+    vec<basesolver *> workers;
 
     int finalResult;
     int winner;
@@ -27,12 +35,12 @@ public:
     atomic<bool> globalEnding;
 
     void arg_parse(int argc, char **argv);
-    void init_solvers();
+    void init_workers();
-    void diversity_solvers();
+    void diversity_workers();
     void parse_input();
     int  run();
     int  solve();
-    void terminate_solvers();
+    void terminate_workers();
     void print_model();
 };
 

preprocess.cpp

@@ -246,7 +246,7 @@ bool preprocess::preprocess_binary() {
         for (int j = 0; j < l; j++)
             clause[i][j] = tolit(clause[i][j]);
     }
-    nlit = vars << 1;
+    nlit = (vars << 1) + 2;
     for (int i = 1; i <= vars; i++) f[i] = i, val[i] = 1, color[i] = 0;
     for (int i = 1; i <= clauses; i++) clause_delete[i] = 0;
     int len = 0;
@@ -284,6 +284,8 @@ bool preprocess::preprocess_binary() {
         }
     }
     
+    for (int i = 1; i <= vars; i++) find(i);
+
     for (int i = 1; i <= clauses; i++) {
         if (clause_delete[i]) continue;
         int l = clause[i].size(), oril = l;
@@ -296,15 +298,17 @@ bool preprocess::preprocess_binary() {
             if (resseen[a[j]] == i) continue;
             resseen[a[j]] = i, a[t++] = a[j];
         }
-        if (t != l) l = t;
+        if (t != l) {l = t;}
         for (int j = 0; j < l; j++)
-            if (resseen[negative(a[j])] == i)
+            if (resseen[negative(a[j])] == i) {
                 clause_delete[i] = 1;
+            }
         for (int j = 0; j < l; j++) resseen[a[j]] = 0;
         clause[i].clear();
         for (int j = 0; j < l; j++)
             clause[i].push(a[j]);
     }
+    
 
     for (int i = 1; i <= clauses; i++) {
         if (clause_delete[i]) continue;
@@ -313,6 +317,7 @@ bool preprocess::preprocess_binary() {
             clause[i][j] = toeidx(clause[i][j]);
         }
     }
+
     update_var_clause_label();
     for (int i = 1; i <= orivars; i++) {
         if (mapval[i]) continue;
@@ -420,7 +425,6 @@ bool preprocess::preprocess_easy_clause() {
         }
     }
     update_var_clause_label();
-
     for (int i = 1; i <= tail; i++) {
         int v = q[i];
         mapval[v] = varval[v];

solve.cpp

@@ -2,6 +2,7 @@
 #include "workers/basekissat.hpp"
 #include <unistd.h>
 #include <chrono>
+#include <algorithm>
 char* worker_sign = "";
 atomic<int> terminated;
 auto clk_st = std::chrono::high_resolution_clock::now();
@@ -27,7 +28,7 @@ void * solve_worker(void *arg) {
             sq->get_model(seq_model);
         }
         if (res && !terminated) {
-            sq->controller->terminate_solvers();
+            sq->controller->terminate_workers();
             terminated = 1;
             result = res;
             winner = sq->id;
@@ -38,29 +39,29 @@ void * solve_worker(void *arg) {
    return NULL;
 }
 
-void light::init_solvers() {
+void light::init_workers() {
     for (int i = 0; i < OPT(threads); i++) {
         basekissat* kissat = new basekissat(i, this);
-        solvers.push(kissat);
+        workers.push(kissat);
     }
 }
 
-void light::diversity_solvers() {
+void light::diversity_workers() {
     for (int i = 0; i < OPT(threads); i++) {
-        solvers[i]->diversity(i);
+        workers[i]->diversity(i);
     }
 }
 
-void light::terminate_solvers() {
+void light::terminate_workers() {
     for (int i = 0; i < OPT(threads); i++) {
-        solvers[i]->terminate();
+        workers[i]->terminate();
     }
 }
 
 void light::parse_input() {
     pthread_t *ptr = new pthread_t[OPT(threads)];
     for (int i = 0; i < OPT(threads); i++) {
-      pthread_create(&ptr[i], NULL, read_worker, solvers[i]);
+      pthread_create(&ptr[i], NULL, read_worker, workers[i]);
    }   
    for (int i = 0; i < OPT(threads); i++) {
       pthread_join(ptr[i], NULL);
@@ -73,27 +74,48 @@ int light::solve() {
     terminated = 0;
     pthread_t *ptr = new pthread_t[OPT(threads)];
     for (int i = 0; i < OPT(threads); i++) {
-      pthread_create(&ptr[i], NULL, solve_worker, solvers[i]);
+      pthread_create(&ptr[i], NULL, solve_worker, workers[i]);
-   }
+    }
+
+    thread_inf unimprove[OPT(threads)];
+    auto clk_sol_st = std::chrono::high_resolution_clock::now();
+    int pre_time = std::chrono::duration_cast<std::chrono::seconds>(clk_sol_st - clk_st).count();
+    int sol_thd = 0, intv_time = OPT(reset_time);
     while (!terminated) {
         usleep(100000);        
         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 >= OPT(times)) {
             terminated = 1;
-            terminate_solvers();
+            terminate_workers();
+        }
+        if (OPT(reset) && solve_time >= pre_time + intv_time) {
+            pre_time = solve_time;
+            intv_time += OPT(reset_time);
+            sol_thd = 0;
+            for (int i = 0; i < OPT(threads); i++) {
+                unimprove[sol_thd++] = (thread_inf) {i, workers[i]->get_reset_data()};
+            }
+            std::sort(unimprove, unimprove + sol_thd);
+            printf("Reset thread (%d): ", solve_time);
+            for (int i = 0; i < sol_thd / 2; i++) {
+                workers[i]->reset();
+                printf("%d(%d) ", unimprove[i].id, unimprove[i].inf);
+            }
+            puts("\n");
         }
     }
+
     for (int i = 0; i < OPT(threads); i++) {
         pthread_join(ptr[i], NULL);
     }    
-   delete []ptr;
+    delete []ptr;
-   return result;
+    return result;
 }
 
 int light::run() {
-    init_solvers();
+    init_workers();
-    diversity_solvers();
+    diversity_workers();
     if (OPT(simplify)) {
         pre = new preprocess();
         int res = pre->do_preprocess(filename);

solvers/kissat-inc/build/build.h

@@ -1,5 +1,5 @@
 #define VERSION "1.0.3"
 #define COMPILER "gcc (Ubuntu 9.4.0-1ubuntu1~20.04.1) 9.4.0 -W -Wall -O3 -DNEMBEDDED -DNDEBUG -DNMETRICS -DNSTATISTICS"
 #define ID "79d8d8f20465e71fd2b0f193b468898cd803a59a"
-#define BUILD "Thu Aug 25 15:41:16 CST 2022 Linux seed1 5.4.0-120-generic x86_64"
+#define BUILD "Wed Aug 31 12:28:43 CST 2022 Linux seed1 5.4.0-120-generic x86_64"
-#define DIR "/home/chenzh/solvers/Light/kissat-inc/build"
+#define DIR "/home/chenzh/solvers/Light/solvers/kissat-inc/build"

solvers/kissat-inc/makefile

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

solvers/kissat-inc/src/bump.c

@@ -53,6 +53,36 @@ rescale_scores (kissat * solver, heap * scores)
 		GET (rescaled), "rescaled by factor %g", factor);
 }
 
+void kissat_shuffle_score(kissat * solver) {
+  heap *scores = &solver->scores;
+  heap *scores_chb = &solver->scores_chb;
+  flags *flags = solver->flags;
+  int *id = (int *)malloc(sizeof(int) * (VARS));
+  for (int i = 0; i < VARS; i++) id[i] = i;
+  for (int i = 0; i < VARS; i++)
+  {
+    int j = (rand() % VARS);
+    int x = id[i];
+    id[i] = id[j];
+    id[j] = x;
+  }
+  for (int i = 0; i < VARS; i++) {
+    int idx = id[i];
+    if (flags[idx].active) {
+      double new_score = 1.0 * i / VARS;
+      kissat_update_heap (solver, scores, idx, new_score);
+      kissat_update_heap (solver, scores_chb, idx, new_score);
+    }
+  }
+  for (int i = 0; i < VARS; i++) {
+    int idx = id[i];
+    if (flags[idx].active)
+      kissat_move_to_front(solver, idx);
+  }
+  solver->scinc = 1.0;
+  free(id);
+}
+
 static void
 bump_score_increment (kissat * solver, heap * scores)
 {

solvers/kissat-inc/src/bump.h

@@ -6,6 +6,7 @@ struct kissat;
 void kissat_bump_variables (struct kissat *);
 void kissat_bump_chb (struct kissat *, unsigned idx, double multiplier);
 void kissat_decay_chb (struct kissat *);
+void kissat_shuffle_score(struct kissat *);
 void kissat_update_conflicted_chb (struct kissat *);
 
 #define MAX_SCORE 1e150

solvers/kissat-inc/src/internal.c

@@ -45,6 +45,7 @@ kissat_init (void)
   solver-> mab_decisions = 0;
   solver-> mab_chosen_tot = 0;
   solver-> order_reset = -1;
+  solver-> reseting = 0;
 #ifndef NDEBUG
   kissat_init_checker (solver);
 #endif

solvers/kissat-inc/src/internal.h

@@ -72,6 +72,7 @@ typedef STACK (watch *) patches;
 
 struct kissat
 {
+  int reseting;
   int order_reset;
   int max_var;
 #ifdef LOGGING

solvers/kissat-inc/src/search.c

@@ -18,185 +18,188 @@
 #include <inttypes.h>
 
 static void
-start_search (kissat * solver)
+start_search(kissat *solver)
 {
-  START (search);
+  START(search);
-  INC (searches);
+  INC(searches);
 
-  REPORT (0, '*');
+  REPORT(0, '*');
 
-  bool stable = (GET_OPTION (stable) == 2);
+  bool stable = (GET_OPTION(stable) == 2);
 
   solver->stable = stable;
-  kissat_phase (solver, "search", GET (searches),
+  kissat_phase(solver, "search", GET(searches),
-		"initializing %s search after %" PRIu64 " conflicts",
+               "initializing %s search after %" PRIu64 " conflicts",
-		(stable ? "stable" : "focus"), CONFLICTS);
+               (stable ? "stable" : "focus"), CONFLICTS);
 
-  kissat_init_averages (solver, &AVERAGES);
+  kissat_init_averages(solver, &AVERAGES);
 
   if (solver->stable)
-    kissat_init_reluctant (solver);
+    kissat_init_reluctant(solver);
 
-  kissat_init_limits (solver);
+  kissat_init_limits(solver);
 
-  unsigned seed = GET_OPTION (seed);
+  unsigned seed = GET_OPTION(seed);
   solver->random = seed;
-  LOG ("initialized random number generator with seed %u", seed);
+  LOG("initialized random number generator with seed %u", seed);
 
-  kissat_reset_rephased (solver);
+  kissat_reset_rephased(solver);
 
-  const unsigned eagersubsume = GET_OPTION (eagersubsume);
+  const unsigned eagersubsume = GET_OPTION(eagersubsume);
   if (eagersubsume && !solver->clueue.elements)
-    kissat_init_clueue (solver, &solver->clueue, eagersubsume);
+    kissat_init_clueue(solver, &solver->clueue, eagersubsume);
 #ifndef QUIET
   limits *limits = &solver->limits;
   limited *limited = &solver->limited;
   if (!limited->conflicts && !limited->decisions)
-    kissat_very_verbose (solver, "starting unlimited search");
+    kissat_very_verbose(solver, "starting unlimited search");
   else if (limited->conflicts && !limited->decisions)
-    kissat_very_verbose (solver,
+    kissat_very_verbose(solver,
-			 "starting search with conflicts limited to %" PRIu64,
+                        "starting search with conflicts limited to %" PRIu64,
-			 limits->conflicts);
+                        limits->conflicts);
   else if (!limited->conflicts && limited->decisions)
-    kissat_very_verbose (solver,
+    kissat_very_verbose(solver,
-			 "starting search with decisions limited to %" PRIu64,
+                        "starting search with decisions limited to %" PRIu64,
-			 limits->decisions);
+                        limits->decisions);
   else
-    kissat_very_verbose (solver,
+    kissat_very_verbose(solver,
-			 "starting search with decisions limited to %" PRIu64
+                        "starting search with decisions limited to %" PRIu64
-			 " and conflicts limited to %" PRIu64,
+                        " and conflicts limited to %" PRIu64,
-			 limits->decisions, limits->conflicts);
+                        limits->decisions, limits->conflicts);
   if (stable)
-    {
+  {
-      START (stable);
+    START(stable);
-      REPORT (0, '[');
+    REPORT(0, '[');
-    }
+  }
   else
-    {
+  {
-      START (focused);
+    START(focused);
-      REPORT (0, '{');
+    REPORT(0, '{');
-    }
+  }
 #endif
 }
 
 static void
-stop_search (kissat * solver, int res)
+stop_search(kissat *solver, int res)
 {
   if (solver->limited.conflicts)
-    {
+  {
-      LOG ("reset conflict limit");
+    LOG("reset conflict limit");
-      solver->limited.conflicts = false;
+    solver->limited.conflicts = false;
-    }
+  }
 
   if (solver->limited.decisions)
-    {
+  {
-      LOG ("reset decision limit");
+    LOG("reset decision limit");
-      solver->limited.decisions = false;
+    solver->limited.decisions = false;
-    }
+  }
 
   if (solver->terminate)
-    {
+  {
-      kissat_very_verbose (solver, "termination forced externally");
+    kissat_very_verbose(solver, "termination forced externally");
-      solver->terminate = 0;
+    solver->terminate = 0;
-    }
+  }
 
 #ifndef QUIET
-  LOG ("search result %d", res);
+  LOG("search result %d", res);
   if (solver->stable)
-    {
+  {
-      REPORT (0, ']');
+    REPORT(0, ']');
-      STOP (stable);
+    STOP(stable);
-      solver->stable = false;
+    solver->stable = false;
-    }
+  }
   else
-    {
+  {
-      REPORT (0, '}');
+    REPORT(0, '}');
-      STOP (focused);
+    STOP(focused);
-    }
+  }
-  char type = (res == 10 ? '1' : res == 20 ? '0' : '?');
+  char type = (res == 10 ? '1' : res == 20 ? '0'
-  REPORT (0, type);
+                                           : '?');
+  REPORT(0, type);
 #else
-  (void) res;
+  (void)res;
 #endif
 
-  STOP (search);
+  STOP(search);
 }
 
 static void
-iterate (kissat * solver)
+iterate(kissat *solver)
 {
-  assert (solver->iterating);
+  assert(solver->iterating);
   solver->iterating = false;
-  REPORT (0, 'i');
+  REPORT(0, 'i');
 }
 
 static bool
-conflict_limit_hit (kissat * solver)
+conflict_limit_hit(kissat *solver)
 {
   if (!solver->limited.conflicts)
     return false;
   if (solver->limits.conflicts > solver->statistics.conflicts)
     return false;
-  kissat_very_verbose (solver, "conflict limit %" PRIu64
+  kissat_very_verbose(solver, "conflict limit %" PRIu64 " hit after %" PRIu64 " conflicts",
-		       " hit after %" PRIu64 " conflicts",
+                      solver->limits.conflicts,
-		       solver->limits.conflicts,
+                      solver->statistics.conflicts);
-		       solver->statistics.conflicts);
   return true;
 }
 
 static bool
-decision_limit_hit (kissat * solver)
+decision_limit_hit(kissat *solver)
 {
   if (!solver->limited.decisions)
     return false;
   if (solver->limits.decisions > solver->statistics.decisions)
     return false;
-  kissat_very_verbose (solver, "decision limit %" PRIu64
+  kissat_very_verbose(solver, "decision limit %" PRIu64 " hit after %" PRIu64 " decisions",
-		       " hit after %" PRIu64 " decisions",
+                      solver->limits.decisions,
-		       solver->limits.decisions,
+                      solver->statistics.decisions);
-		       solver->statistics.decisions);
   return true;
 }
 
-int
+int kissat_search(kissat *solver)
-kissat_search (kissat * solver)
 {
-  start_search (solver);
+  start_search(solver);
 
-  int res = kissat_walk_initially (solver);
+  int res = kissat_walk_initially(solver);
 
   while (!res)
+  {
+    if (!solver->level && solver->reseting)
     {
-      clause *conflict = kissat_search_propagate (solver);
+      kissat_shuffle_score(solver);
-      if (conflict)
+      solver->reseting = 0;
-	res = kissat_analyze (solver, conflict);
-      else if (solver->iterating)
-	iterate (solver);
-      else if (!solver->unassigned)
-	res = 10;
-      else if (TERMINATED (11))
-	break;
-      else if (conflict_limit_hit (solver))
-	break;
-      else if (kissat_reducing (solver))
-	res = kissat_reduce (solver);
-      else if (kissat_restarting (solver))
-	kissat_restart (solver);
-      else if (kissat_rephasing (solver))
-	kissat_rephase (solver);
-      else if (kissat_eliminating (solver))
-	res = kissat_eliminate (solver);
-      else if (kissat_probing (solver))
-	res = kissat_probe (solver);
-      else if (!solver->level && solver->unflushed)
-	kissat_flush_trail (solver);
-      else if (decision_limit_hit (solver))
-	break;
-      else
-	kissat_decide (solver);
     }
+    clause *conflict = kissat_search_propagate(solver);
+    if (conflict)
+      res = kissat_analyze(solver, conflict);
+    else if (solver->iterating)
+      iterate(solver);
+    else if (!solver->unassigned)
+      res = 10;
+    else if (TERMINATED(11))
+      break;
+    else if (conflict_limit_hit(solver))
+      break;
+    else if (kissat_reducing(solver))
+      res = kissat_reduce(solver);
+    else if (kissat_restarting(solver))
+      kissat_restart(solver);
+    else if (kissat_rephasing(solver))
+      kissat_rephase(solver);
+    else if (kissat_eliminating(solver))
+      res = kissat_eliminate(solver);
+    else if (kissat_probing(solver))
+      res = kissat_probe(solver);
+    else if (!solver->level && solver->unflushed)
+      kissat_flush_trail(solver);
+    else if (decision_limit_hit(solver))
+      break;
+    else
+      kissat_decide(solver);
+  }
 
-  stop_search (solver, res);
+  stop_search(solver, res);
 
   return res;
 }

utils/paras.hpp

@@ -6,10 +6,12 @@
 
 //        name,      type,   default, low, high, comments
 #define PARAS \
-    PARA( mode     , int    , 0     , 0  , 2   , "SAT=1, UNSAT=2") \
+    PARA( mode       , int    , 0     , 0  , 2   , "SAT=1, UNSAT=2") \
-    PARA( simplify , int    , 1     , 0  , 1   , "Use Simplify(only preprocess)") \
+    PARA( reset      , int    , 0     , 0  , 1   , "Dynamically reseting") \
-    PARA( times    , double , 5000  , 0  , 1e8 , "Cutoff time") \
+    PARA( reset_time , int    , 10    , 1  , 1e5 , "Reseting base interval (seconds)") \
-    PARA( threads  , int    , 32    , 1  , 128 , "Thread number") \
+    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") \
     
 
 struct paras 

version.md

@@ -0,0 +1,5 @@
+### 1.0
+base Framework
+RS
+#### 1.1
+Dynamically reseting

workers/basekissat.cpp

@@ -57,4 +57,13 @@ void basekissat::get_model(vec<int> &model) {
       if (!tmp) tmp = i;
       model.push(tmp);
    }
+}
+
+int basekissat::get_reset_data() {
+    return solver->best_assigned;
+}
+
+
+void basekissat::reset() {
+    solver->reseting = 1;
 }

workers/basekissat.hpp

@@ -10,6 +10,8 @@ public:
     void terminate();
     int  solve();
     void get_model(vec<int> &model);
+    int  get_reset_data();
+    void reset();
 
     basekissat(int id, light *light);
     ~basekissat();

workers/basesolver.hpp

@@ -11,6 +11,8 @@ public:
     virtual int  solve() = 0;
     virtual void terminate() = 0;
     virtual void get_model(vec<int> &model) = 0;
+    virtual int  get_reset_data() = 0;
+    virtual void reset() = 0;
     light * controller;
     int id;