0413 with 24 threads,modify pmaple's bugs

ReasonLS-run.sh

@@ -1,4 +1,4 @@
 #! /bin/bash
 
 cd bin
-python ./pmaple.py $1 6 14 -drup-file=$2/proof.out
+python ./pmaple.py $1 6 24 -drup-file=$2/proof.out

sources/core/Solver.cc

@@ -69,8 +69,8 @@ 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 IntOption     opt_aspiration(_cat,"aspiration","if turn on aspiration",1,IntRange(0,1));
+static DoubleOption  opt_swt_threshold(_cat,"swt_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));
 //==============
 
@@ -170,7 +170,7 @@ Solver::Solver() :
   , solvedByUncom       (false)
   , forceRestart        (false)
   , lastLearntNum       (0)
-  , aspiration          (opt_aspiration)
+  , aspiration          ((opt_aspiration==1)?true:false)
   , swt_q               (opt_swt_q)
   , swt_threshold       (opt_swt_threshold)
 
@@ -2551,7 +2551,9 @@ bool Solver::callUnCom(){
         //largely increase call time of cnnr
         ccnr._max_steps = maxstep;
         ccnr._max_tries = 10;
-        if(ccnr.local_search()){
+
+        vector<bool> * vp = 0;
+        if(ccnr.local_search(vp)){
 
             //ccnr.print_solution();
             result_call.clear();

sources/simp/Main.cc

@@ -54,6 +54,8 @@ void printStats(Solver& solver)
     printf("c conflict literals     : %-12"PRIu64"   (%4.2f %% deleted)\n", solver.tot_literals, (solver.max_literals - solver.tot_literals)*100 / (double)solver.max_literals);
     if (mem_used != 0) printf("c Memory used           : %.2f MB\n", mem_used);
     printf("c CPU time              : %g s\n", cpu_time);
+    printf("c Unc CPU time          : %g s\n",solver.UnComTime);
+    printf("c Unc call times        : %d \n", solver.callNum);
 }
 
 

sources/simp/pmaple.py

@@ -19,6 +19,16 @@ def check_pid(pid):
     else:
         return True
 
+def kill_pid(pid):        
+    """ Check For the existence of a unix pid. """
+    try:
+        os.kill(pid, 15)
+    except OSError:
+        return False
+    else:
+        return True
+
+
 #
 # usage and current PID
 #
@@ -76,13 +86,18 @@ random.seed(seed)
 pids = set()
 pidsseed = set()
 seeds = set()
+            #  1        2       3       4       5       6       7       8       9       10      11      12      13      14      15      16      17      18      19      20      21      22      23      24
+confl       = [0.9,     0.9,    0.9,    0.9,    0.9,    0.9,    0.9,    0.1,    0.1,    0.1,    0.1,    0.1,    0.1,    0.1,    0.1,    0.1,    0.9,    0.7,    0.5,    0.9,    0.7,    0.5,    1,      1]
+area        = [1.01,    1.01,   1.01,   1.01,   1.01,   1.01,   1.01,   1.01,   1,      1,      1,      1,      1,      1,      1,      1,      1.01,   1.05,   1.1,    1.01,   1.05,   1.1,    1.01,   1.01]
+maxflip     = [600,     600,    600,    600,    600,    600,    600,    600,    600,    600,    600,    600,    600,    600,    600,    600,    500,    600,    600,    500,    600,    600,    600,    600]
+initflip    = [100,     100,    100,    100,    100,    100,    100,    100,    100,    100,    100,    100,    100,    100,    100,    100,    50,     50,     50,     50,     50,     50,     100,    100]
+raiseflip   = [1.02,    1.02,   1.02,   1.02,   1.02,   1.02,   1.02,   1.02,   1.02,   1.02,   1.02,   1.02,   1.02,   1.02,   1.02,   1.02,   1.02,   1.02,   1.02,   1.02,   1.02,   1.02,   1.02,   1.02]
+switch      = [2500,    2500,   2500,   2500,   2500,   2500,   2500,   2500,   2500,   2500,   2500,   2500,   2500,   2500,   2500,   2500,   2500,   2500,   2500,   0,      0,      0,      0,      2500]
+time        = [0.35,    0.35,   0.35,   0.35,   0.35,   0.35,   0.35,   0.35,   1.1,    1.1,    1.1,    1.1,    1.1,    1.1,    1.1,    1.1,    0.35,   0.45,   0.55,   0.35,   0.45,   0.55,   0.35,   0.35]
+aspiration  = [1,       1,      1,      1,      0,      0,      0,      0,      1,      1,      1,      1,      0,      0,      0,      0,      1,      1,      1,      1,      1,      1,      1,      1]
+threshold   = [50,      50,     300,    300,    50,     50,     300,    300,    50,     50,     300,    300,    50,     50,     300,    300,    50,     50,     50,     50,     50,     50,     50,     50]
+q           = [0,       0.7,    0,      0.7,    0,      0.7,    0,      0.7,    0,      0.7,    0,      0.7,    0,      0.7,    0,      0.7,    0.7,    0.7,    0.7,    0.7,    0.7,    0.7,    0.7,    0.7]
 
-confl = [0.9, 0.01, 1, 0.5, 0.6, 0.7, 0.8]
-area = [1.01, 1, 1.01, 1.05, 1.04, 1.03, 1.02]
-maxflip = [600, 600, 600, 600, 600, 600, 600]
-initflip = [100, 100, 100, 100, 100, 100, 100]
-raiseflip = [1.02, 1.02, 1.02, 1.02, 1.02, 1.02, 1.02]
-time = [0.35, 1.2, 0.35, 0.5, 0.45, 0.4, 0.35]
 
 tmpBassename = os.path.basename(inputFile)
 
@@ -99,13 +114,10 @@ for i in range(0, numCores):
     else:
         tmpProof = proof
     reasonLSCallString = "./ReasonLS " + inputFile + " -drup-file=" + tmpProof  # add CNF file and tmp directory
-    reasonLSCallString = reasonLSCallString + " -conflRatio=" + str(confl[i % 7]) + " -areaRatio=" + str(area[i % 7])
-    reasonLSCallString = reasonLSCallString + " -maxFlipRatio=" + str(maxflip[i % 7]) + " -initFlipRatio=" + str(initflip[i % 7]) + " -raiseFlipRatio=" + str(raiseflip[i % 7])
-    reasonLSCallString = reasonLSCallString + " -timeRatio=" + str(time[i % 7]) + " -switchMode="
-    if (i < 7):
-        reasonLSCallString = reasonLSCallString + "2500"
-    else:
-        reasonLSCallString = reasonLSCallString + "0"
+    reasonLSCallString = reasonLSCallString + " -conflRatio=" + str(confl[i])     + " -areaRatio=" + str(area[i])
+    reasonLSCallString = reasonLSCallString + " -maxFlipRatio=" + str(maxflip[i]) + " -initFlipRatio=" + str(initflip[i]) + " -raiseFlipRatio=" + str(raiseflip[i])
+    reasonLSCallString = reasonLSCallString + " -timeRatio=" + str(time[i])       + " -switchMode=" +str(switch[i])
+    reasonLSCallString = reasonLSCallString + " -swt_q=" + str(q[i])              + " -swt_threshold="+ str(threshold[i]) + " -aspiration=" +str(aspiration[i])
 
     args = reasonLSCallString.split()
     # split the actual command line
@@ -162,7 +174,7 @@ if winnerCode != 0:
         if( not os.path.exists(pathz) ):
             os.mkdir(pathz)
         if( os.path.exists(tmpDir+tmpProof)):
-            os.system("mv " + tmpDir + tmpProof + " " + pathz + '/' +proof)
+            os.system("cp " + tmpDir + tmpProof + " " + pathz + '/' +proof)
     
 
 else:
@@ -170,12 +182,7 @@ else:
 
 # kill the other process, and its child processes
 for p in pids:
-    try:
-        os.kill(p, 15)
-    except OSError:
-        #do nothing
-    else:
-        #do nothing
+    kill_pid(p)
 
 # clean up the temporary files
 for i in range(numCores):