可用版
This commit is contained in:
parent
d4c6df7b98
commit
38f925c9a4
BIN
CCAnr/CCAnr
BIN
CCAnr/CCAnr
Binary file not shown.
@ -1,2 +0,0 @@
|
|||||||
CCAnr: cca.cpp cca.h basis.h cw.h preprocessor.h
|
|
||||||
g++ cca.cpp -O3 -static -o CCAnr
|
|
||||||
377
CCAnr/basis.h
377
CCAnr/basis.h
@ -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
|
|
||||||
|
|
||||||
292
CCAnr/cca.cpp
292
CCAnr/cca.cpp
@ -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;
|
|
||||||
}
|
|
||||||
295
CCAnr/cca.h
295
CCAnr/cca.h
@ -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
|
|
||||||
|
|
||||||
@ -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();
|
|
||||||
}
|
|
||||||
103
CCAnr/cw.h
103
CCAnr/cw.h
@ -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
|
|
||||||
@ -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;
|
|
||||||
|
|
||||||
}
|
|
||||||
515
CCAnr/test.cnf
515
CCAnr/test.cnf
@ -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
|
|
||||||
10
circuit.cpp
10
circuit.cpp
@ -10,10 +10,6 @@ void Circuit::init_stems() {
|
|||||||
if(gate->outputs.size() >= 2) {
|
if(gate->outputs.size() >= 2) {
|
||||||
gate->stem = true;
|
gate->stem = true;
|
||||||
}
|
}
|
||||||
// gate->stem = true;
|
|
||||||
// if(rand() % 1000 <= 100) {
|
|
||||||
// gate->stem = true;
|
|
||||||
// }
|
|
||||||
if(gate->stem) {
|
if(gate->stem) {
|
||||||
stems.push_back(gate);
|
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) {
|
for(Gate *g : gates) {
|
||||||
@ -179,6 +175,10 @@ bool Circuit::is_valid_circuit() {
|
|||||||
fault_total_cnt += 1;
|
fault_total_cnt += 1;
|
||||||
}
|
}
|
||||||
|
|
||||||
|
if(g->stem) {
|
||||||
|
assert(stem_satisfied[g->id] == (g->cal_value() == g->value));
|
||||||
|
}
|
||||||
|
|
||||||
// 检查门的赋值情况
|
// 检查门的赋值情况
|
||||||
if(g->cal_value() != g->value) {
|
if(g->cal_value() != g->value) {
|
||||||
printf("WRONG-ASSGIN: %s \n", g->name.c_str());
|
printf("WRONG-ASSGIN: %s \n", g->name.c_str());
|
||||||
|
|||||||
@ -117,7 +117,6 @@ ll ls_score();
|
|||||||
|
|
||||||
int** simulate();
|
int** simulate();
|
||||||
|
|
||||||
|
|
||||||
// time status
|
// time status
|
||||||
|
|
||||||
int flip_cnt = 0;
|
int flip_cnt = 0;
|
||||||
@ -126,4 +125,6 @@ double flip_time = 0;
|
|||||||
int update_cnt = 0;
|
int update_cnt = 0;
|
||||||
double update_time = 0;
|
double update_time = 0;
|
||||||
|
|
||||||
|
std::unordered_set<Gate*> stem_unsatisfied_set;
|
||||||
|
|
||||||
};
|
};
|
||||||
3
gate.cpp
3
gate.cpp
@ -2,7 +2,6 @@
|
|||||||
|
|
||||||
#include "assert.h"
|
#include "assert.h"
|
||||||
|
|
||||||
|
|
||||||
int Gate::cal_propagate_len(bool x) {
|
int Gate::cal_propagate_len(bool x) {
|
||||||
|
|
||||||
int fpl[2];
|
int fpl[2];
|
||||||
@ -10,10 +9,8 @@ int Gate::cal_propagate_len(bool x) {
|
|||||||
|
|
||||||
for(Gate* out : outputs) {
|
for(Gate* out : outputs) {
|
||||||
if(!out->is_detected(this)) continue;
|
if(!out->is_detected(this)) continue;
|
||||||
|
|
||||||
fpl[!value] = std::max(fpl[!value], out->fault_propagate_len[!out->value] + 1);
|
fpl[!value] = std::max(fpl[!value], out->fault_propagate_len[!out->value] + 1);
|
||||||
}
|
}
|
||||||
|
|
||||||
return fpl[x];
|
return fpl[x];
|
||||||
}
|
}
|
||||||
|
|
||||||
|
|||||||
36
ls.cpp
36
ls.cpp
@ -23,24 +23,19 @@ bool Circuit::local_search(std::unordered_set<Fault*> &faults) {
|
|||||||
|
|
||||||
while(true) {
|
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();
|
auto start = std::chrono::system_clock::now();
|
||||||
|
|
||||||
Gate* stem = nullptr;
|
Gate* stem = nullptr;
|
||||||
ll max_score = 0;
|
ll max_score = 0;
|
||||||
|
|
||||||
// std::vector<Gate*> stems_random;
|
const int T = 20;
|
||||||
// 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;
|
|
||||||
|
|
||||||
for(int i=0; i<T; i++) {
|
for(int i=0; i<T; i++) {
|
||||||
Gate* t_stem = stems[rand()%stems.size()];
|
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;
|
std::chrono::duration<double> elapsed_seconds = end - start;
|
||||||
update_cnt++;
|
update_cnt++;
|
||||||
update_time += elapsed_seconds.count();
|
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);
|
//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;
|
fault_weight[f->gate->id][f->type] = 1;
|
||||||
}
|
}
|
||||||
|
|
||||||
int r = rand() % faults.size();
|
// int r = rand() % faults.size();
|
||||||
auto it = faults.begin();
|
// auto it = faults.begin();
|
||||||
std::advance(it, r);
|
// std::advance(it, r);
|
||||||
|
|
||||||
fault_weight[(*it)->gate->id][(*it)->type] = 1000000;
|
// fault_weight[(*it)->gate->id][(*it)->type] = 1000000;
|
||||||
|
|
||||||
for(Gate* s: stems) {
|
for(Gate* s: stems) {
|
||||||
flip_weight[s->id] = 1;
|
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]){
|
if(stem->cal_value() == stem->value && !stem_satisfied[stem->id]){
|
||||||
|
stem_unsatisfied_set.erase(stem);
|
||||||
|
|
||||||
stem_satisfied[stem->id] = true;
|
stem_satisfied[stem->id] = true;
|
||||||
stem_total_weight -= stem_weight[stem->id];
|
stem_total_weight -= stem_weight[stem->id];
|
||||||
stem_total_cnt += 1;
|
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]) {
|
if(stem->cal_value() != stem->value && stem_satisfied[stem->id]) {
|
||||||
|
stem_unsatisfied_set.insert(stem);
|
||||||
|
|
||||||
stem_satisfied[stem->id] = false;
|
stem_satisfied[stem->id] = false;
|
||||||
stem_total_weight += stem_weight[stem->id];
|
stem_total_weight += stem_weight[stem->id];
|
||||||
stem_total_cnt -= 1;
|
stem_total_cnt -= 1;
|
||||||
@ -459,12 +457,14 @@ void Circuit::ls_block_recal(Gate* stem) {
|
|||||||
stem->fault_propagate_len[1] = fpl1;
|
stem->fault_propagate_len[1] = fpl1;
|
||||||
|
|
||||||
if(stem->cal_value() == stem->value && !stem_satisfied[stem->id]){
|
if(stem->cal_value() == stem->value && !stem_satisfied[stem->id]){
|
||||||
|
stem_unsatisfied_set.erase(stem);
|
||||||
stem_satisfied[stem->id] = true;
|
stem_satisfied[stem->id] = true;
|
||||||
stem_total_weight -= stem_weight[stem->id];
|
stem_total_weight -= stem_weight[stem->id];
|
||||||
stem_total_cnt += 1;
|
stem_total_cnt += 1;
|
||||||
}
|
}
|
||||||
|
|
||||||
if(stem->cal_value() != stem->value && stem_satisfied[stem->id]) {
|
if(stem->cal_value() != stem->value && stem_satisfied[stem->id]) {
|
||||||
|
stem_unsatisfied_set.insert(stem);
|
||||||
stem_satisfied[stem->id] = false;
|
stem_satisfied[stem->id] = false;
|
||||||
stem_total_weight += stem_weight[stem->id];
|
stem_total_weight += stem_weight[stem->id];
|
||||||
stem_total_cnt -= 1;
|
stem_total_cnt -= 1;
|
||||||
|
|||||||
@ -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
|
|
||||||
}
|
|
||||||
150
simulator.cpp
150
simulator.cpp
@ -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;
|
|
||||||
}
|
|
||||||
Loading…
x
Reference in New Issue
Block a user