version 5.7 DPS

light.cpp

@@ -5,9 +5,9 @@
 
 light::light():
   finalResult           (0),
-  winner                (0),
-  maxtime               (5000),
-  globalEnding          (false)
+  winner_period         (1e9),
+  winner_id             (-1),
+  maxtime               (5000)
 {
     opt = new paras();
     opt->init_paras();

light.hpp

@@ -5,7 +5,9 @@
 #include "preprocess/preprocess.hpp"
 #include <atomic>
 #include <iostream>
-#include <mutex>
+#include <boost/thread.hpp>
+#include <boost/thread/thread.hpp>
+#include <boost/lockfree/spsc_queue.hpp>
 typedef long long ll;
 
 class basesolver;
@@ -35,10 +37,20 @@ public:
     vec<sharer *> sharers;
 
     int finalResult;
-    int winner;
+    int winner_period, winner_id;
+    mutable boost::mutex winner_mtx;
     int maxtime;
-    std::atomic<bool> globalEnding;
-
+    void update_winner(int id, int period) {
+        boost::mutex::scoped_lock lock(winner_mtx);
+        if (period < winner_period || (period == winner_period && id < winner_id)) {
+            winner_period = period;
+            winner_id = id;
+        }
+    }
+    int  get_winner_period() {
+        boost::mutex::scoped_lock lock(winner_mtx);
+        return winner_period;
+    }
     void arg_parse(int argc, char **argv);
     void init_workers();
     void diversity_workers();

solve.cpp

@@ -7,7 +7,7 @@
 #include <mutex>
 auto clk_st = std::chrono::high_resolution_clock::now();
 char* worker_sign = "";
-std::mutex mtx;
+
 std::atomic<int> terminated;
 int result = 0;
 int winner, winner_conf;
@@ -26,21 +26,37 @@ void * solve_worker(void *arg) {
    basesolver * sq = (basesolver *)arg;
    while (!terminated) {
         int res = sq->solve();
-        vec<int> seq_model;
-        if (res == 10) {
-            sq->get_model(seq_model);
+        if (sq->controller->opt->DPS == 2) {
+            printf("c %d solved, res is %d\n", sq->id, res);
+            if (res) {
+                terminated = 1;
+                result = res; 
+                printf("c %d solved 1\n", sq->id);
+                sq->set_winner_period();
+                printf("c %d solved 2\n", sq->id);
+                sq->controller->update_winner(sq->id, sq->period);
+                printf("c %d solved 3\n", sq->id);
+                if (res == 10) sq->get_model(sq->model);
+            }
+            printf("c %d really solved, period is %d\n", sq->id, sq->period);
         }
-        if (res && !terminated) {
-            printf("c result: %d, winner is %d, winner run %d confs\n", res, sq->id, sq->get_conflicts());
-            terminated = 1;
-            sq->controller->terminate_workers();
-            result = res;
-            winner = sq->id;
-            winner_conf = sq->get_conflicts();
-            if (res == 10) seq_model.copyTo(model);
+        else {
+            vec<int> seq_model;
+            if (res == 10) {
+                sq->get_model(seq_model);
+            }
+            if (res && !terminated) {
+                printf("c result: %d, winner is %d, winner run %d confs\n", res, sq->id, sq->get_conflicts());
+                terminated = 1;
+                sq->controller->terminate_workers();
+                result = res;
+                winner = sq->id;
+                winner_conf = sq->get_conflicts();
+                if (res == 10) seq_model.copyTo(model);
+            }
+            seq_model.clear();
+            printf("get result %d with res %d\n", sq->id, res);
         }
-        seq_model.clear();
-        // printf("get result %d with res %d\n", sq->id, res);
    }
    return NULL;
 }
@@ -97,8 +113,12 @@ void light::diversity_workers() {
 }
 
 void light::terminate_workers() {
+    printf("c controller reach limit\n");
     for (int i = 0; i < OPT(threads); i++) {
-        workers[i]->terminate();
+        if (OPT(share) == 1 && OPT(DPS) == 2) 
+            workers[i]->dps_terminate();
+        else 
+            workers[i]->terminate();
     }
     for (int i = 0; i < sharers.size(); i++) {
         sharers[i]->set_terminated();
@@ -152,15 +172,19 @@ int light::solve() {
         // }
     }
     // printf("ending solve\n");
-    terminate_workers();
+    // terminate_workers(); //important, need combine nps/dps !!!!!!!!!!!!!!!!
 
     for (int i = 0; i < OPT(threads); i++) {
         pthread_join(ptr[i], NULL);
     }
+    
+    printf("ending join\n");
+    if (result == 10)
+        workers[winner_id]->model.copyTo(model);
     auto clk_now = std::chrono::high_resolution_clock::now();
     double solve_time = std::chrono::duration_cast<std::chrono::milliseconds>(clk_now - clk_sol_st).count();
     solve_time = 0.001 * solve_time;
-    printf("c solve time: %.2lf\n", solve_time);
+    printf("c solve time: %.2lf\nwinner is %d, period is %d\n", solve_time, winner_id, winner_period);
     for (int i = 0; i < OPT(threads); i++) {
         printf("c thread %d waiting time: %.2lf\n", i, workers[i]->get_waiting_time());
     }   
@@ -206,7 +230,7 @@ void solve(int argc, char **argv) {
     int res = S->run();
     if (res == 10) {
         printf("s SATISFIABLE\n");
-        print_model(model);
+        // print_model(model);
     }
     else if (res == 20) {
         printf("s UNSATISFIABLE\n");

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 "Mon Feb 27 07:44:55 UTC 2023 Linux seed4 5.4.0-125-generic x86_64"
+#define BUILD "Mon Mar 13 18:39:10 CST 2023 Linux seed1 5.4.0-139-generic x86_64"
 #define DIR "/home/chenzh/solvers/Light/solvers/kissat-inc/build"

solvers/kissat-inc/src/analyze.c

@@ -168,6 +168,7 @@ analyze_reason_side_literals(kissat *solver)
     {
       assert(a->reason < SIZE_STACK(solver->arena));
       clause *c = (clause *)(arena + a->reason);
+      solver->dps_ticks++;
       for (all_literals_in_clause(lit, c))
         if (IDX(lit) != idx)
           mark_literal_as_analyzed(solver, all_assigned, lit,

solvers/kissat-inc/src/eliminate.c

@@ -315,6 +315,7 @@ weaken_clauses (kissat * solver, unsigned lit)
 	    kissat_weaken_clause (solver, lit, c);
 	  LOGCLS (c, "removing %s", LOGLIT (lit));
 	  kissat_eliminate_clause (solver, c, lit);
+    solver->dps_ticks++;
 	}
     }
   RELEASE_WATCHES (*pos_watches);
@@ -351,7 +352,8 @@ weaken_clauses (kissat * solver, unsigned lit)
 	  if (!optimize && !satisfied)
 	    kissat_weaken_clause (solver, not_lit, d);
 	  LOGCLS (d, "removing %s", LOGLIT (not_lit));
-	  kissat_eliminate_clause (solver, d, not_lit);
+	  kissat_eliminate_clause (solver, d, not_lit);   
+    solver->dps_ticks++;
 	}
     }
   if (optimize && neg_watches->size)

solvers/kissat-inc/src/forward.c

@@ -151,6 +151,7 @@ find_forward_subsumption_candidates (kissat * solver, references * candidates)
 	continue;
       assert (c->size > 2);
       unsigned subsume = 0;
+	  solver->dps_ticks++;
       for (all_literals_in_clause (lit, c))
 	{
 	  const unsigned idx = IDX (lit);
@@ -270,7 +271,11 @@ forward_literal (kissat * solver, unsigned lit, bool binaries,
 
 	  INC (subsumption_checks);
 
-	  subsume = true;
+	  subsume = true;	
+
+
+	  solver->dps_ticks++;
+
 
 	  unsigned candidate = INVALID_LIT;
 
@@ -605,6 +610,7 @@ forward_subsume_all_clauses (kissat * solver)
 #ifndef QUIET
 	checked++;
 #endif
+	solver->dps_ticks++;
 	bool removed = false;
 	if (forward_subsumed_clause (solver, c, &removed))
 	  subsumed++;
@@ -656,6 +662,7 @@ forward_subsume_all_clauses (kissat * solver)
 	if (c->subsume)
 	  remain++;
 #endif
+	solver->dps_ticks++;
 	for (all_literals_in_clause (lit, c))
 	  {
 	    const unsigned idx = IDX (lit);

solvers/kissat-inc/src/internal.c

@@ -39,6 +39,7 @@ kissat_init (void)
   solver->watching = true;
   solver->conflict.size = 2;
   solver->conflict.keep = true;
+  solver->dps_ticks=0;
   solver->scinc = 1.0;
   solver->first_reducible = INVALID_REF;
   solver->last_irredundant = INVALID_REF;

solvers/kissat-inc/src/internal.h

@@ -73,10 +73,12 @@ typedef STACK (watch *) patches;
 
 struct kissat
 {
+  int dps_ticks;
   int  (* cbkImportUnit)  (void *);
   int  (* cbkImportClause)(void *, int *, cvec *);
   void (* cbkExportClause)(void *, int, cvec *);	        
-  void (* cbkWaitSharing) (void *);           // callback for clause learning
+  int (* cbkWaitSharing) (void *);          
+  void (* cbkFreeClause)  (void *);           // callback for clause learning
   int share_dps;
   int share_dps_period;
   cvec *importedClause;

solvers/kissat-inc/src/minimize.c

@@ -9,6 +9,7 @@ minimize_reference (kissat * solver, assigned * assigned,
 {
   const unsigned not_lit = NOT (lit);
   clause *c = kissat_dereference_clause (solver, ref);
+  solver->dps_ticks++;
   for (all_literals_in_clause (other, c))
     if (other != not_lit &&
 	!minimize_literal (solver, assigned, other, depth))

solvers/kissat-inc/src/propdense.c

@@ -107,6 +107,7 @@ non_watching_propagate_literal (kissat * solver,
 
   ADD (ticks, ticks);
   ADD (dense_ticks, ticks);
+  solver->dps_ticks += ticks;
 
   return true;
 }

solvers/kissat-inc/src/prophyper.c

@@ -77,6 +77,8 @@ binary_propagate_literal (kissat * solver, unsigned lit)
   const watch *begin = BEGIN_WATCHES (*watches);
   const watch *end = END_WATCHES (*watches);
   const watch *p = begin;
+  int ticks =  kissat_cache_lines (watches->size, sizeof (watch));
+  solver->dps_ticks +=ticks;
 
   clause *res = 0;
 

solvers/kissat-inc/src/proplit.h

@@ -243,6 +243,7 @@ PROPAGATE_LITERAL (kissat * solver,
 	}
     }
   solver->ticks += ticks;
+  solver->dps_ticks += ticks;
 
   while (p != end_watches)
     *q++ = *p++;

solvers/kissat-inc/src/resolve.c

@@ -213,6 +213,7 @@ generate_resolvents (kissat * solver, unsigned lit,
 	    }
 
 	  PUSH_STACK (solver->resolvents, INVALID_LIT);
+	  solver->dps_ticks++;
 	}
 
       for (all_literals_in_clause (other, c))

solvers/kissat-inc/src/search.c

@@ -171,12 +171,16 @@ int kissat_search(kissat *solver)
       solver->reseting = 0;
     }
     if (!solver->level) {
-      if (solver->share_dps == 1 && solver->nconflict >= solver->share_dps_period) {
-        solver->nconflict = 0;
-        solver->cbkWaitSharing(solver->issuer);
+      int should_free = 0;
+      if (solver->share_dps > 0 && solver->dps_ticks >= solver->share_dps_period) {
+        solver->dps_ticks -= solver->share_dps_period;
+        should_free = solver->cbkWaitSharing(solver->issuer);
+        if (should_free == -1) return 0;
       }
       if (!kissat_importUnitClauses(solver)) return 20;
       if (!kissat_importClauses(solver)) return 20;
+      if (should_free == 1 && solver->share_dps == 2)
+        solver->cbkFreeClause(solver->issuer);
     }
     clause *conflict = kissat_search_propagate(solver);
     if (conflict)

solvers/kissat-inc/src/substitute.c

@@ -100,6 +100,10 @@ determine_representatives (kissat * solver, unsigned *repr)
 	      assert (reach_lit == mark_lit);
 	      assert (repr[lit] == INVALID_LIT);
 	      watches *watches = all_watches + not_lit;
+
+  		unsigned ticks = kissat_cache_lines (watches->size, sizeof (watch));
+		solver->dps_ticks += 1 + ticks;
+
 	      for (all_binary_blocking_watches (watch, *watches))
 		{
 		  if (!watch.type.binary)
@@ -199,6 +203,10 @@ determine_representatives (kissat * solver, unsigned *repr)
 	      LOG ("substitute mark[%s] = %u", LOGLIT (lit), reached);
 	      const unsigned not_lit = NOT (lit);
 	      watches *watches = all_watches + not_lit;
+		  
+			unsigned ticks = kissat_cache_lines (watches->size, sizeof (watch));
+			solver->dps_ticks += 1 + ticks;
+
 	      for (all_binary_blocking_watches (watch, *watches))
 		{
 		  if (!watch.type.binary)

solvers/kissat-inc/src/transitive.c

@@ -89,6 +89,7 @@ transitive_reduce (kissat * solver,
   watch *begin_src = BEGIN_WATCHES (*src_watches);
   unsigned ticks = kissat_cache_lines (src_watches->size, sizeof (watch));
   ADD (transitive_ticks, ticks + 1);
+  solver->dps_ticks += 1 + ticks;
   const unsigned not_src = NOT (src);
   unsigned reduced = 0;
   bool failed = false;
@@ -158,7 +159,7 @@ transitive_reduce (kissat * solver,
       ADD (propagations, propagated);
       ADD (probing_propagations, propagated);
       ADD (transitive_propagations, propagated);
-
+      solver->dps_ticks += ticks + 1;
       transitive_backtrack (solver, saved);
 
       if (transitive)

testLight/cal_solver.py

@@ -228,10 +228,10 @@ class calculater(object):
                     have_diff_res = True
 
                 # if(True):
-                # if(False):
+                if(False):
                 # if(no_answer):
                 # if(all_can_solve):
-                if(have_diff_res):
+                # if(have_diff_res):
                 # if(have_diff_res and answer_this == "sat"):
                 # if(self.solvers[-2].datas[ins_name].res != self.solvers[-1].datas[ins_name].res):
                     print_line_ct += 1
@@ -271,21 +271,48 @@ if __name__ == "__main__":
     # solvers.append(solver_SAT_standard_gnomon("/pub/data/chenzh/res/sota/p-mcomsps","p-mcomsps"))
     # solvers.append(solver_SAT_standard_gnomon("/pub/data/chenzh/res/sota/treengeling","treengeling"))
     # solvers.append(solver_SAT_standard_gnomon("/pub/data/chenzh/res/sota/pakis","pakis"))
-    solvers.append(solver_SAT_standard_gnomon("/pub/data/chenzh/res/sota/pakis22","pakis22"))
+    # solvers.append(solver_SAT_standard_gnomon("/pub/data/chenzh/res/sota/pakis22","pakis22"))
     solvers.append(solver_SAT_standard_gnomon("/pub/data/chenzh/res/sota/NPS","NPS"))
-    # solvers.append(solver_SAT_standard_gnomon("/pub/data/chenzh/res/sota/pakis-mab","pakis-mab"))
-    # solvers.append(solver_SAT_standard_gnomon("/pub/data/chenzh/res/light/v3--1-preprocess","preprocess"))
-    solvers.append(solver_SAT_standard_gnomon("/pub/data/chenzh/res/light/v4-1-preprocess","pre"))
-    solvers.append(solver_SAT_standard_gnomon("/pub/data/chenzh/res/light/v4-1-nps","sharing-nps"))
-    # solvers.append(solver_SAT_standard_gnomon("/pub/data/chenzh/res/light/v4-2-nps-rp","sharing-nps-rp"))
-    # solvers.append(solver_SAT_standard_gnomon("/pub/data/chenzh/res/light/v4-2-nps-p","sharing-nps-p"))
-    # solvers.append(solver_SAT_standard_gnomon("/pub/data/chenzh/res/light/v4-dps","sharing-dps"))
+
+    # solvers.append(solver_SAT_standard_gnomon("/pub/data/chenzh/res/light/v4-1-nps","sharing-nps"))
+    # solvers.append(solver_SAT_standard_gnomon("/pub/data/chenzh/res/light/v4-2-dps-r","4-2-dps"))
+    # solvers.append(solver_SAT_standard_gnomon("/pub/data/chenzh/res/light/v4-2-dps2-r","4-2-dps2"))
+
+    # solvers.append(solver_SAT_standard_gnomon("/pub/data/chenzh/res/light/v4-3-nps","4-3-sharing-nps"))
+    # solvers.append(solver_SAT_standard_gnomon("/pub/data/chenzh/res/light/v4-3-nps-rp-tc2","4-3-sharing-nps-rp2"))
+    # solvers.append(solver_SAT_standard_gnomon("/pub/data/chenzh/res/light/v4-3-nps-p","4-3-sharing-nps-p"))
+
+    solvers.append(solver_SAT_standard_gnomon("/pub/data/chenzh/res/light/v4-3-nps-tc2","4-3-sharing-nps2"))
+    # solvers.append(solver_SAT_standard_gnomon("/pub/data/chenzh/res/light/v4-3-nps-rp","4-3-sharing-nps-rp"))
+    # solvers.append(solver_SAT_standard_gnomon("/pub/data/chenzh/res/light/v4-3-nps-p-tc2","4-3-sharing-nps-p2"))
+    # solvers.append(solver_SAT_standard_gnomon("/pub/data/chenzh/res/light/v4-3-nopre-sharing-r","4-3-nopre"))
+    # solvers.append(solver_SAT_standard_gnomon("/pub/data/chenzh/res/light/v4-3-nosharing-r","4-3-nosharing"))
+
+    # solvers.append(solver_SAT_standard_gnomon("/pub/data/chenzh/res/light/v4-4-nps-2","thread2"))
+    # solvers.append(solver_SAT_standard_gnomon("/pub/data/chenzh/res/light/v4-4-nps-4","thread4"))
+    # solvers.append(solver_SAT_standard_gnomon("/pub/data/chenzh/res/light/v4-4-nps-8","thread8"))
+    # solvers.append(solver_SAT_standard_gnomon("/pub/data/chenzh/res/light/v4-4-nps-16","thread16"))
+    # solvers.append(solver_SAT_standard_gnomon("/pub/data/chenzh/res/light/v4-3-nps-tc2","thread32"))
+    # solvers.append(solver_SAT_standard_gnomon("/pub/data/chenzh/res/light/v4-4-nps-64","thread64"))
+    # solvers.append(solver_SAT_standard_gnomon("/pub/data/chenzh/res/light/v4-4-nps-64-2","thread64-2"))
+
+
+    
+    # solvers.append(solver_SAT_standard_gnomon("/pub/data/chenzh/res/light/v4-3-nps-tc3","4-3-sharing-nps3"))
+    # solvers.append(solver_SAT_standard_gnomon("/pub/data/chenzh/res/light/v4-3-nps-tc4","4-3-sharing-nps4"))
+    solvers.append(solver_SAT_standard_gnomon("/pub/data/chenzh/res/light/v5-5-dps-20","5-5-dps-20"))
+    solvers.append(solver_SAT_standard_gnomon("/pub/data/chenzh/res/light/v5-6-dps-2","5-6-dps-2"))
+    solvers.append(solver_SAT_standard_gnomon("/pub/data/chenzh/res/light/v5-7-dps-20-1k","5-7-dps-20-1k"))
+    solvers.append(solver_SAT_standard_gnomon("/pub/data/chenzh/res/light/v5-7-dps-20-2k","5-7-dps-20-2k"))
+    solvers.append(solver_SAT_standard_gnomon("/pub/data/chenzh/res/light/v5-7-dps-20-4k","5-7-dps-20-4k"))
 
     # append_all_solvers_in_dir(solvers, "/pub/data/chenzh/res/light/")
     samples = []
-    samples.append(["/pub/data/chenzh/data/sat2020/vbs.txt", "vbs"])
-    samples.append(["/pub/data/chenzh/data/sat2021/vbs.txt", "vbs"])
+    # samples.append(["/pub/data/chenzh/data/sat2020/vbs.txt", "vbs"])
+    # samples.append(["/pub/data/chenzh/data/sat2021/vbs.txt", "vbs"])
+    samples.append(["/pub/data/chenzh/data/sat2022/vbs.txt", "vbs"])
     # samples.append(["/pub/data/chenzh/data/sat2022/all.txt", "all"])
+    # samples.append(["/pub/data/chenzh/data/sat2022/unknown.txt", "unknown"])
     clt = calculater(solvers, samples)
     clt.cal_and_show()
 

testLight/dps.log

@@ -0,0 +1,347 @@
+nohup: ignoring input
+10pipe_k.cnf
+13pipe_k.cnf
+14pipe_q0_k.cnf
+20-100-frag12-0_sat.cnf
+20-100-frag12-14_sat.cnf
+20-100-frag12-32_sat.cnf
+20-100-frag12-53_sat.cnf
+20-100-lambda100-14_sat.cnf
+20-100-lambda100-14_unsat.cnf
+20-100-lambda100-47_unsat.cnf
+20-100-lambda100-49_sat.cnf
+20-100-lambda100-65_sat.cnf
+20-100-lambda100-89_sat.cnf
+20-100-lambda100-89_unsat.cnf
+20-100-p100-55_sat.cnf
+20-100-p100-55_unsat.cnf
+2bitcomp_5.hg_20.cnf
+51.smt2.cnf
+73.smt2.cnf
+9dlx_vliw_at_b_iq5.cnf
+9dlx_vliw_at_b_iq8.cnf
+ACG-15-10p1.cnf
+ak016modbtsimpbisc.cnf
+ak032modbtmodbtisc.cnf
+ak128paralparalisc.cnf
+assoc_mult_err_3.c.cnf
+at-least-two-aaai10-planning-ipc5-pathways-17-step20.cnf
+at-least-two-aaai10-planning-ipc5-pipesworld-12-step15.cnf
+at-least-two-hwmcc10-timeframe-expansion-k50-pdtviseisenberg2-tseitin.cnf
+at-least-two-ibm-2004-23-k100.cnf
+at-least-two-maris-s03-gripper11.cnf
+at-least-two-smtlib-qfbv-aigs-ext_con_032_008_0256-tseitin.cnf
+at-least-two-sokoban-sequential-p145-microban-sequential.030-NOTKNOWN.cnf
+at-least-two-traffic_b_unsat.cnf
+at-least-two-traffic_f_unknown.cnf
+at-least-two-traffic_kkb_unknown.cnf
+at-least-two-traffic_pcb_unknown.cnf
+vmpc_26.cnf
+at-least-two-vmpc_28.cnf
+b04_s_unknown_pre.cnf
+b2005-p3-12x12c10h7-Ser7-0.cnf
+barman-pfile10-039.sas.ex.15.cnf
+barman-pfile10-040.sas.ex.15.cnf
+battleship-12-12-unsat.cnf
+battleship-14-26-sat.cnf
+blocks-blocks-36-0.180-SAT.cnf
+blocks-blocks-37-1.120-NOTKNOWN.cnf
+blocks-blocks-37-1.130-NOTKNOWN.cnf
+bvsdiv_19.smt2.cnf
+bvsmod_18.smt2.cnf
+bvsmod_19.smt2.cnf
+bvsub_08985.smt2.cnf
+bvsub_12973.smt2.cnf
+bvsub_19952.smt2.cnf
+bv-term-small-rw_1492.smt2.cnf
+bvurem_20.smt2.cnf
+Circuit_multiplier18.cnf
+Circuit_multiplier22.cnf
+Circuit_multiplier24.cnf
+Circuit_multiplier25.cnf
+Circuit_multiplier26.cnf
+Circuit_multiplier29.cnf
+Circuit_multiplier33.cnf
+Circuit_multiplier34.cnf
+Circuit_multiplier35.cnf
+Circuit_multiplier36.cnf
+Circuit_multiplier37.cnf
+Circuit_multiplier45.cnf
+Circuit_multiplier53.cnf
+crafted_n10_d6_c4_num15.cnf
+crafted_n10_d6_c4_num21.cnf
+crafted_n11_d6_c4_num14.cnf
+crafted_n12_d6_c3_num18.cnf
+crafted_n12_d6_c3_num28.cnf
+crafted_n12_d6_c4_num17.cnf
+ctl_4201_555_unsat.cnf
+ctl_4291_567_1_unsat.cnf
+ctl_4291_567_11_unsat.cnf
+ctl_4291_567_6_unsat_pre.cnf
+ctl_4291_567_9_unsat.cnf
+dist10.c.cnf
+dist4.c.cnf
+E00X23.cnf
+E02F17.cnf
+ecarev-110-1031-23-40-8.cnf
+ecarev-110-4099-22-30-4.cnf
+edit_distance007_85.cnf
+edit_distance019_312.cnf
+edit_distance023_281.cnf
+edit_distance023_282.cnf
+edit_distance023_283.cnf
+edit_distance025_448.cnf
+edit_distance025_449.cnf
+edit_distance025_450.cnf
+edit_distance031_283.cnf
+edit_distance031_284.cnf
+edit_distance035_393.cnf
+edit_distance041_182.cnf
+edit_distance041_183.cnf
+ER_500_40_2.apx_0.cnf
+erin2_0x0_n207-379.cnf
+erin2_0x0-379.cnf
+erin2_0x1e3-216.cnf
+ex045_7.cnf
+ex065_25.cnf
+ex095_8.cnf
+ex175_20.cnf
+HCP-424-60.cnf
+HCP-446-105.cnf
+HCP-446-420.cnf
+HCP-446-60.cnf
+HCP-470-105.cnf
+HCP-470-420.cnf
+HCP-470-60.cnf
+HCP-506-60.cnf
+HCP-522-105.cnf
+HCP-526-105.cnf
+HCP-526-420.cnf
+HCP-529-420.cnf
+HCP-529-60.cnf
+huck.col.11.cnf
+IBM_FV_2004_rule_batch_30_SAT_dat.k75.cnf
+k2fix_gr_rcs_w8.shuffled.cnf
+Kakuro-easy-045-ext.xml.hg_4.cnf
+Kakuro-easy-051-ext.xml.hg_4.cnf
+Kakuro-easy-089-ext.xml.hg_4.cnf
+Kakuro-easy-104-ext.xml.hg_6.cnf
+Kakuro-easy-112-ext.xml.hg_7.cnf
+Kakuro-easy-115-ext.xml.hg_5.cnf
+Kakuro-easy-118-ext.xml.hg_4.cnf
+Kakuro-easy-127-ext.xml.hg_7.cnf
+Kakuro-easy-132-ext.xml.hg_8.cnf
+Kakuro-easy-142-ext.xml.hg_8.cnf
+Kakuro-easy-150-ext.xml.hg_9.cnf
+Kakuro-easy-156-ext.xml.hg_7.cnf
+ktf_TF-1.tf_4_0.06_101.cnf
+ktf_TF-3.tf_2_0.02_24.cnf
+ktf_TF-3.tf_3_0.02_24.cnf
+ktf_TF-4.tf_2_0.02_18.cnf
+ktf_TF-4.tf_4_0.04_35.cnf
+ktf_TF-4.tf_4_0.06_52.cnf
+ktf_TF-6.tf_4_0.06_77.cnf
+ktf_TF-7.tf_3_0.06_113.cnf
+ktf_TF-8.tf_4_0.06_109.cnf
+LABS_n041_goal003.cnf
+LABS_n068_goal001.cnf
+LABS_n069_goal001.cnf
+LABS_n072_goal006.cnf
+LABS_n089_goal008.cnf
+maximum_constrained_partition_14_bits_n200.cnf
+maximum_constrained_partition_18_bits_n200.cnf
+maxor128.cnf
+mp1-blockpuzzle_5x10_s5_free3.cnf
+mp1-blockpuzzle_5x12_s6_free3.cnf
+mp1-blockpuzzle_9x9_s1_free8.cnf
+mp1-blockpuzzle_9x9_s5_free3.cnf
+mp1-bsat201-707.cnf
+mp1-bsat210-739.cnf
+mp1-klieber2017s-0300-034-t12.cnf
+mp1-klieber2017s-0490-024-t12.cnf
+mp1-klieber2017s-1000-023-eq.cnf
+mp1-klieber2017s-1000-024-eq.cnf
+mp1-klieber2017s-1200-022-eq.cnf
+mp1-klieber2017s-2000-022-eq.cnf
+mp1-Nb6T06.cnf
+mp1-Nb6T07.cnf
+mp1-Nb7T44.cnf
+mp1-Nb7T46.cnf
+mp1-squ_ali_s10x10_c39_abio_SAT.cnf
+mp1-squ_any_s09x07_c27_abix_UNS.cnf
+mp1-tri_ali_s11_c35_abix_UNS.cnf
+mp1-tri_ali_s11_c35_bail_UNS.cnf
+MVD_ADS_S1_5_5.cnf
+MVD_ADS_S10_5_6.cnf
+MVD_ADS_S10_6_6.cnf
+MVD_ADS_S11_6_7.cnf
+MVD_ADS_S11_7_7.cnf
+MVD_ADS_S11_8_7.cnf
+MVD_ADS_S3_5_5.cnf
+MVD_ADS_S4_5_5.cnf
+MVD_ADS_S5_6_6.cnf
+MVD_ADS_S6_6_5.cnf
+MVD_ADS_S6_6_6.cnf
+MVD_ADS_S7_6_6.cnf
+MVD_ADS_S9_6_6.cnf
+Mycielski-10-hints-10.cnf
+Mycielski-10-hints-7.cnf
+Mycielski-10-hints-8.cnf
+Mycielski-10-hints-9.cnf
+Mycielski-11-hints-1.cnf
+Mycielski-11-hints-2.cnf
+Mycielski-11-hints-3.cnf
+Mycielski-11-hints-4.cnf
+n320p5q2_n.apx_16.cnf
+n320p5q2_n.apx_17.cnf
+Nb51T6.cnf
+ndhf_xits_09_UNSAT.cnf
+p01_lb_05.cnf
+pb_300_05_lb_16.cnf
+pb_300_05_lb_17.cnf
+pb_300_06_lb_02.cnf
+pb_300_10_lb_06.cnf
+php12e12.cnf
+prime_a20_b20.cnf
+prime_a22_b22.cnf
+prime_a24_b24.cnf
+puzzle30_sat.cnf
+puzzle34_sat.cnf
+puzzle34_unsat.cnf
+puzzle35_sat.cnf
+puzzle35_unsat.cnf
+puzzle36_sat.cnf
+puzzle37_unsat.cnf
+puzzle39_sat.cnf
+puzzle42_sat.cnf
+puzzle44_unsat.cnf
+quad_res_r21_m22.cnf
+quad_res_r26_m27.cnf
+quad_res_r28_m29.cnf
+quad_res_r29_m32.cnf
+randomG-B-Mix-n15-d05.cnf
+randomG-B-Mix-n16-d05.cnf
+randomG-B-Mix-n18-d05.cnf
+randomG-Mix-n17-d05.cnf
+randomG-Mix-n18-d05.cnf
+randomG-n16-d05.cnf
+randomG-n17-d05.cnf
+randomG-n18-d05.cnf
+randomG-n19-d05.cnf
+randomG-n20-d05.cnf
+rphp4_065_shuffled.cnf
+rphp4_080_shuffled.cnf
+rphp4_090_shuffled.cnf
+rpoc_xits_10_UNKNOWN.cnf
+satch2ways12u.cnf
+satch2ways12wu.cnf
+satch2ways13wu.cnf
+satch2ways14u.cnf
+satch2ways15.cnf
+satch2ways15u.cnf
+satch2ways15wu.cnf
+satch2ways16.cnf
+satch2ways16w.cnf
+SC21_Timetable_C_466_E_62_Cl_31_S_30.cnf
+SC21_Timetable_C_527_E_71_Cl_35_S_35.cnf
+SC21_Timetable_C_542_E_71_Cl_36_S_35.cnf
+SC21_Timetable_C_557_E_73_Cl_37_S_35.cnf
+scc_1213_40_10_3.apx_0.cnf
+stb_531_83.apx_1.cnf
+stb_588_138.apx_1.cnf
+SE_PR_WS_500_16_70_10.apx_0.cnf
+shift1add.26949.cnf
+size_5_5_5_i003_r12.cnf
+size_5_5_5_i223_r12.cnf
+size_5_5_5_i251_r12.cnf
+snw_13_8_pre.cnf
+snw_13_8_pre-sc2016.cnf
+snw_13_9_pre.cnf
+snw_16_9_Encpre.cnf
+sokoban-p16.sas.ex.19-sc2016.cnf
+sokoban-p20.sas.cr.21.cnf
+sokoban-p20.sas.cr.27.cnf
+sokoban-p20.sas.ex.13.cnf
+sokoban-sequential-p145-microban-sequential.070-NOTKNOWN.cnf
+sp4-33-bin-stri-flat-noid.cnf
+sp4-33-one-nons-flat-noid.cnf
+sp4-33-one-stri-tree-noid.cnf
+sp4-33-una-stri-flat-noid.cnf
+sp5-21-15-bin-stri-flat-noid.cnf
+sp5-21-15-bin-stri-tree-noid.cnf
+sp5-21-15-one-nons-tree-noid.cnf
+sp5-21-15-one-stri-tree-noid.cnf
+sp5-21-15-una-nons-tree-noid.cnf
+sp5-21-15-una-stri-flat-noid.cnf
+sp5-26-19-bin-nons-tree-noid.cnf
+sp5-26-19-bin-stri-flat-noid.cnf
+sp5-26-19-una-nons-tree-noid.cnf
+spg_200_300.cnf
+spg_200_301.cnf
+spg_200_307.cnf
+spg_200_316.cnf
+spg_200_317.cnf
+spg_200_321.cnf
+spg_300_300.cnf
+spg_300_301.cnf
+spg_300_312.cnf
+spg_330_400.cnf
+spg_400_281.cnf
+spg_420_280.cnf
+spg_420_350.cnf
+stb_531_83.apx_0.cnf
+stb_792_333.apx_0.cnf
+sted1_0x0-637.cnf
+sted1_0x1e3-393.cnf
+sted12a_0x1e1-67.cnf
+sted2_0x0-343.cnf
+sted2_0x1e3-216.cnf
+sted3_0x0_n201-239.cnf
+sted4_0x0_n159-185.cnf
+sted5_0x0_n90-157.cnf
+sted5_0x1e3-120.cnf
+sted5_0x1e3-20.cnf
+sted6_0x1e3-97.cnf
+string_compare_safety_cbmc_unwinding_600.cnf
+string_compare_safety_cbmc_unwinding_630.cnf
+string_compare_safety_cbmc_unwinding_670.cnf
+string_compare_safety_cbmc_unwinding_680.cnf
+string_compare_safety_cbmc_unwinding_690.cnf
+string_compare_safety_cbmc_unwinding_700.cnf
+string_compare_safety_cbmc_unwinding_730.cnf
+string_compare_safety_cbmc_unwinding_780.cnf
+string_compare_safety_cbmc_unwinding_800.cnf
+string_compare_safety_cbmc_unwinding_870.cnf
+string_compare_safety_cbmc_unwinding_900.cnf
+string_compare_safety_cbmc_unwinding_930.cnf
+string_compare_safety_cbmc_unwinding_940.cnf
+sum_of_3_cubes_37_bits_87.cnf
+sum_of_3_cubes_42_bits_96.cnf
+sum_of_3_cubes_50_bits_91.cnf
+sum_of_3_cubes_51_bits_80.cnf
+sum_of_3_cubes_52_bits_39.cnf
+Sz1024_34824.smt2.cnf
+Sz512_15128_1.smt2.cnf
+test_v7_r12_vr1_c1_s10576.smt2.cnf
+toughsat_factoring_426s.cnf
+toughsat_factoring_895s.cnf
+UCG-20-10p1-sc2009.cnf
+UR-15-10p0.cnf
+g2-UR-20-5p1.cnf
+vlsat2_11_26.cnf
+vlsat2_11_42.cnf
+vlsat2_111_1186.cnf
+vlsat2_112_4223.cnf
+vlsat2_113_1150.cnf
+vlsat2_142_6781.cnf
+vlsat2_144_7585.cnf
+vlsat2_297_3780.cnf
+vlsat2_377_5364.cnf
+vlsat2_44_545.cnf
+vlsat2_51_824.cnf
+vlsat2_56_1042.cnf
+vlsat2_702_14170.cnf
+WS_300_24_90_10.apx_0.cnf
+WS_400_16_90_70.apx_0.cnf
+WS_500_16_70_10.apx_0.cnf
+WS_500_32_30_10.apx_0.cnf

testLight/run10-1.sh

@@ -0,0 +1,150 @@
+#!/bin/bash
+
+SEND_THREAD_NUM=4
+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
+instance_20="/pub/data/chenzh/data/sat2020"
+instance_21="/pub/data/chenzh/data/sat2021"
+instance_22="/pub/data/chenzh/data/sat2022"
+
+
+res1="/pub/data/chenzh/res/light/v1-origin"
+res2="/pub/data/chenzh/res/light/v4-1-preprocess"
+res3="/pub/data/chenzh/res/light/v1-1-origin"
+res4="/pub/data/chenzh/res/light/v2-preprocess"
+res5="/pub/data/chenzh/res/light/v3--1-preprocess"
+res6="/pub/data/chenzh/res/light/v4-3-rp"
+res_no="/pub/data/chenzh/res/unused"
+#####################################################
+
+all_datas=($instance_21)
+for((i=0;i<${#all_datas[*]};i++))
+do
+	instance=${all_datas[$i]}
+
+	res_solver_ins=$res6
+	if [ ! -d "$res_solver_ins" ]; then
+		mkdir -p $res_solver_ins
+	fi
+	for dir_file in `cat $instance/vbs.txt`
+	do
+		file=$dir_file
+		echo $file
+		touch $res_solver_ins/$file
+		read -u 6
+		{
+			cd /home/chenzh/solvers/Light
+			time ./light-v4-3 $instance/$file --pakis=1
+			echo >&6
+		} >$res_solver_ins/$file  2>>$res_solver_ins/$file &
+	done
+
+	# res_solver_ins=$res5
+	# if [ ! -d "$res_solver_ins" ]; then
+	# 	mkdir -p $res_solver_ins
+	# fi
+	# for dir_file in `cat $instance/vbs.txt`
+	# do
+	# 	file=$dir_file
+	# 	echo $file
+	# 	touch $res_solver_ins/$file
+	# 	read -u 6
+	# 	{
+	# 		cd /home/chenzh/solvers/Light
+	# 		time ./light-v3--1 $instance/$file --share=1 --threads=31
+	# 		echo >&6
+	# 	} >$res_solver_ins/$file  2>>$res_solver_ins/$file &
+	# done
+	# res_solver_ins=$res4
+	# if [ ! -d "$res_solver_ins" ]; then
+	# 	mkdir -p $res_solver_ins
+	# fi
+	# for dir_file in `cat $instance/vbs.txt`
+	# do
+	# 	file=$dir_file
+	# 	echo $file
+	# 	touch $res_solver_ins/$file
+	# 	read -u 6
+	# 	{
+	# 		cd /home/chenzh/solvers/Light
+	# 		time ./light-v2 $instance/$file --share=1 --threads=31
+	# 		echo >&6
+	# 	} >$res_solver_ins/$file  2>>$res_solver_ins/$file &
+	# done
+
+	# res_solver_ins=$res3
+	# if [ ! -d "$res_solver_ins" ]; then
+	# 	mkdir -p $res_solver_ins
+	# fi
+	# for dir_file in `cat $instance/vbs.txt`
+	# do
+	# 	file=$dir_file
+	# 	echo $file
+	# 	touch $res_solver_ins/$file
+	# 	read -u 6
+	# 	{
+	# 		cd /home/chenzh/solvers/Light
+	# 		time ./light-v1-1 $instance/$file --simplify=0 --reset=1
+	# 		echo >&6
+	# 	} >$res_solver_ins/$file  2>>$res_solver_ins/$file &
+	# done
+
+	# res_solver_ins=$res2
+	# if [ ! -d "$res_solver_ins" ]; then
+	# 	mkdir -p $res_solver_ins
+	# fi
+	# for dir_file in `cat $instance/vbs.txt`
+	# do
+	# 	file=$dir_file
+	# 	echo $file
+	# 	touch $res_solver_ins/$file
+	# 	read -u 6
+	# 	{
+	# 		cd /home/chenzh/solvers/Light
+	# 		time ./light-v4-1 $instance/$file --simplify=1
+	# 		echo >&6
+	# 	} >$res_solver_ins/$file  2>>$res_solver_ins/$file &
+	# done
+
+	# res_solver_ins=$res1
+	# if [ ! -d "$res_solver_ins" ]; then
+	# 	mkdir -p $res_solver_ins
+	# fi
+	# for dir_file in `cat $instance/vbs.txt`
+	# do
+	# 	file=$dir_file
+	# 	echo $file
+	# 	touch $res_solver_ins/$file
+	# 	read -u 6
+	# 	{
+	# 		cd /home/chenzh/solvers/Light
+	# 		time ./light-v1 $instance/$file --simplify=0
+	# 		echo >&6
+	# 	} >$res_solver_ins/$file  2>>$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<4;i++))
+do
+	read -u 6
+	{
+		cd /home/chenzh/solvers/Light
+		time ./light-v1 /home/chenzh/data/hard_cnfs/49.cnf
+		echo >&6
+	} >$res_solver_ins/$i  2>>$res_solver_ins/$i &
+done
+
+
+exit 0

testLight/run10-2.sh

@@ -0,0 +1,150 @@
+#!/bin/bash
+
+SEND_THREAD_NUM=4
+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
+instance_20="/pub/data/chenzh/data/sat2020"
+instance_21="/pub/data/chenzh/data/sat2021"
+instance_22="/pub/data/chenzh/data/sat2022"
+
+
+res1="/pub/data/chenzh/res/light/v1-origin"
+res2="/pub/data/chenzh/res/light/v4-1-preprocess"
+res3="/pub/data/chenzh/res/light/v1-1-origin"
+res4="/pub/data/chenzh/res/light/v2-preprocess"
+res5="/pub/data/chenzh/res/light/v3--1-preprocess"
+res6="/pub/data/chenzh/res/light/v4-3-rp"
+res_no="/pub/data/chenzh/res/unused"
+#####################################################
+
+all_datas=($instance_22)
+for((i=0;i<${#all_datas[*]};i++))
+do
+	instance=${all_datas[$i]}
+
+	res_solver_ins=$res6
+	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/chenzh/solvers/Light
+			time ./light-v4-3 $instance/$file --pakis=1
+			echo >&6
+		} >$res_solver_ins/$file  2>>$res_solver_ins/$file &
+	done
+
+	# res_solver_ins=$res5
+	# if [ ! -d "$res_solver_ins" ]; then
+	# 	mkdir -p $res_solver_ins
+	# fi
+	# for dir_file in `cat $instance/vbs.txt`
+	# do
+	# 	file=$dir_file
+	# 	echo $file
+	# 	touch $res_solver_ins/$file
+	# 	read -u 6
+	# 	{
+	# 		cd /home/chenzh/solvers/Light
+	# 		time ./light-v3--1 $instance/$file --share=1 --threads=31
+	# 		echo >&6
+	# 	} >$res_solver_ins/$file  2>>$res_solver_ins/$file &
+	# done
+	# res_solver_ins=$res4
+	# if [ ! -d "$res_solver_ins" ]; then
+	# 	mkdir -p $res_solver_ins
+	# fi
+	# for dir_file in `cat $instance/vbs.txt`
+	# do
+	# 	file=$dir_file
+	# 	echo $file
+	# 	touch $res_solver_ins/$file
+	# 	read -u 6
+	# 	{
+	# 		cd /home/chenzh/solvers/Light
+	# 		time ./light-v2 $instance/$file --share=1 --threads=31
+	# 		echo >&6
+	# 	} >$res_solver_ins/$file  2>>$res_solver_ins/$file &
+	# done
+
+	# res_solver_ins=$res3
+	# if [ ! -d "$res_solver_ins" ]; then
+	# 	mkdir -p $res_solver_ins
+	# fi
+	# for dir_file in `cat $instance/vbs.txt`
+	# do
+	# 	file=$dir_file
+	# 	echo $file
+	# 	touch $res_solver_ins/$file
+	# 	read -u 6
+	# 	{
+	# 		cd /home/chenzh/solvers/Light
+	# 		time ./light-v1-1 $instance/$file --simplify=0 --reset=1
+	# 		echo >&6
+	# 	} >$res_solver_ins/$file  2>>$res_solver_ins/$file &
+	# done
+
+	# res_solver_ins=$res2
+	# if [ ! -d "$res_solver_ins" ]; then
+	# 	mkdir -p $res_solver_ins
+	# fi
+	# for dir_file in `cat $instance/vbs.txt`
+	# do
+	# 	file=$dir_file
+	# 	echo $file
+	# 	touch $res_solver_ins/$file
+	# 	read -u 6
+	# 	{
+	# 		cd /home/chenzh/solvers/Light
+	# 		time ./light-v4-1 $instance/$file --simplify=1
+	# 		echo >&6
+	# 	} >$res_solver_ins/$file  2>>$res_solver_ins/$file &
+	# done
+
+	# res_solver_ins=$res1
+	# if [ ! -d "$res_solver_ins" ]; then
+	# 	mkdir -p $res_solver_ins
+	# fi
+	# for dir_file in `cat $instance/vbs.txt`
+	# do
+	# 	file=$dir_file
+	# 	echo $file
+	# 	touch $res_solver_ins/$file
+	# 	read -u 6
+	# 	{
+	# 		cd /home/chenzh/solvers/Light
+	# 		time ./light-v1 $instance/$file --simplify=0
+	# 		echo >&6
+	# 	} >$res_solver_ins/$file  2>>$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<4;i++))
+do
+	read -u 6
+	{
+		cd /home/chenzh/solvers/Light
+		time ./light-v1 /home/chenzh/data/hard_cnfs/49.cnf
+		echo >&6
+	} >$res_solver_ins/$i  2>>$res_solver_ins/$i &
+done
+
+
+exit 0