modified python bugs, add some args, 14 threads version

sources/core/Solver.cc

@@ -69,7 +69,9 @@ static DoubleOption  opt_lastflipRatio(_cat,"initFlipRatio","initial & now steps
 static DoubleOption  opt_timeRatio    (_cat,"timeRatio","cnnrTime / totalTime",  0.35, DoubleRange(0, true, 1.5, true));
 static DoubleOption  opt_raiseFlipRatio(_cat,"raiseFlipRatio","lastflipRatio*=raiseFlipRatio every time call cnnr",  1.02, DoubleRange(1, true, 5, true));
 static DoubleOption  opt_switchMode(_cat,"switchMode","time to switch to VSIDS",  2500, DoubleRange(0, true, 6000, true));
-
+static BoolOption    opt_aspiration(_cat,"aspiration","if turn on aspiration",true);
+static DoubleOption  opt_swt_threshold(_cat,"threshold","_swt_threshold in cnnr",50,DoubleRange(0,true,400,true));
+static DoubleOption  opt_swt_q(_cat,"swt_q","_swt_q in cnnr",0.7,DoubleRange(0,true,1,true));
 //==============
 
 
@@ -168,6 +170,10 @@ Solver::Solver() :
   , solvedByUncom       (false)
   , forceRestart        (false)
   , lastLearntNum       (0)
+  , aspiration          (opt_aspiration)
+  , swt_q               (opt_swt_q)
+  , swt_threshold       (opt_swt_threshold)
+
 //=============================
 {
     //--------------------------------
@@ -2239,7 +2245,8 @@ lbool Solver::solve_()
         //printf("c | Conflicts |          ORIGINAL         |          LEARNT          | Progress |\n");
         //printf("c |           |    Vars  Clauses Literals |    Limit  Clauses Lit/Cl |          |\n");
         printf("c areaRatio:%lf         conflRatio:%lf          timeRatio:%lf\n",areaRatio,conflRatio,timeRatio);
-        printf("c maxFlipRatio:%lf    initFlipRatio:%lf     raiseFlipRatio:%lf\t \n",maxflipRatio,lastflipRatio,raiseFlipRatio);
+        printf("c maxFlipRatio:%lf    initFlipRatio:%lf     raiseFlipRatio:%lf\n",maxflipRatio,lastflipRatio,raiseFlipRatio);
+        printf("c aspiration:%s            swt_q:%lf             swt_threshold:%lf \n",(aspiration?"true":"false"),swt_q,swt_threshold);
         printf("c -------------------------------------------------------------------------------\n");
         printf("c call|nRestart|trueRatio|expect|LastLearnts|Learnts|ccnrTime |totalTime |  end\n");       
         printf("c ===============================================================================\n");
@@ -2506,9 +2513,14 @@ bool Solver::callUnCom(){
 bool Solver::callUnCom(){
        
     ls_solver ccnr;
-    
+
     int	ret = build_instance(ccnr);
 
+
+    ccnr.aspiration = this->aspiration;
+    ccnr._swt_q = this->swt_q;
+    ccnr._swt_threshold = this->swt_threshold;
+
     if (!ret) { printf("c init fail\n");return 1;}
 
     if(timeRatio <= 1){

sources/core/Solver.h

@@ -470,6 +470,9 @@ public:
     bool    solvedByUncom      ;// = false;
     bool    forceRestart       ;// = false;
     int     lastLearntNum      ;// = 0;
+    bool    aspiration         ;
+    double  swt_q              ;
+    double  swt_threshold      ;
     //;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;
     
     void getInitModelByValue();

sources/simp/pmaple.py

@@ -56,7 +56,7 @@ else:
 # setup tmp files
 #
 tmpDir = "/tmp/"
-print ("c found " + str(len(sys.argv)) + "parameters")
+print ("c found " + str(len(sys.argv)) + " parameters")
 if (len(sys.argv) > 5):
     tmpDir = sys.argv[5]
 if (tmpDir[-1:] != '/'):
@@ -158,7 +158,7 @@ if winnerCode != 0:
         shutil.copyfileobj(f, sys.stdout)
 
     if (proof != "/dev/null"):
-        tmpProof = proof + tmpBassename + "reasonLS_" + str(winnerseed)
+        tmpProof = tmpBassename + proof + "reasonLS_" + str(winnerseed)
         if( not os.path.exists(pathz) ):
             os.mkdir(pathz)
         if( os.path.exists(tmpDir+tmpProof)):
@@ -170,8 +170,12 @@ else:
 
 # kill the other process, and its child processes
 for p in pids:
-    if(check_pid(p)):
-        os.kill(-p, 15)
+    try:
+        os.kill(p, 15)
+    except OSError:
+        #do nothing
+    else:
+        #do nothing
 
 # clean up the temporary files
 for i in range(numCores):
@@ -183,8 +187,8 @@ for i in range(numCores):
         os.unlink(tmpFile + ".out")
     if(proof != "/dev/null"):
         tmpProof = tmpDir + tmpBassename + proof + "reasonLS_" + str(seed)
-        if(os.path.exists(tmpProof)):
-            os.unlink(tmpProof)
+        #if(os.path.exists(tmpProof)):
+        os.unlink(tmpProof)
 
 # exit with the correct exit code
 sys.exit(winnerCode)

sources/utils/ccnr.cc

@@ -140,6 +140,7 @@ ls_solver::ls_solver()
 	_swt_threshold = 50;
 	_swt_p = 0.3;
 	_swt_q = 0.7;
+	aspiration = true;
 }
 /******************************the top function******************************/
 /**********************************build instance*******************************/
@@ -399,24 +400,30 @@ int 	ls_solver::pick_var()
 	}
 	
 	//Aspriation Mode
-	_aspiration_score=_avg_clause_weight;
-	for(i=0;i<_unsat_vars.size();++i)
-	{
-		v=_unsat_vars[i];
-		if(_vars[v].score>_aspiration_score)
+
+	//----------------------------------------
+	if(aspiration){
+		_aspiration_score=_avg_clause_weight;
+		for(i=0;i<_unsat_vars.size();++i)
 		{
-			best_var=v;
-			break;
+			v=_unsat_vars[i];
+			if(_vars[v].score>_aspiration_score)
+			{
+				best_var=v;
+				break;
+			}
 		}
+		for(++i;i<_unsat_vars.size();++i)
+		{
+			v=_unsat_vars[i];
+			if(_vars[v].score>_vars[best_var].score) best_var=v;
+			else if(_vars[v].score==_vars[best_var].score && _vars[v].last_flip_step<_vars[best_var].last_flip_step) best_var=v;
+		}
+		if(best_var!=0) return best_var;
 	}
-	for(++i;i<_unsat_vars.size();++i)
-	{
-		v=_unsat_vars[i];
-		if(_vars[v].score>_vars[best_var].score) best_var=v;
-		else if(_vars[v].score==_vars[best_var].score && _vars[v].last_flip_step<_vars[best_var].last_flip_step) best_var=v;
-	}
-	if(best_var!=0) return best_var;
-	
+	//=========================================
+
+
 	/**Diversification Mode**/
 	update_clause_weights();	
 	/*focused random walk*/	

sources/utils/ccnr.h

@@ -141,6 +141,9 @@ public:
 	float 	_swt_p;//w=w*p+ave_w*q
 	float 	_swt_q;
 	int		_avg_clause_weight;
+	//-------------------
+	bool 	aspiration;
+	//=================
 	long long		_delta_total_clause_weight;
 	//main functions
 	void	initialize(const vector<bool>* init_solution = 0);