293 lines
6.5 KiB
C++
293 lines
6.5 KiB
C++
#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;
|
|
}
|