slight modification about grain size control in satisfiability program
authorYanhua Yanhua <sun51@illinois.edu>
Tue, 9 Mar 2010 03:27:44 +0000 (21:27 -0600)
committerYanhua Yanhua <sun51@illinois.edu>
Tue, 9 Mar 2010 03:27:44 +0000 (21:27 -0600)
examples/charm++/satisfiability/Makefile
examples/charm++/satisfiability/Solver.C
examples/charm++/satisfiability/main.C

index 878840b49cde784644e5cb179efc81626c3e3315..ae22ab6761dcc08809c9dc96295b7c5c7814634d 100644 (file)
@@ -2,10 +2,10 @@
 OPTS = -g
 CHARMC = charmc $(OPTS)  
 default: all
-all: 3sat
+all: sat
 
-3sat : main.o Solver.o 
-       $(CHARMC) -lz -language charm++  -o 3sat main.o Solver.o
+sat : main.o Solver.o 
+       $(CHARMC) -lz -language charm++  -o sat main.o Solver.o
 
 main.o : main.C main.decl.h main.def.h 
        $(CHARMC) -o main.o main.C 
@@ -21,4 +21,4 @@ main.def.h main.decl.h : main.ci
 
 clean:
        rm *.o *.def.h *.decl.h
-       rm  3sat
+       rm  sat
index 5d94d8955348c9100370f81148c36152c5eacc80..9c5abec366c161e93a6172410edf3c76de5f18b3 100644 (file)
@@ -100,9 +100,9 @@ Solver::Solver(SolverState* state_msg)
     CkVec<Clause> next_clauses;
     /* Which variable get assigned  */
     Lit assigned_var = state_msg->assigned_lit;
-#ifdef DEBUG    
+//#ifdef DEBUG    
     CkPrintf("\n\nNew chare: literal = %d, occurrence size=%d, level=%d \n", toInt(assigned_var), state_msg->occurrence.size(), state_msg->level);
-#endif    
+//#endif    
     SolverState *next_state = copy_solverstate(state_msg);
     
     //Unit clauses
@@ -257,7 +257,7 @@ Solver::Solver(SolverState* state_msg)
         bool satisfiable_0 = true;
         if(unit_clauses.empty()||unit_clauses[max_index+1]>0)        
         {
-            if(next_state->clauses.size() > 2)
+            if(next_state->clauses.size() > 30)
                 CProxy_Solver::ckNew(next_state);
             else //sequential
             {
@@ -274,7 +274,7 @@ Solver::Solver(SolverState* state_msg)
         new_msg2->occurrence[max_index] = -1;
         if(unit_clauses.empty()||unit_clauses[-max_index-1]>0)
         {
-            if(new_msg2->clauses.size() > 2)
+            if(new_msg2->clauses.size() > 30)
                 CProxy_Solver::ckNew(new_msg2);
             else
             {
@@ -309,9 +309,7 @@ bool Solver::seq_solve(SolverState* state_msg)
     CkVec<Clause> next_clauses;
     /* Which variable get assigned  */
     Lit assigned_var = state_msg->assigned_lit;
-#ifdef DEBUG    
     CkPrintf("\n\nSequential SAT New chare: literal = %d, occurrence size=%d, level=%d \n", toInt(assigned_var), state_msg->occurrence.size(), state_msg->level);
-#endif    
     SolverState *next_state = copy_solverstate(state_msg);
     
     //Unit clauses
index 6cc2eece802b37d0ebcfb9508efcde1214fbdc95..f068ea2a36d528967b69e09d81191e7936bb3b91 100644 (file)
@@ -74,7 +74,7 @@ int parseInt(StreamBuffer& in) {
     if      (*in == '-') neg = true, ++in;
     else if (*in == '+') ++in;
     if (*in < '0' || *in > '9')
-        error_exit("ParseInt error\n");
+        error_exit((char*)"ParseInt error\n");
 
     while (*in >= '0' && *in <= '9')
     {
@@ -110,7 +110,7 @@ static void parse_confFile(gzFile input_stream, SolverState& S) {
         if (*in == EOF)                                            
             break;                                                 
         else if (*in == 'p'){                                      
-            if (match(in, "p cnf")){                               
+            if (match(in, (char*)"p cnf")){                               
                 int vars    = parseInt(in);                        
                 int clauses = parseInt(in);                        
                 printf("|  Number of variables:  %-12d                                         |\n", vars);
@@ -122,7 +122,7 @@ static void parse_confFile(gzFile input_stream, SolverState& S) {
                     S.occurrence[__i] = 0;
             }else{
                 printf("PARSE ERROR! Unexpected char: %c\n", *in);
-                error_exit("Parse Error\n");
+                error_exit((char*)"Parse Error\n");
             }
         } else if (*in == 'c' || *in == 'p')
             skipLine(in);
@@ -145,7 +145,7 @@ Main::Main(CkArgMsg* msg)
     SolverState* solver_msg = new SolverState;
     if(msg->argc < 2)
     {
-        error_exit("Usage: 3sat filename\n");
+        error_exit((char*)"Usage: 3sat filename\n");
     }
 
     char filename[50];
@@ -159,7 +159,7 @@ Main::Main(CkArgMsg* msg)
 
     if(in == NULL)
     {
-        error_exit("Invalid input filename\n");
+        error_exit((char*)"Invalid input filename\n");
     }
 
     parse_confFile(in, *solver_msg);