Glucose 3.0

Author: audemard

README.md

@@ -1,9 +1,13 @@
 # Glucose SAT solver
 
-This is the release 2.1 of the glucose SAT solver. 
+This is the release 3.0 of the glucose SAT solver. 
 It is based on [Minisat 2.2](http://minisat.se/MiniSat.html)
 
-For compiling:  ```./build.sh```
+For compiling:  
+ - ```cd simp```
+- ```make```
+
+
+For running: ```simp/glucose BENCHNAME```
 
 
-For running: ```glucose.sh BENCHNAME```

build.sh

@@ -27,7 +27,7 @@ OF OR IN CONNECTION WITH THE SOFTWARE OR THE USE OR OTHER DEALINGS IN THE SOFTWA
 
 //=================================================================================================
 
-namespace Minisat {
+namespace Glucose {
 
 template <class T>
 class bqueue {
@@ -54,7 +54,7 @@ class bqueue {
 			queuesize++;
 		sumofqueue += x;
 		elems[first] = x;
-		if ((++first) == maxsize) first = 0;
+		if ((++first) == maxsize) {first = 0;last = 0;}
 	}
 
 	T peek() { assert(queuesize>0); return elems[last]; }
@@ -74,7 +74,7 @@ class bqueue {
 
 	void growTo(int size) {
 		elems.growTo(size); 
-		first=0; maxsize=size; queuesize = 0;
+		first=0; maxsize=size; queuesize = 0;last = 0;
 		for(int i=0;i<size;i++) elems[i]=0; 
 	}
 

clean.sh

@@ -18,15 +18,15 @@ DAMAGES OR OTHER LIABILITY, WHETHER IN AN ACTION OF CONTRACT, TORT OR OTHERWISE,
 OF OR IN CONNECTION WITH THE SOFTWARE OR THE USE OR OTHER DEALINGS IN THE SOFTWARE.
 **************************************************************************************************/
 
-#ifndef Minisat_Dimacs_h
-#define Minisat_Dimacs_h
+#ifndef Glucose_Dimacs_h
+#define Glucose_Dimacs_h
 
 #include <stdio.h>
 
 #include "utils/ParseUtils.h"
 #include "core/SolverTypes.h"
 
-namespace Minisat {
+namespace Glucose {
 
 //=================================================================================================
 // DIMACS Parser:

sources/glucose/core/BoundedQueue.h renamed to core/BoundedQueue.h

@@ -38,7 +38,7 @@ OF OR IN CONNECTION WITH THE SOFTWARE OR THE USE OR OTHER DEALINGS IN THE SOFTWA
 #include "core/Dimacs.h"
 #include "core/Solver.h"
 
-using namespace Minisat;
+using namespace Glucose;
 
 //=================================================================================================
 
@@ -47,7 +47,7 @@ void printStats(Solver& solver)
 {
     double cpu_time = cpuTime();
     double mem_used = 0;//memUsedPeak();
-    printf("c restarts              : %"PRIu64" (%"PRIu64" conflicts in avg)\n", solver.starts,solver.conflicts/solver.starts);
+    printf("c restarts              : %"PRIu64" (%"PRIu64" conflicts in avg)\n", solver.starts,(solver.starts>0 ?solver.conflicts/solver.starts : 0));
     printf("c blocked restarts      : %"PRIu64" (multiple: %"PRIu64") \n", solver.nbstopsrestarts,solver.nbstopsrestartssame);
     printf("c last block at restart : %"PRIu64"\n",solver.lastblockatrestart);
     printf("c nb ReduceDB           : %lld\n", solver.nbReduceDB);
@@ -89,7 +89,7 @@ static void SIGINT_exit(int signum) {
 
 int main(int argc, char** argv)
 {
-  printf("c\nc This is glucose 2.1 --  based on MiniSAT (Many thanks to MiniSAT team)\nc\n");
+  printf("c\nc This is glucose 3.0 --  based on MiniSAT (Many thanks to MiniSAT team)\nc\n");
     try {
         setUsageHelp("c USAGE: %s [options] <input-file> <result-output-file>\n\n  where input may be either in plain or gzipped DIMACS.\n");
         // printf("This is MiniSat 2.0 beta\n");
@@ -102,17 +102,20 @@ int main(int argc, char** argv)
         // Extra options:
         //
         IntOption    verb   ("MAIN", "verb",   "Verbosity level (0=silent, 1=some, 2=more).", 1, IntRange(0, 2));
+        BoolOption   mod   ("MAIN", "model",   "show model.", false);
         IntOption    vv  ("MAIN", "vv",   "Verbosity every vv conflicts", 10000, IntRange(1,INT32_MAX));
         IntOption    cpu_lim("MAIN", "cpu-lim","Limit on CPU time allowed in seconds.\n", INT32_MAX, IntRange(0, INT32_MAX));
         IntOption    mem_lim("MAIN", "mem-lim","Limit on memory usage in megabytes.\n", INT32_MAX, IntRange(0, INT32_MAX));
 
+
         parseOptions(argc, argv, true);
 
         Solver S;
         double initial_time = cpuTime();
 
         S.verbosity = verb;
         S.verbEveryConflicts = vv;
+	S.showModel = mod;
         solver = &S;
         // Use signal handlers that forcibly quit until the solver will be able to respond to
         // interrupts:
@@ -153,8 +156,11 @@ int main(int argc, char** argv)
 
         parse_DIMACS(in, S);
         gzclose(in);
-        FILE* res = (argc >= 3) ? fopen(argv[2], "wb") : NULL;
 
+
+	
+        FILE* res = (argc >= 3) ? fopen(argv[argc-1], "wb") : NULL;
+
         if (S.verbosity > 0){
             printf("c |  Number of variables:  %12d                                                                   |\n", S.nVars());
             printf("c |  Number of clauses:    %12d                                                                   |\n", S.nClauses()); }
@@ -170,6 +176,7 @@ int main(int argc, char** argv)
         //signal(SIGXCPU,SIGINT_interrupt);
 
         if (!S.simplify()){
+            if (S.certifiedOutput != NULL) fprintf(S.certifiedOutput, "0\n"), fclose(S.certifiedOutput);
             if (res != NULL) fprintf(res, "UNSAT\n"), fclose(res);
             if (S.verbosity > 0){
 	        printf("c =========================================================================================================\n");
@@ -179,35 +186,40 @@ int main(int argc, char** argv)
             printf("s UNSATISFIABLE\n");
             exit(20);
         }
-        
+
         vec<Lit> dummy;
         lbool ret = S.solveLimited(dummy);
         if (S.verbosity > 0){
             printStats(S);
             printf("\n"); }
-        if (res != NULL){
-            if (ret == l_True){
-                fprintf(res, "SAT\n");
-                for (int i = 0; i < S.nVars(); i++)
-                    if (S.model[i] != l_Undef)
-                        fprintf(res, "%s%s%d", (i==0)?"":" ", (S.model[i]==l_True)?"":"-", i+1);
-                fprintf(res, " 0\n");
-            }else if (ret == l_False)
-                fprintf(res, "UNSAT\n");
-            else
-                fprintf(res, "INDET\n");
-            fclose(res);
-        } else {
-        printf(ret == l_True ? "s SATISFIABLE\n" : ret == l_False ? "s UNSATISFIABLE\n" : "s INDETERMINATE\n");
-	  if(ret==l_True) {
+
+	//-------------- Result is put in a external file
+        if (res != NULL){  
+	  if (ret == l_True){
+	    fprintf(res, "SAT\n");
+	    for (int i = 0; i < S.nVars(); i++)
+	      if (S.model[i] != l_Undef)
+		fprintf(res, "%s%s%d", (i==0)?"":" ", (S.model[i]==l_True)?"":"-", i+1);
+	    fprintf(res, " 0\n");
+	  }else if (ret == l_False)
+	    fprintf(res, "UNSAT\n");
+	  else
+	    fprintf(res, "INDET\n");
+	  fclose(res);
+	
+	//-------------- Want certified output
+        } else { 
+	  printf(ret == l_True ? "s SATISFIABLE\n" : ret == l_False ? "s UNSATISFIABLE\n" : "s INDETERMINATE\n");
+	  if(S.showModel && ret==l_True) {
 	    printf("v ");
 	    for (int i = 0; i < S.nVars(); i++)
 	      if (S.model[i] != l_Undef)
 		printf("%s%s%d", (i==0)?"":" ", (S.model[i]==l_True)?"":"-", i+1);
 	    printf(" 0\n");
 	  }
 	}
-        
+    
+    
 #ifdef NDEBUG
         exit(ret == l_True ? 10 : ret == l_False ? 20 : 0);     // (faster than "return", which will invoke the destructor for 'Solver')
 #else