diff --git a/CCAnr/CCAnr b/CCAnr/CCAnr
deleted file mode 100755
index caca9ce..0000000
Binary files a/CCAnr/CCAnr and /dev/null differ
diff --git a/CCAnr/Makefile b/CCAnr/Makefile
deleted file mode 100644
index 47f869a..0000000
--- a/CCAnr/Makefile
+++ /dev/null
@@ -1,2 +0,0 @@
-CCAnr: cca.cpp cca.h basis.h cw.h preprocessor.h
-	g++ cca.cpp -O3 -static  -o CCAnr
diff --git a/CCAnr/basis.h b/CCAnr/basis.h
deleted file mode 100644
index a4daedf..0000000
--- a/CCAnr/basis.h
+++ /dev/null
@@ -1,377 +0,0 @@
-#ifndef _BASIS_H_
-#define _BASIS_H_
-
-#include <iostream>
-#include <fstream>
-#include <cstdlib>
-#include <cmath>
-
-using namespace std;
-
-enum type{SAT3, SAT5, SAT7, strSAT} probtype;
-
-/* limits on the size of the problem. */
-#define MAX_VARS    4000010
-#define MAX_CLAUSES 20000000
-
-
-// Define a data structure for a literal in the SAT problem.
-struct lit {
-    int clause_num;		//clause num, begin with 0
-    int var_num;		//variable num, begin with 1
-    int sense;			//is 1 for true literals, 0 for false literals.
-};
-
-/*parameters of the instance*/
-int     num_vars;		//var index from 1 to num_vars
-int     num_clauses;	//clause index from 0 to num_clauses-1
-int		max_clause_len;
-int		min_clause_len;
-int		formula_len=0;
-double	avg_clause_len;
-double	ratio;
-
-/* literal arrays */				
-lit*	var_lit[MAX_VARS];				//var_lit[i][j] means the j'th literal of var i.
-int		var_lit_count[MAX_VARS];        //amount of literals of each var
-lit*	clause_lit[MAX_CLAUSES];		//clause_lit[i][j] means the j'th literal of clause i.
-int		clause_lit_count[MAX_CLAUSES]; 	// amount of literals in each clause		
-
-lit*	org_clause_lit[MAX_CLAUSES];		//clause_lit[i][j] means the j'th literal of clause i.
-int		org_clause_lit_count[MAX_CLAUSES]; 	// amount of literals in each clause
-int		simplify=0;
-			
-/* Information about the variables. */
-int     score[MAX_VARS];				
-int		time_stamp[MAX_VARS];
-int		conf_change[MAX_VARS];
-int*	var_neighbor[MAX_VARS];
-int		var_neighbor_count[MAX_VARS];
-//int		pscore[MAX_VARS];
-int		fix[MAX_VARS];
-
-/* Information about the clauses */			
-int     clause_weight[MAX_CLAUSES];		
-int     sat_count[MAX_CLAUSES];			
-int		sat_var[MAX_CLAUSES];
-//int		sat_var2[MAX_CLAUSES];
-
-//unsat clauses stack
-int		unsat_stack[MAX_CLAUSES];		//store the unsat clause number
-int		unsat_stack_fill_pointer;
-int		index_in_unsat_stack[MAX_CLAUSES];//which position is a clause in the unsat_stack
-
-int		this_try_best_unsat_stack_fill_pointer;
-
-//variables in unsat clauses
-int		unsatvar_stack[MAX_VARS];		
-int		unsatvar_stack_fill_pointer;
-int		index_in_unsatvar_stack[MAX_VARS];
-int		unsat_app_count[MAX_VARS];		//a varible appears in how many unsat clauses
-
-//configuration changed decreasing variables (score>0 and confchange=1)
-int		goodvar_stack[MAX_VARS];		
-int		goodvar_stack_fill_pointer;
-int		already_in_goodvar_stack[MAX_VARS];
-
-//unit clauses preprocess
-lit		unitclause_queue[MAX_VARS];		
-int		unitclause_queue_beg_pointer=0;
-int     unitclause_queue_end_pointer=0;
-int     clause_delete[MAX_CLAUSES];
-
-/* Information about solution */
-int             cur_soln[MAX_VARS];	//the current solution, with 1's for True variables, and 0's for False variables
-
-//cutoff
-int		max_tries = 10000;
-int		tries;
-int		max_flips = 2000000000;
-int		step;
-
-void setup_datastructure();
-void free_memory();
-int build_instance(char *filename);
-void build_neighbor_relation();
-
-void free_memory()
-{
-	int i;
-	for (i = 0; i < num_clauses; i++) 
-	{
-		delete[] clause_lit[i];
-	}
-	
-	for(i=1; i<=num_vars; ++i)
-	{
-		delete[] var_lit[i];
-		delete[] var_neighbor[i];
-	}
-}
-
-/*
- * Read in the problem.
- */
-int temp_lit[MAX_VARS]; //the max length of a clause can be MAX_VARS
-int build_instance(char *filename)
-{
-	char    line[1000000];
-	char    tempstr1[10];
-	char    tempstr2[10];
-	int     cur_lit;
-	int     i,j;
-	int		v,c;//var, clause
-	
-	ifstream infile(filename);
-	if(!infile.is_open())
-		return 0;
-
-	/*** build problem data structures of the instance ***/
-	infile.getline(line,1000000);
-	while (line[0] != 'p')
-		infile.getline(line,1000000);
-
-	sscanf(line, "%s %s %d %d", tempstr1, tempstr2, &num_vars, &num_clauses);
-	::ratio = double(num_clauses) / num_vars;
-	
-	if(num_vars>=MAX_VARS || num_clauses>=MAX_CLAUSES)
-	{
-		cout<<"the size of instance exceeds out limitation, please enlarge MAX_VARS and (or) MAX_CLAUSES."<<endl;
-		exit(-1);
-	}
-	
-	for (c = 0; c < num_clauses; c++) 
-	{
-		clause_lit_count[c] = 0;
-		clause_delete[c] = 0;
-	}
-	for (v=1; v<=num_vars; ++v)
-	{
-		var_lit_count[v] = 0;
-		fix[v] = 0;
-	}
-		
-	max_clause_len = 0;
-	min_clause_len = num_vars;
-		
-	//Now, read the clauses, one at a time.
-	for (c = 0; c < num_clauses; c++) 
-	{
-		infile>>cur_lit;
-
-		while (cur_lit != 0) { 
-			temp_lit[clause_lit_count[c]] = cur_lit;
-			clause_lit_count[c]++;
-		
-			infile>>cur_lit;
-		}
-		
-		clause_lit[c] = new lit[clause_lit_count[c]+1];
-		
-		for(i=0; i<clause_lit_count[c]; ++i)
-		{
-			clause_lit[c][i].clause_num = c;
-			clause_lit[c][i].var_num = abs(temp_lit[i]);
-			if (temp_lit[i] > 0) clause_lit[c][i].sense = 1;
-				else clause_lit[c][i].sense = 0;
-			
-			var_lit_count[clause_lit[c][i].var_num]++;
-		}
-		clause_lit[c][i].var_num=0; 
-		clause_lit[c][i].clause_num = -1;
-        
-        //unit clause
-        if(clause_lit_count[c]==1)
-        {
-            unitclause_queue[unitclause_queue_end_pointer++] = clause_lit[c][0];
-            clause_delete[c]=1;
-        }
-		
-		if(clause_lit_count[c] > max_clause_len)
-			max_clause_len = clause_lit_count[c];
-		else if(clause_lit_count[c] < min_clause_len)
-			min_clause_len = clause_lit_count[c];
-			
-		formula_len += clause_lit_count[c];
-	}
-	infile.close();
-	
-	avg_clause_len = (double)formula_len/num_clauses;
-	
-	if(unitclause_queue_end_pointer>0)
-	{
-		simplify = 1;
-		for (c = 0; c < num_clauses; c++) 
-		{
-			org_clause_lit_count[c] = clause_lit_count[c];
-			org_clause_lit[c] = new lit[clause_lit_count[c]+1];
-			for(i=0; i<org_clause_lit_count[c]; ++i)
-			{
-				org_clause_lit[c][i] = clause_lit[c][i];
-			}
-			
-		}
-	}
-
-	
-	//creat var literal arrays
-	for (v=1; v<=num_vars; ++v)
-	{
-		var_lit[v] = new lit[var_lit_count[v]+1];
-		var_lit_count[v] = 0;	//reset to 0, for build up the array
-	}
-	//scan all clauses to build up var literal arrays
-	for (c = 0; c < num_clauses; ++c) 
-	{
-		for(i=0; i<clause_lit_count[c]; ++i)
-		{
-			v = clause_lit[c][i].var_num;
-			var_lit[v][var_lit_count[v]] = clause_lit[c][i];
-			++var_lit_count[v];
-		}
-	}
-	for (v=1; v<=num_vars; ++v) //set boundary
-		var_lit[v][var_lit_count[v]].clause_num=-1;
-	
-	return 1;
-}
-
-
-void build_neighbor_relation()
-{
-	int*	neighbor_flag = new int[num_vars+1];
-	int		i,j,count;
-	int 	v,c;
-
-	for(v=1; v<=num_vars; ++v)
-	{
-		var_neighbor_count[v] = 0;
-		
-		if(fix[v]==1) continue;
-
-		for(i=1; i<=num_vars; ++i)
-			neighbor_flag[i] = 0;
-		neighbor_flag[v] = 1;
-		
-		for(i=0; i<var_lit_count[v]; ++i)
-		{
-			c = var_lit[v][i].clause_num;
-			if(clause_delete[c]==1) continue;
-			
-			for(j=0; j<clause_lit_count[c]; ++j)
-			{
-				if(neighbor_flag[clause_lit[c][j].var_num]==0)
-				{
-					var_neighbor_count[v]++;
-					neighbor_flag[clause_lit[c][j].var_num] = 1;
-				}
-			}
-		}
-
-		neighbor_flag[v] = 0;
- 
-		var_neighbor[v] = new int[var_neighbor_count[v]+1];
-
-		count = 0;
-		for(i=1; i<=num_vars; ++i)
-		{
-			if(fix[i]==1) continue;
-			
-			if(neighbor_flag[i]==1)
-			{
-				var_neighbor[v][count] = i;
-				count++;
-			}
-		}
-		var_neighbor[v][count]=0;
-	}
-	
-	delete[] neighbor_flag; neighbor_flag=NULL;
-}
-
-
-void print_solution()
-{
-     int    i;
-
-     cout<<"v ";
-     for (i=1; i<=num_vars; i++) {
-         if(cur_soln[i]==0) cout<<"-";
-         cout<<i;
-         if(i%10==0) cout<<endl<<"v ";
-         else	cout<<' ';
-     }
-     cout<<"0"<<endl;
-}
-
-
-int verify_sol()
-{
-	int c,j; 
-	int flag;
-	
-	if(simplify==0)
-	{
-	
-		for (c = 0; c<num_clauses; ++c) 
-		{
-			flag = 0;
-			for(j=0; j<clause_lit_count[c]; ++j)
-				if (cur_soln[clause_lit[c][j].var_num] == clause_lit[c][j].sense) {flag = 1; break;}
-
-			if(flag ==0){//output the clause unsatisfied by the solution
-				cout<<"c clause "<<c<<" is not satisfied"<<endl;
-			
-				cout<<"c ";
-				for(j=0; j<clause_lit_count[c]; ++j)
-				{
-					if(clause_lit[c][j].sense==0)cout<<"-";
-					cout<<clause_lit[c][j].var_num<<" ";
-				}
-				cout<<endl;
-			
-				for(j=0; j<clause_lit_count[c]; ++j)
-					cout<<cur_soln[clause_lit[c][j].var_num]<<" ";
-				cout<<endl;
-
-				return 0;
-			}
-		}
-	}
-	
-	if(simplify==1)
-	{
-		for (c = 0; c<num_clauses; ++c) 
-		{
-			flag = 0;
-			for(j=0; j<org_clause_lit_count[c]; ++j)
-				if (cur_soln[org_clause_lit[c][j].var_num] == org_clause_lit[c][j].sense) {flag = 1; break;}
-
-			if(flag ==0){//output the clause unsatisfied by the solution
-				cout<<"c clause "<<c<<" is not satisfied"<<endl;
-				
-				if(clause_delete[c]==1)cout<<"c this clause is deleted by UP."<<endl;
-			
-				cout<<"c ";
-				for(j=0; j<org_clause_lit_count[c]; ++j)
-				{
-					if(org_clause_lit[c][j].sense==0)cout<<"-";
-					cout<<org_clause_lit[c][j].var_num<<" ";
-				}
-				cout<<endl;
-			
-				for(j=0; j<org_clause_lit_count[c]; ++j)
-					cout<<cur_soln[org_clause_lit[c][j].var_num]<<" ";
-				cout<<endl;
-
-				return 0;
-			}
-		}
-		
-	}
-	
-	return 1;
-}
-
-#endif
-
diff --git a/CCAnr/cca.cpp b/CCAnr/cca.cpp
deleted file mode 100644
index a865fa0..0000000
--- a/CCAnr/cca.cpp
+++ /dev/null
@@ -1,292 +0,0 @@
-#include "basis.h"
-#include "cca.h"
-#include "cw.h"
-#include "preprocessor.h"
-
-#include <string.h>
-#include <sys/times.h> //these two h files are for linux
-#include <unistd.h>
-
-#include "ccanr.h"
-
-char * inst;
-int seed;
-
-long long ls_no_improv_times;
-
-bool aspiration_active;
-
-static int pick_var(void)
-{
-	int         i,k,c,v;
-	int         best_var;
-	lit*		clause_c;
-
-	/**Greedy Mode**/
-	/*CCD (configuration changed decreasing) mode, the level with configuation chekcing*/
-	if(goodvar_stack_fill_pointer>0)
-	{
-
-		//if(goodvar_stack_fill_pointer<balancePar)
-		//{
-			best_var = goodvar_stack[0];
-			for(i=1; i<goodvar_stack_fill_pointer; ++i)
-			{
-				v=goodvar_stack[i];
-				if(score[v]>score[best_var]) best_var = v;
-				else if(score[v]==score[best_var])
-				{
-					//if(unsat_app_count[v]>unsat_app_count[best_var]) best_var = v;
-					//else if(unsat_app_count[v]==unsat_app_count[best_var]&&time_stamp[v]<time_stamp[best_var]) best_var = v;
-					
-					if(time_stamp[v]<time_stamp[best_var]) best_var = v;
-				}
-			}
-			return best_var;
-		//}
-		/*else
-		{
-			best_var = goodvar_stack[rand()%goodvar_stack_fill_pointer];
-			for(int j=1;j<balancePar;++j)
-			{
-				v = goodvar_stack[rand()%goodvar_stack_fill_pointer];
-				if(score[v]>score[best_var]) best_var = v;
-				else if(score[v]==score[best_var])
-				{
-					//if(unsat_app_count[v]>unsat_app_count[best_var]) best_var = v;
-					//else if(unsat_app_count[v]==unsat_app_count[best_var]&&time_stamp[v]<time_stamp[best_var]) best_var = v;
-					if(time_stamp[v]<time_stamp[best_var]) best_var = v;
-				}
-			}
-			return best_var;
-		}*/
-	}
-	
-	
-	/*aspiration*/
-	if (aspiration_active)
-	{
-		best_var = 0;
-		for(i=0; i<unsatvar_stack_fill_pointer; ++i)
-		{
-			if(score[unsatvar_stack[i]]>ave_weight) 
-			{
-				best_var = unsatvar_stack[i];
-				break;
-			}
-		}
-
-		for(++i; i<unsatvar_stack_fill_pointer; ++i)
-		{
-			v=unsatvar_stack[i];
-			if(score[v]>score[best_var]) best_var = v;
-			else if(score[v]==score[best_var] && time_stamp[v]<time_stamp[best_var]) best_var = v;
-		}
-		
-		if(best_var!=0) return best_var;
-	}
-	/*****end aspiration*******************/
-
-	update_clause_weights();
-
-	/*focused random walk*/
-
-	c = unsat_stack[rand()%unsat_stack_fill_pointer];
-	clause_c = clause_lit[c];
-	best_var = clause_c[0].var_num;
-	for(k=1; k<clause_lit_count[c]; ++k)
-	{
-		v=clause_c[k].var_num;
-		
-		//using score
-		//if(score[v]>score[best_var]) best_var = v;
-		//else if(score[v]==score[best_var]&&time_stamp[v]<time_stamp[best_var]) best_var = v;
-		
-		//using unweighted make
-		if(unsat_app_count[v]>unsat_app_count[best_var]) best_var = v;
-		//else if(unsat_app_count[v]==unsat_app_count[best_var] && time_stamp[v]<time_stamp[best_var]) best_var = v;
-		else if(unsat_app_count[v]==unsat_app_count[best_var])
-		{
-			if(score[v]>score[best_var]) best_var = v;
-			else if(score[v]==score[best_var]&&time_stamp[v]<time_stamp[best_var]) best_var = v;
-		}
-	}
-
-	return best_var;
-}
-
-
-
-
-//set functions in the algorithm
-void settings()
-{
-	//set_clause_weighting();
-	
-	//aspiration_active = false; //
-}
-
-/*
-void local_search(int max_flips)
-{
-	int flipvar;
-     
-	for (step = 0; step<max_flips; step++)
-	{
-		//find a solution
-		if(unsat_stack_fill_pointer==0) return;
-
-		flipvar = pick_var();
-
-		flip(flipvar);
-
-		time_stamp[flipvar] = step;
-	}
-}
-*/
-
-void local_search(long long no_improv_times)
-{
-	int flipvar;
-	long long notime = 1 + no_improv_times;
-
-	// printf("cur_sol: ");
-	// for(int i=1; i<=num_vars; i++) {
-	// 	printf("%d ", cur_soln[i]);
-	// }
-	// printf("\n");
-	
-	while(--notime)
-	{
-		flipvar = pick_var();
-		flip(flipvar);
-		time_stamp[flipvar] = step;
-
-
-		step++;
-		if(unsat_stack_fill_pointer < this_try_best_unsat_stack_fill_pointer)
-		{
-			this_try_best_unsat_stack_fill_pointer = unsat_stack_fill_pointer;
-			notime = 1 + no_improv_times;
-		}
-		
-		if(unsat_stack_fill_pointer == 0)
-		{
-			return;
-		}
-	}
-     
-	return;
-}
-
-void default_settings()
-{
-	seed = 1;
-	ls_no_improv_times = 200000;
-	p_scale = 0.3;
-	q_scale = 0.7;
-	threshold = 50;
-	
-	aspiration_active = false; //
-}
-
-int CCAnr::module_pick_var() {
-	return pick_var();
-}
-void CCAnr::module_flip_var(int flipvar) {
-	flip(flipvar);
-	time_stamp[flipvar] = step;
-	step++;
-	if(unsat_stack_fill_pointer < this_try_best_unsat_stack_fill_pointer)
-	{
-		this_try_best_unsat_stack_fill_pointer = unsat_stack_fill_pointer;
-	}
-		
-	if(unsat_stack_fill_pointer == 0)
-	{
-		printf("[CCAnr] find solution!\n");
-
-		if(verify_sol()!=1) {
-	 	    cout<<"c Sorry, something is wrong."<<endl;
-			exit(-1);
-		}
-	}
-}
-
-int* CCAnr::module_cur_soln() {
-	return cur_soln;
-}
-
-void CCAnr::module_reset() {
-	settings();
-	init();
-}
-
-void CCAnr::module_init()
-{
-	int     seed,i;
-	int		satisfy_flag=0;
-	struct 	tms start, stop;
-    
-    cout<<"c This is CCAnr 2.0 [Version: 2018.01.28] [Author: Shaowei Cai]."<<endl;	
-	
-	times(&start);
-
-	default_settings();
-
-	build_instance("test.cnf");
-    
-    srand(seed);
-    
-    //if(unitclause_queue_end_pointer > 0) preprocess();
-    
-    build_neighbor_relation();
-    
-    scale_ave=(threshold+1)*q_scale; //
-    
-	cout<<"c Instance: Number of variables = "<<num_vars<<endl;
-	cout<<"c Instance: Number of clauses = "<<num_clauses<<endl;
-	cout<<"c Instance: Ratio = "<<::ratio<<endl;
-	cout<<"c Instance: Formula length = "<<formula_len<<endl;
-	cout<<"c Instance: Avg (Min,Max) clause length = "<<avg_clause_len<<" ("<<min_clause_len<<","<<max_clause_len<<")"<<endl;
-	cout<<"c Algorithmic: Random seed = "<<seed<<endl;
-	cout<<"c Algorithmic: ls_no_improv_steps = " << ls_no_improv_times << endl;
-	cout<<"c Algorithmic: swt_p = " << p_scale << endl;
-	cout<<"c Algorithmic: swt_q = " << q_scale << endl;
-	cout<<"c Algorithmic: swt_threshold = " << threshold << endl;
-	cout<<"c Algorithmic: scale_ave = " << scale_ave << endl;
-	if(aspiration_active) cout<<"c Algorithmic: aspiration_active = true" << endl;
-	else cout<<"c Algorithmic: aspiration_active = false" << endl;
-    
-	// for (tries = 0; tries <= max_tries; tries++) 
-	// {
-	// 	 settings();
-		 
-	// 	 init();
-	 
-	// 	 local_search(ls_no_improv_times);
-
-	// 	 if (unsat_stack_fill_pointer==0) 
-	// 	 {
-	// 	 	if(verify_sol()==1) {satisfy_flag = 1; break;}
-	// 	    else cout<<"c Sorry, something is wrong."<<endl;/////
-	// 	 }
-	// }
-
-	// times(&stop);
-	// double comp_time = double(stop.tms_utime - start.tms_utime +stop.tms_stime - start.tms_stime) / sysconf(_SC_CLK_TCK);
-
-    // if(satisfy_flag==1)
-    // {
-    // 	cout<<"s SATISFIABLE"<<endl;
-	// 	//print_solution();
-    // }
-    // else  cout<<"s UNKNOWN"<<endl;
-    
-    // cout<<"c solveSteps = "<<tries<<" tries + "<<step<<" steps (each try has "<<max_flips<<" steps)."<<endl;
-    // cout<<"c solveTime = "<<comp_time<<endl;
-	 
-    // free_memory();
-
-    return;
-}
diff --git a/CCAnr/cca.h b/CCAnr/cca.h
deleted file mode 100644
index 6ed4dd8..0000000
--- a/CCAnr/cca.h
+++ /dev/null
@@ -1,295 +0,0 @@
-/************************************=== CCAnr ===***************************************          
- ** CCAnr is a local search solver for the Boolean Satisfiability (SAT) problem,
- ** which is especially designed for non-random instances.
- ** CCAnr is designed and implemented by Shaowei Cai (email: shaoweicai.cs@gmail.com),                                        
- *****************************************************************************************/
-
-/*****************************=== Develpment history ===*************************************
-** 2011.5
-** SWCC (Smoothed Weighting and Configuration Checking) by Shaowei Cai
-** New Idea: Configuration Checking (CC)
-** A variable is configuration changed, if since its last flip, at least one of its 
-** neighboring var has been flipped. 
-** In the greedy mode, Swcc picks the best Configuration Changed Decreasing  var to flip.
-** In the random mode, it updates weights, and flips the oldest var in a random unsat clause.
- 
-** 2011.9 
-** SWCCA (Smoothed Weighting and Configuration Checking with Aspiration) by Shaowei Cai                 
-** New Idea: CC with Aspiration (CCA)
-** Modification: in greedy mode, it first prefers to flip the best CCD var. If there is 
-** no CCD variable, then flip the best significant decreasing var, i.e., with a great 
-** positive score (in Swcca, bigger than averaged clause weight), if there exsit such vars.                  
- 
-** 2013.4	
-** CCAnr (CCA for non-random SAT)
-** Modifications: Generalize the smoothig fomula as w(ci)=w(ci)*p+ave_w*q; pick the greediest
-** variable in the diversification mode.
-************************************************************************************************/
-
-
-#ifndef _CCA_H_
-#define _CCA_H_
-
-#include "basis.h"
-
-#define pop(stack) stack[--stack ## _fill_pointer]
-#define push(item, stack) stack[stack ## _fill_pointer++] = item
-
-inline void unsat(int clause)
-{
-	index_in_unsat_stack[clause] = unsat_stack_fill_pointer;
-	push(clause,unsat_stack);
-	
-	//update appreance count of each var in unsat clause and update stack of vars in unsat clauses
-	int v;
-	for(lit* p=clause_lit[clause]; (v=p->var_num)!=0; p++)
-	{	
-		unsat_app_count[v]++;
-		if(unsat_app_count[v]==1)
-		{
-			index_in_unsatvar_stack[v] = unsatvar_stack_fill_pointer;
-			push(v,unsatvar_stack);	
-		}
-	}
-}
-
-
-inline void sat(int clause)
-{
-	int index,last_unsat_clause;
-
-	//since the clause is satisfied, its position can be reused to store the last_unsat_clause
-	last_unsat_clause = pop(unsat_stack);
-	index = index_in_unsat_stack[clause];
-	unsat_stack[index] = last_unsat_clause;
-	index_in_unsat_stack[last_unsat_clause] = index;
-	
-	//update appreance count of each var in unsat clause and update stack of vars in unsat clauses
-	int v,last_unsat_var;
-	for(lit* p=clause_lit[clause]; (v=p->var_num)!=0; p++)
-	{	
-		unsat_app_count[v]--;
-		if(unsat_app_count[v]==0)
-		{
-			last_unsat_var = pop(unsatvar_stack);
-			index = index_in_unsatvar_stack[v];
-			unsatvar_stack[index] = last_unsat_var;
-			index_in_unsatvar_stack[last_unsat_var] = index;
-		}
-	}
-}
-
-//initiation of the algorithm
-void init()
-{
-	int 		v,c;
-	int			i,j;
-	int			clause;
-	
-	//Initialize edge weights
-	for (c = 0; c<num_clauses; c++)
-		clause_weight[c] = 1;
-
-	//init unsat_stack
-	unsat_stack_fill_pointer = 0;
-	unsatvar_stack_fill_pointer = 0;
-
-	//init solution
-	for (v = 1; v <= num_vars; v++) {
-        
-        if(fix[v]==0){
-            if(rand()%2==1) cur_soln[v] = 1;
-            else cur_soln[v] = 0;
-
-			time_stamp[v] = 0;
-			conf_change[v] = 1;
-			unsat_app_count[v] = 0;
-		
-			//pscore[v] = 0;
-		}
-	}
-
-	/* figure out sat_count, and init unsat_stack */
-	for (c=0; c<num_clauses; ++c) 
-	{
-		if(clause_delete[c]==1) continue;
-		
-		sat_count[c] = 0;
-		
-		for(j=0; j<clause_lit_count[c]; ++j)
-		{
-			if (cur_soln[clause_lit[c][j].var_num] == clause_lit[c][j].sense)
-			{
-				sat_count[c]++;
-				sat_var[c] = clause_lit[c][j].var_num;	
-			}
-		}
-
-		if (sat_count[c] == 0) 
-			unsat(c);
-	}
-
-	/*figure out var score*/
-	int lit_count;
-	for (v=1; v<=num_vars; v++) 
-	{
-		if(fix[v]==1) 
-		{
-			score[v] = -100000;
-			continue;
-		}
-		
-		score[v] = 0;
-
-		lit_count = var_lit_count[v];
-		
-		for(i=0; i<lit_count; ++i)
-		{
-			c = var_lit[v][i].clause_num;
-			if (sat_count[c]==0) score[v]++;
-			else if (sat_count[c]==1 && var_lit[v][i].sense==cur_soln[v]) score[v]--;
-		}
-	}
-	
-	/*
-	int flag;
-	//compute pscore and record sat_var and sat_var2 for 2sat clauses
-	for (c=0; c<num_clauses; ++c) 
-	{
-		if(clause_delete[c]==1) continue;
-		
-		if (sat_count[c]==1)
-		{
-			for(j=0;j<clause_lit_count[c];++j)
-			{
-				v=clause_lit[c][j].var_num;
-				if(v!=sat_var[c])pscore[v]++;
-			}
-		}
-		else if(sat_count[c]==2)
-		{
-			flag=0;
-			for(j=0;j<clause_lit_count[c];++j)
-			{
-				v=clause_lit[c][j].var_num;
-				if(clause_lit[c][j].sense == cur_soln[v])
-				{
-					pscore[v]--;
-					if(flag==0){sat_var[c] = v; flag=1;}
-					else	{sat_var2[c] = v; break;}
-				}
-			}
-		
-		}
-	}
-	*/
-	
-		
-	//init goodvars stack
-	goodvar_stack_fill_pointer = 0;
-	for (v=1; v<=num_vars; v++) 
-	{
-		if(fix[v]==1)  continue;
-		if(score[v]>0)// && conf_change[v]==1)
-		{
-			already_in_goodvar_stack[v] = 1;
-			push(v,goodvar_stack);
-			
-		}
-		else already_in_goodvar_stack[v] = 0;
-	}
-	
-	//setting for the virtual var 0
-	time_stamp[0]=0;
-	//pscore[0]=0;
-	
-	this_try_best_unsat_stack_fill_pointer = unsat_stack_fill_pointer;
-}
-
-
-void flip(int flipvar)
-{
-	cur_soln[flipvar] = 1 - cur_soln[flipvar];
-	
-	int i,j;
-	int v,c;
-
-	lit* clause_c;
-	
-	int org_flipvar_score = score[flipvar];
-	
-	//update related clauses and neighbor vars
-	for(lit *q = var_lit[flipvar]; (c=q->clause_num)>=0; q++)
-	{
-		clause_c = clause_lit[c];
-		if(cur_soln[flipvar] == q->sense)
-		{
-			++sat_count[c];
-			
-			if (sat_count[c] == 2) //sat_count from 1 to 2
-				score[sat_var[c]] += clause_weight[c];
-			else if (sat_count[c] == 1) // sat_count from 0 to 1
-			{
-				sat_var[c] = flipvar;//record the only true lit's var
-				for(lit* p=clause_c; (v=p->var_num)!=0; p++) score[v] -= clause_weight[c];
-                
-				sat(c);
-			}
-		}
-		else // cur_soln[flipvar] != cur_lit.sense
-		{
-			--sat_count[c];
-			if (sat_count[c] == 1) //sat_count from 2 to 1
-			{
-				for(lit* p=clause_c; (v=p->var_num)!=0; p++) 
-				{
-					if(p->sense == cur_soln[v] )
-					{
-						score[v] -= clause_weight[c];
-						sat_var[c] = v;
-						break;
-					}
-				}
-			}
-			else if (sat_count[c] == 0) //sat_count from 1 to 0
-			{
-				for(lit* p=clause_c; (v=p->var_num)!=0; p++) score[v] += clause_weight[c];
-				unsat(c);
-			}//end else if
-			
-		}//end else
-	}
-
-	score[flipvar] = -org_flipvar_score;
-	
-	/*update CCD */
-	int index;
-	
-	conf_change[flipvar] = 0;
-	//remove the vars no longer goodvar in goodvar stack 
-	for(index=goodvar_stack_fill_pointer-1; index>=0; index--)
-	{
-		v = goodvar_stack[index];
-		if(score[v]<=0)
-		{
-			goodvar_stack[index] = pop(goodvar_stack);
-			already_in_goodvar_stack[v] = 0;
-		}	
-	}
-
-	//update all flipvar's neighbor's conf_change to be 1, add goodvar
-	int* p;
-	for(p=var_neighbor[flipvar]; (v=*p)!=0; p++)
-	{
-		conf_change[v] = 1;
-		
-		if(score[v]>0 && already_in_goodvar_stack[v] ==0)
-		{
-			push(v,goodvar_stack);
-			already_in_goodvar_stack[v] = 1;
-		}
-	}
-}
-
-#endif
-
diff --git a/CCAnr/ccanr.h b/CCAnr/ccanr.h
deleted file mode 100644
index d343031..0000000
--- a/CCAnr/ccanr.h
+++ /dev/null
@@ -1,9 +0,0 @@
-namespace CCAnr {
-
-void module_init();
-int module_pick_var();
-void module_flip_var(int var);
-void module_reset();
-
-int* module_cur_soln();
-}
\ No newline at end of file
diff --git a/CCAnr/cw.h b/CCAnr/cw.h
deleted file mode 100644
index c3a252d..0000000
--- a/CCAnr/cw.h
+++ /dev/null
@@ -1,103 +0,0 @@
-#ifndef _CW_H_
-#define _CW_H_
-
-#include "basis.h"
-
-#define sigscore	ave_weight   //significant score needed for aspiration
-
-int		ave_weight=1;
-int		delta_total_weight=0;
-
-/**************************************** clause weighting for 3sat **************************************************/
-
-int		threshold;
-float	p_scale;//w=w*p+ave_w*q
-float	q_scale=0;
-int		scale_ave;//scale_ave==ave_weight*q_scale
-
-int 	q_init=0;
-
-void smooth_clause_weights()
-{
-	int i,j,c,v;
-	int new_total_weight=0;
-
-	for (v=1; v<=num_vars; ++v) 
-		score[v] = 0;
-	
-	//smooth clause score and update score of variables
-	for (c = 0; c<num_clauses; ++c)
-	{
-		clause_weight[c] = clause_weight[c]*p_scale+scale_ave;
-		if(clause_weight[c]<1) clause_weight[c] = 1;
-		
-		new_total_weight+=clause_weight[c];
-		
-		//update score of variables in this clause 
-		if (sat_count[c]==0) 
-		{
-			for(j=0; j<clause_lit_count[c]; ++j)
-			{
-				score[clause_lit[c][j].var_num] += clause_weight[c];
-			}
-		}
-		else  if(sat_count[c]==1)
-			score[sat_var[c]]-=clause_weight[c];
-	}
-	
-	ave_weight=new_total_weight/num_clauses;
-}
-
-void update_clause_weights()
-{
-	int i,v;
-
-	for(i=0; i < unsat_stack_fill_pointer; ++i)
-		clause_weight[unsat_stack[i]]++;
-	
-	for(i=0; i<unsatvar_stack_fill_pointer; ++i)
-	{
-		v = unsatvar_stack[i];
-		score[v] += unsat_app_count[v];
-		if(score[v]>0 &&  conf_change[v]==1 && already_in_goodvar_stack[v] ==0)
-		{
-			push(v,goodvar_stack);
-			already_in_goodvar_stack[v] =1;
-		}
-	}
-	
-	delta_total_weight+=unsat_stack_fill_pointer;
-	if(delta_total_weight>=num_clauses)
-	{
-		ave_weight+=1;
-		delta_total_weight -= num_clauses;
-		
-		//smooth weights
-		if(ave_weight>threshold)
-			smooth_clause_weights();
-	}
-}
-
-
-void set_clause_weighting()
-{	
-	threshold=300;
-	p_scale=0.3;
-	if(q_init==0)
-	{
-		if(::ratio<=15) q_scale=0;
-		else q_scale=0.7;
-	}
-	else 
-	{
-		if(q_scale<0.5)  //0
-			q_scale = 0.7;
-		else
-			q_scale = 0;
-	}
-	
-	scale_ave=(threshold+1)*q_scale;
-	q_init = 1;
-}
-
-#endif
diff --git a/CCAnr/preprocessor.h b/CCAnr/preprocessor.h
deleted file mode 100644
index 894353c..0000000
--- a/CCAnr/preprocessor.h
+++ /dev/null
@@ -1,133 +0,0 @@
-#include "basis.h"
-//preprocess
-void unit_propagation()
-{
-    lit uc_lit;
-    int uc_clause;
-    int uc_var;
-    bool uc_sense;
-    
-    int c,v;
-    int i,j;
-    lit cur, cur_c;
-    
-    
-    //while (unitclause_queue_beg_pointer < unitclause_queue_end_pointer) 
-    for(unitclause_queue_beg_pointer=0; unitclause_queue_beg_pointer < unitclause_queue_end_pointer; unitclause_queue_beg_pointer++)
-    {
-        uc_lit = unitclause_queue[unitclause_queue_beg_pointer];
-        
-        uc_var = uc_lit.var_num;
-        uc_sense = uc_lit.sense;
-        
-        if(fix[uc_var]==1) {if(uc_sense!=cur_soln[uc_var])cout<<"c wants to fix a variable twice, forbid."<<endl; continue;}
-     
-        cur_soln[uc_var] = uc_sense;//fix the variable in unit clause
-        fix[uc_var] = 1;
-        
-        for(i = 0; i<var_lit_count[uc_var]; ++i)
-        {
-            cur = var_lit[uc_var][i];
-            c = cur.clause_num;
-            
-            if(clause_delete[c]==1) continue;
-            
-            if(cur.sense == uc_sense)//then remove the clause from var's var_lit[] array
-            {
-                clause_delete[c]=1;
-            }
-            else
-            {
-                if(clause_lit_count[c]==2)
-                {
-                    if(clause_lit[c][0].var_num == uc_var)
-                    {
-                        unitclause_queue[unitclause_queue_end_pointer++] = clause_lit[c][1];
-                    }
-                    else
-                    {
-                        unitclause_queue[unitclause_queue_end_pointer++] = clause_lit[c][0];
-                    }
-                    
-                    clause_delete[c]=1;
-                }
-                else
-                {
-                    for(j=0; j<clause_lit_count[c]; ++j)
-                    {
-                        if(clause_lit[c][j].var_num == uc_var)
-                        {
-                            clause_lit[c][j]=clause_lit[c][clause_lit_count[c]-1];
-    
-                            clause_lit_count[c]--;
-                            
-                            break;
-                        }
-                    }//for
-                }
-            }
-            
-        }//for 
-        
-        
-        
-    }//begpointer to endpointer for
-    
-}
-
-
-void preprocess()
-{
-    int c,v,i;
-    int delete_clause_count=0;
-    int fix_var_count=0;
-    
-    unit_propagation();
-    
-    //rescan all clauses to build up var literal arrays
-    for (v=1; v<=num_vars; ++v) 
-        var_lit_count[v] = 0;
-    
-    max_clause_len = 0;
-	min_clause_len = num_vars;
-    int    formula_len=0;
-    
-    for (c = 0; c < num_clauses; ++c) 
-    {
-        if(clause_delete[c]==1) {
-            delete_clause_count++;
-            continue;
-        }
-        
-        for(i=0; i<clause_lit_count[c]; ++i)
-        {
-            v = clause_lit[c][i].var_num;
-            var_lit[v][var_lit_count[v]] = clause_lit[c][i];
-            ++var_lit_count[v];
-        }
-        clause_lit[c][i].var_num=0; //new clause boundary
-        clause_lit[c][i].clause_num = -1;
-        
-        //about clause length
-        formula_len += clause_lit_count[c];
-        
-        if(clause_lit_count[c] > max_clause_len)
-            max_clause_len = clause_lit_count[c];
-        else if(clause_lit_count[c] < min_clause_len)
-            min_clause_len = clause_lit_count[c];
-    }
-    
-    avg_clause_len = (double)formula_len/num_clauses;
-    
-    for (v=1; v<=num_vars; ++v) 
-    {
-    	if(fix[v]==1)
-    	{
-    		fix_var_count++;
-    	}
-        var_lit[v][var_lit_count[v]].clause_num=-1;//new var_lit boundary
-    }
-
-    cout<<"c unit propagation fixes "<<fix_var_count<<" variables, and delets "<<delete_clause_count<<" clauses"<<endl;
-    
-}
diff --git a/CCAnr/test.cnf b/CCAnr/test.cnf
deleted file mode 100644
index 1046c52..0000000
--- a/CCAnr/test.cnf
+++ /dev/null
@@ -1,515 +0,0 @@
-p cnf 196 514
--37 -1 0
-37 1 0
--38 -2 0
-38 2 0
--39 -4 0
-39 4 0
--40 -6 0
-40 6 0
--41 -8 0
-41 8 0
--42 -10 0
-42 10 0
--43 -12 0
-43 12 0
--44 -14 0
-44 14 0
--45 -16 0
-45 16 0
--46 -18 0
-46 18 0
--47 -20 0
-47 20 0
--48 -22 0
-48 22 0
--49 -24 0
-49 24 0
--50 -26 0
-50 26 0
--51 -28 0
-51 28 0
--52 -30 0
-52 30 0
--53 -32 0
-53 32 0
--54 -34 0
-54 34 0
-55 37 0
-55 2 0
--37 -2 -55 0
-3 38 56 0
--56 -3 0
--56 -38 0
-5 38 57 0
--57 -5 0
--57 -38 0
-58 39 0
-58 6 0
--39 -6 -58 0
-61 41 0
-61 10 0
--41 -10 -61 0
-64 43 0
-64 14 0
--43 -14 -64 0
-67 45 0
-67 18 0
--45 -18 -67 0
-70 47 0
-70 22 0
--47 -22 -70 0
-73 49 0
-73 26 0
--49 -26 -73 0
-76 51 0
-76 30 0
--51 -30 -76 0
-79 53 0
-79 34 0
--53 -34 -79 0
-7 40 59 0
--59 -7 0
--59 -40 0
-9 40 60 0
--60 -9 0
--60 -40 0
-11 42 62 0
--62 -11 0
--62 -42 0
-13 42 63 0
--63 -13 0
--63 -42 0
-15 44 65 0
--65 -15 0
--65 -44 0
-17 44 66 0
--66 -17 0
--66 -44 0
-19 46 68 0
--68 -19 0
--68 -46 0
-21 46 69 0
--69 -21 0
--69 -46 0
-23 48 71 0
--71 -23 0
--71 -48 0
-25 48 72 0
--72 -25 0
--72 -48 0
-27 50 74 0
--74 -27 0
--74 -50 0
-29 50 75 0
--75 -29 0
--75 -50 0
-31 52 77 0
--77 -31 0
--77 -52 0
-33 52 78 0
--78 -33 0
--78 -52 0
-35 54 80 0
--80 -35 0
--80 -54 0
-36 54 81 0
--81 -36 0
--81 -54 0
--82 55 0
--82 58 0
--82 61 0
--82 64 0
--82 67 0
--82 70 0
--82 73 0
--82 76 0
--82 79 0
--55 -58 -61 -64 -67 -70 -73 -76 -79 82 0
--83 -82 0
-83 82 0
--84 -82 0
-84 82 0
--85 -82 0
-85 82 0
--86 -83 -55 0
--86 83 55 0
-86 -83 55 0
-86 83 -55 0
--87 -83 -58 0
--87 83 58 0
-87 -83 58 0
-87 83 -58 0
--88 -83 -61 0
--88 83 61 0
-88 -83 61 0
-88 83 -61 0
--89 -83 -64 0
--89 83 64 0
-89 -83 64 0
-89 83 -64 0
--90 -83 -67 0
--90 83 67 0
-90 -83 67 0
-90 83 -67 0
--91 -83 -70 0
--91 83 70 0
-91 -83 70 0
-91 83 -70 0
-95 1 0
-95 84 0
--1 -84 -95 0
--92 -83 -73 0
--92 83 73 0
-92 -83 73 0
-92 83 -73 0
-96 84 0
-96 4 0
--84 -4 -96 0
--93 -83 -76 0
--93 83 76 0
-93 -83 76 0
-93 83 -76 0
-97 84 0
-97 8 0
--84 -8 -97 0
--94 -83 -79 0
--94 83 79 0
-94 -83 79 0
-94 83 -79 0
-98 84 0
-98 12 0
--84 -12 -98 0
-99 84 0
-99 16 0
--84 -16 -99 0
-100 84 0
-100 20 0
--84 -20 -100 0
-101 84 0
-101 24 0
--84 -24 -101 0
-102 84 0
-102 28 0
--84 -28 -102 0
-103 84 0
-103 32 0
--84 -32 -103 0
-104 86 0
-104 56 0
--86 -56 -104 0
-105 86 0
-105 57 0
--86 -57 -105 0
-106 87 0
-106 59 0
--87 -59 -106 0
-108 88 0
-108 62 0
--88 -62 -108 0
-110 89 0
-110 65 0
--89 -65 -110 0
-112 90 0
-112 68 0
--90 -68 -112 0
-114 91 0
-114 71 0
--91 -71 -114 0
-116 92 0
-116 74 0
--92 -74 -116 0
-118 93 0
-118 77 0
--93 -77 -118 0
-120 94 0
-120 80 0
--94 -80 -120 0
-107 87 0
-107 60 0
--87 -60 -107 0
-109 88 0
-109 63 0
--88 -63 -109 0
-111 89 0
-111 66 0
--89 -66 -111 0
-113 90 0
-113 69 0
--90 -69 -113 0
-115 91 0
-115 72 0
--91 -72 -115 0
-117 92 0
-117 75 0
--92 -75 -117 0
-119 93 0
-119 78 0
--93 -78 -119 0
-121 94 0
-121 81 0
--94 -81 -121 0
--130 104 0
--130 106 0
--130 108 0
--130 110 0
--130 112 0
--130 114 0
--130 116 0
--130 118 0
--130 120 0
--104 -106 -108 -110 -112 -114 -116 -118 -120 130 0
--122 -105 0
-122 105 0
--123 -107 0
-123 107 0
--124 -109 0
-124 109 0
--125 -111 0
-125 111 0
--126 -113 0
-126 113 0
--127 -115 0
-127 115 0
--128 -117 0
-128 117 0
--129 -119 0
-129 119 0
--131 -121 0
-131 121 0
--132 -130 0
-132 130 0
--133 -130 0
-133 130 0
--134 -130 0
-134 130 0
--135 -132 -104 0
--135 132 104 0
-135 -132 104 0
-135 132 -104 0
--136 -132 -106 0
--136 132 106 0
-136 -132 106 0
-136 132 -106 0
--137 -132 -108 0
--137 132 108 0
-137 -132 108 0
-137 132 -108 0
--138 -132 -110 0
--138 132 110 0
-138 -132 110 0
-138 132 -110 0
-144 3 0
-144 133 0
--3 -133 -144 0
--139 -132 -112 0
--139 132 112 0
-139 -132 112 0
-139 132 -112 0
-145 133 0
-145 7 0
--133 -7 -145 0
--140 -132 -114 0
--140 132 114 0
-140 -132 114 0
-140 132 -114 0
-146 133 0
-146 11 0
--133 -11 -146 0
--141 -132 -116 0
--141 132 116 0
-141 -132 116 0
-141 132 -116 0
-147 133 0
-147 15 0
--133 -15 -147 0
--142 -132 -118 0
--142 132 118 0
-142 -132 118 0
-142 132 -118 0
-148 133 0
-148 19 0
--133 -19 -148 0
--143 -132 -120 0
--143 132 120 0
-143 -132 120 0
-143 132 -120 0
-149 133 0
-149 23 0
--133 -23 -149 0
-150 133 0
-150 27 0
--133 -27 -150 0
-151 133 0
-151 31 0
--133 -31 -151 0
-152 133 0
-152 35 0
--133 -35 -152 0
-153 135 0
-153 122 0
--135 -122 -153 0
-154 136 0
-154 123 0
--136 -123 -154 0
-155 137 0
-155 124 0
--137 -124 -155 0
-156 138 0
-156 125 0
--138 -125 -156 0
-157 139 0
-157 126 0
--139 -126 -157 0
-158 140 0
-158 127 0
--140 -127 -158 0
-159 141 0
-159 128 0
--141 -128 -159 0
-160 142 0
-160 129 0
--142 -129 -160 0
-161 143 0
-161 131 0
--143 -131 -161 0
--162 153 0
--162 154 0
--162 155 0
--162 156 0
--162 157 0
--162 158 0
--162 159 0
--162 160 0
--162 161 0
--153 -154 -155 -156 -157 -158 -159 -160 -161 162 0
--163 -162 0
-163 162 0
--164 -162 0
-164 162 0
-165 5 0
-165 163 0
--5 -163 -165 0
-166 163 0
-166 9 0
--163 -9 -166 0
-167 163 0
-167 13 0
--163 -13 -167 0
-168 163 0
-168 17 0
--163 -17 -168 0
-169 163 0
-169 21 0
--163 -21 -169 0
-170 163 0
-170 25 0
--163 -25 -170 0
-171 163 0
-171 29 0
--163 -29 -171 0
-172 163 0
-172 33 0
--163 -33 -172 0
-173 163 0
-173 36 0
--163 -36 -173 0
-174 2 0
-174 95 0
-174 144 0
-174 165 0
--2 -95 -144 -165 -174 0
-175 96 0
-175 145 0
-175 166 0
-175 6 0
--96 -145 -166 -6 -175 0
-176 97 0
-176 146 0
-176 167 0
-176 10 0
--97 -146 -167 -10 -176 0
-177 98 0
-177 147 0
-177 168 0
-177 14 0
--98 -147 -168 -14 -177 0
-178 99 0
-178 148 0
-178 169 0
-178 18 0
--99 -148 -169 -18 -178 0
-179 100 0
-179 149 0
-179 170 0
-179 22 0
--100 -149 -170 -22 -179 0
-180 101 0
-180 150 0
-180 171 0
-180 26 0
--101 -150 -171 -26 -180 0
-181 102 0
-181 151 0
-181 172 0
-181 30 0
--102 -151 -172 -30 -181 0
-182 103 0
-182 152 0
-182 173 0
-182 34 0
--103 -152 -173 -34 -182 0
--183 -174 0
-183 174 0
--188 175 0
--188 176 0
--188 177 0
--188 178 0
--188 179 0
--188 180 0
--188 181 0
--188 182 0
--175 -176 -177 -178 -179 -180 -181 -182 188 0
--184 -177 0
-184 177 0
--185 -179 0
-185 179 0
--186 -180 0
-186 180 0
--187 -181 0
-187 181 0
-183 188 193 0
--193 -183 0
--193 -188 0
-189 176 0
-189 184 0
--176 -184 -189 0
-190 176 0
-190 177 0
-190 185 0
-190 178 0
--176 -177 -185 -178 -190 0
-191 178 0
-191 177 0
-191 186 0
--178 -177 -186 -191 0
-192 176 0
-192 177 0
-192 180 0
-192 187 0
--176 -177 -180 -187 -192 0
-194 175 0
-194 176 0
-194 189 0
-194 178 0
--175 -176 -189 -178 -194 0
-195 175 0
-195 176 0
-195 190 0
-195 191 0
--175 -176 -190 -191 -195 0
-196 175 0
-196 189 0
-196 190 0
-196 192 0
--175 -189 -190 -192 -196 0
diff --git a/atpg b/atpg
index e54fdb2..5e459eb 100755
Binary files a/atpg and b/atpg differ
diff --git a/circuit.cpp b/circuit.cpp
index 4376100..5156cb3 100644
--- a/circuit.cpp
+++ b/circuit.cpp
@@ -10,10 +10,6 @@ void Circuit::init_stems() {
         if(gate->outputs.size() >= 2) {
             gate->stem = true;
         }
-        // gate->stem = true;
-        // if(rand() % 1000 <= 100) {
-        //     gate->stem = true;
-        // }
         if(gate->stem) {
             stems.push_back(gate);
         }
@@ -37,7 +33,7 @@ void Circuit::init_stems() {
                 }
             }
         }
-        //printf("pre: %s %d\n", g->name.c_str(), g->pre_stems.size());
+        printf("pre: %s %d\n", g->name.c_str(), g->pre_stems.size());
     }
 
     for(Gate *g : gates) {
@@ -179,6 +175,10 @@ bool Circuit::is_valid_circuit() {
             fault_total_cnt += 1;
         }
 
+        if(g->stem) {
+            assert(stem_satisfied[g->id] == (g->cal_value() == g->value));
+        }
+
         // 检查门的赋值情况
         if(g->cal_value() != g->value) {
             printf("WRONG-ASSGIN: %s \n", g->name.c_str());
diff --git a/circuit.h b/circuit.h
index d883458..bef48b5 100644
--- a/circuit.h
+++ b/circuit.h
@@ -117,7 +117,6 @@ ll ls_score();
 
 int** simulate();
 
-
 // time status
 
 int flip_cnt = 0;
@@ -126,4 +125,6 @@ double flip_time = 0;
 int update_cnt = 0;
 double update_time = 0;
 
+std::unordered_set<Gate*> stem_unsatisfied_set;
+
 };
\ No newline at end of file
diff --git a/gate.cpp b/gate.cpp
index 5b79081..c2e1b23 100644
--- a/gate.cpp
+++ b/gate.cpp
@@ -2,7 +2,6 @@
 
 #include "assert.h"
 
-
 int Gate::cal_propagate_len(bool x) {
 
     int fpl[2];
@@ -10,10 +9,8 @@ int Gate::cal_propagate_len(bool x) {
 
     for(Gate* out : outputs) {
         if(!out->is_detected(this)) continue;
-
         fpl[!value] = std::max(fpl[!value], out->fault_propagate_len[!out->value] + 1);
     }
-
     return fpl[x];
 }
 
diff --git a/ls.cpp b/ls.cpp
index 4eeab07..328e35f 100644
--- a/ls.cpp
+++ b/ls.cpp
@@ -23,24 +23,19 @@ bool Circuit::local_search(std::unordered_set<Fault*> &faults) {
 
     while(true) {
 
+        // int ustem = 0;
+        // for(Gate* stem : stems) {
+        //     ustem += !stem_satisfied[stem->id];
+        // }
+        // printf("ustem: %d %d\n", ustem, stem_unsatisfied_set.size());
+        // assert(ustem == stem_unsatisfied_set.size());
+
         auto start = std::chrono::system_clock::now();
 
         Gate* stem = nullptr;
         ll max_score = 0;
         
-        // std::vector<Gate*> stems_random;
-        // std::vector<Gate*> candidates;
-
-        // for(int i=0; i<stems.size(); i++) {
-        //     if(CC[stems[i]->id]) {
-        //         stems_random.push_back(stems[i]);
-        //     }
-        // }
-        // for(int i=0; i<stems_random.size(); i++) {
-        //     std::swap(stems_random[i], stems_random[rand()%stems_random.size()]);
-        // }
-
-        const int T = 50;
+        const int T = 20;
 
         for(int i=0; i<T; i++) {
             Gate* t_stem = stems[rand()%stems.size()];
@@ -120,7 +115,6 @@ bool Circuit::local_search(std::unordered_set<Fault*> &faults) {
             std::chrono::duration<double> elapsed_seconds = end - start;
             update_cnt++;
             update_time += elapsed_seconds.count();
-
             //printf("[UP] flip: %lld, stem: %lld, fault:%lld. flip_cnt: %lld, stem_cnt: %lld, fault_cnt:%lld\n", flip_total_weight, stem_total_weight, fault_total_weight, flip_total_cnt, stem_total_cnt, fault_total_cnt);
         }
     }
@@ -248,11 +242,11 @@ void Circuit::ls_init_weight(const std::unordered_set<Fault*> &faults) {
         fault_weight[f->gate->id][f->type] = 1;
     }
 
-    int r = rand() % faults.size();
-    auto it = faults.begin();
-    std::advance(it, r);
+    // int r = rand() % faults.size();
+    // auto it = faults.begin();
+    // std::advance(it, r);
 
-    fault_weight[(*it)->gate->id][(*it)->type] = 1000000;
+    // fault_weight[(*it)->gate->id][(*it)->type] = 1000000;
 
     for(Gate* s: stems) {
         flip_weight[s->id] = 1;
@@ -349,6 +343,8 @@ void Circuit::ls_block_recal(Gate* stem) {
     }
 
     if(stem->cal_value() == stem->value && !stem_satisfied[stem->id]){
+        stem_unsatisfied_set.erase(stem);
+
         stem_satisfied[stem->id] = true;
         stem_total_weight -= stem_weight[stem->id];
         stem_total_cnt += 1;
@@ -364,6 +360,8 @@ void Circuit::ls_block_recal(Gate* stem) {
     }
     
     if(stem->cal_value() != stem->value && stem_satisfied[stem->id]) {
+        stem_unsatisfied_set.insert(stem);
+
         stem_satisfied[stem->id] = false;
         stem_total_weight += stem_weight[stem->id];
         stem_total_cnt -= 1;
@@ -459,12 +457,14 @@ void Circuit::ls_block_recal(Gate* stem) {
         stem->fault_propagate_len[1] = fpl1;
 
         if(stem->cal_value() == stem->value && !stem_satisfied[stem->id]){
+            stem_unsatisfied_set.erase(stem);
             stem_satisfied[stem->id] = true;
             stem_total_weight -= stem_weight[stem->id];
             stem_total_cnt += 1;
         }
     
         if(stem->cal_value() != stem->value && stem_satisfied[stem->id]) {
+            stem_unsatisfied_set.insert(stem);
             stem_satisfied[stem->id] = false;
             stem_total_weight += stem_weight[stem->id];
             stem_total_cnt -= 1;
diff --git a/show_exp.ipynb b/show_exp.ipynb
deleted file mode 100644
index e946599..0000000
--- a/show_exp.ipynb
+++ /dev/null
@@ -1,38 +0,0 @@
-{
- "cells": [
-  {
-   "cell_type": "code",
-   "execution_count": 1,
-   "metadata": {},
-   "outputs": [],
-   "source": []
-  }
- ],
- "metadata": {
-  "kernelspec": {
-   "display_name": "Python 3",
-   "language": "python",
-   "name": "python3"
-  },
-  "language_info": {
-   "codemirror_mode": {
-    "name": "ipython",
-    "version": 3
-   },
-   "file_extension": ".py",
-   "mimetype": "text/x-python",
-   "name": "python",
-   "nbconvert_exporter": "python",
-   "pygments_lexer": "ipython3",
-   "version": "3.10.7"
-  },
-  "orig_nbformat": 4,
-  "vscode": {
-   "interpreter": {
-    "hash": "e7370f93d1d0cde622a1f8e1c04877d8463912d04d973331ad4851f04de6915a"
-   }
-  }
- },
- "nbformat": 4,
- "nbformat_minor": 2
-}
diff --git a/simulator.cpp b/simulator.cpp
deleted file mode 100644
index 41be410..0000000
--- a/simulator.cpp
+++ /dev/null
@@ -1,150 +0,0 @@
-#include "circuit.h"
-
-#include <assert.h>
-#include <unordered_map>
-
-int cal_value(Gate *g, int *value) {
-    int res;
-
-    switch(g->type) {
-        case Gate::NOT:
-            res = !value[g->inputs[0]->id];
-            break;
-        case Gate::BUF:
-            res = value[g->inputs[0]->id];
-            break;
-        case Gate::AND:
-            res = value[g->inputs[0]->id];
-            for(int i=1; i<g->inputs.size(); i++) {
-                res &= value[g->inputs[i]->id];
-            }
-            break;
-        case Gate::NAND:
-            res = value[g->inputs[0]->id];
-            for(int i=1; i<g->inputs.size(); i++) {
-                res &= value[g->inputs[i]->id];
-            }
-            res = !res;
-            break;
-        case Gate::OR:
-            res = value[g->inputs[0]->id];
-            for(int i=1; i<g->inputs.size(); i++) {
-                res |= value[g->inputs[i]->id];
-            }
-            break;
-        case Gate::NOR:
-            res = value[g->inputs[0]->id];
-            for(int i=1; i<g->inputs.size(); i++) {
-                res |= value[g->inputs[i]->id];
-            }
-            res = !res;
-            break;
-        case Gate::XOR:
-            res = value[g->inputs[0]->id];
-            for(int i=1; i<g->inputs.size(); i++) {
-                res ^= value[g->inputs[i]->id];
-            }
-            break;
-        case Gate::XNOR:
-            res = value[g->inputs[0]->id];
-            for(int i=1; i<g->inputs.size(); i++) {
-                res ^= value[g->inputs[i]->id];
-            }
-            res = !res;
-            break;
-        case Gate::INPUT:
-            res = value[g->id];
-            break;
-        default:
-            assert(false);
-            break;
-    }
-    return res;
-}
-
-bool cal_sa(Gate* g, bool x, int** sa, int *value) {
-    if(g->isPO) {
-        if(x == 0) return value[g->id];
-        else return !value[g->id];
-    }
-
-    bool sa0 = 0;
-    bool sa1 = 0;
-
-    for(Gate* out : g->outputs) {
-        if(!sa[out->id][0] && !sa[out->id][1]) continue;
-
-        if(cal_value(out, value) != value[out->id]) continue;
-
-        value[g->id] = !value[g->id];
-        bool detect = cal_value(out, value) != value[out->id];
-        value[g->id] = !value[g->id];
-        if(!detect) continue;
-
-        sa0 |= value[g->id];
-        sa1 |= !value[g->id];
-    }
-    if(x == 0) return sa0;
-    else return sa1;
-}
-
-
-int** Circuit::simulate() {
-
-    static bool init = false;
-    static int** sa = nullptr;
-    static int* value = nullptr;
-
-    if(!init) {
-        const int MAXN = gates.size() + 1;
-        init = true;
-        sa = new int*[MAXN];
-        for(int i=0; i<MAXN; i++) {
-            sa[i] = new int[2];
-        }
-        value = new int[MAXN];
-    }
-
-    // init PI
-    for(Gate* pi : PIs) {
-        value[pi->id] = pi->value;
-    }
-
-    for(Gate *g : gates) {
-        if(g->isPI) continue;
-        value[g->id] = cal_value(g, value);
-    }
-
-    for(Gate *g : gates) {
-        assert(value[g->id] == cal_value(g, value));
-    }
-
-    std::queue<Gate*> q;
-    std::unordered_map<Gate*, int> topo;
-
-    // init PO
-    for(Gate* po : POs) {
-        sa[po->id][!value[po->id]] = 1;
-        sa[po->id][value[po->id]] = 0;
-        q.push(po);
-    }
-
-    while(!q.empty()) {
-        Gate* g = q.front();
-        q.pop();
-        for(Gate* in : g->inputs) {
-            if(++topo[in] == in->outputs.size()) {
-                sa[in->id][0] = cal_sa(in, 0, sa, value);
-                sa[in->id][1] = cal_sa(in, 1, sa, value);
-                q.push(in);
-            }
-        }
-    }
-
-    for(Gate* g : gates) {
-        assert(sa[g->id][0] == cal_sa(g, 0, sa, value));
-        assert(sa[g->id][1] == cal_sa(g, 1, sa, value));
-    }
-
-    return sa;
-}
\ No newline at end of file