134 lines
3.6 KiB
C
134 lines
3.6 KiB
C
#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;
|
|
|
|
}
|