author Yanhua Yanhua Tue, 9 Mar 2010 03:27:44 +0000 (21:27 -0600) committer Yanhua Yanhua Tue, 9 Mar 2010 03:27:44 +0000 (21:27 -0600)

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);