luke
/
abc
mirror of https://github.com/YosysHQ/abc.git
1
0
Fork 0
Code Issues Packages Projects Releases Wiki Activity

Upgrade to the circuit-based solver.

This commit is contained in:
Alan Mishchenko 2021-04-27 14:46:05 -07:00
parent de71e5f610
commit 5f8a8a596a
12 changed files with 685 additions and 366 deletions
Show Stats Download Patch File Download Diff File Expand all files Collapse all files

27
src/sat/glucose2/AbcGlucose2.cpp
View File

@ -99,15 +99,16 @@ void glucose2_solver_setcallback(Gluco2::SimpSolver* S, void * pman, int(*pfunc)
int glucose2_solver_solve(Gluco2::SimpSolver* S, int * plits, int nlits)
{
vec<Lit> lits;
for (int i=0;i<nlits;i++,plits++)
{
Lit p;
p.x = *plits;
lits.push(p);
}
Gluco2::lbool res = S->solveLimited(lits, 0);
return (res == l_True ? 1 : res == l_False ? -1 : 0);
// vec<Lit> lits;
// for (int i=0;i<nlits;i++,plits++)
// {
// Lit p;
// p.x = *plits;
// lits.push(p);
// }
// Gluco2::lbool res = S->solveLimited(lits, 0);
// return (res == l_True ? 1 : res == l_False ? -1 : 0);
return S->solveLimited(plits, nlits, 0);
}
int glucose2_solver_addvar(Gluco2::SimpSolver* S)
@ -383,6 +384,10 @@ void bmcg2_sat_solver_mark_cone(bmcg2_sat_solver* s, int var)
((Gluco2::SimpSolver*)s)->sat_solver_mark_cone(var);
}
void bmcg2_sat_solver_prelocate( bmcg2_sat_solver * s, int var_num ){
((Gluco2::SimpSolver*)s)->prelocate(var_num);
}
#else
/**Function*************************************************************
@ -721,6 +726,10 @@ void bmcg2_sat_solver_mark_cone(bmcg2_sat_solver* s, int var)
((Gluco2::Solver*)s)->sat_solver_mark_cone(var);
}
void bmcg2_sat_solver_prelocate( bmcg2_sat_solver * s, int var_num ){
((Gluco2::Solver*)s)->prelocate(var_num);
}
#endif

1
src/sat/glucose2/AbcGlucose2.h
View File

@ -103,6 +103,7 @@ extern void bmcg2_sat_solver_set_jftr( bmcg2_sat_solver * s, int jf
extern void bmcg2_sat_solver_set_var_fanin_lit( bmcg2_sat_solver * s, int var, int lit0, int lit1 );
extern void bmcg2_sat_solver_start_new_round( bmcg2_sat_solver * s );
extern void bmcg2_sat_solver_mark_cone( bmcg2_sat_solver * s, int var );
extern void bmcg2_sat_solver_prelocate( bmcg2_sat_solver * s, int var_num );
extern void Glucose2_SolveCnf( char * pFilename, Glucose2_Pars * pPars );
extern int Glucose2_SolveAig( Gia_Man_t * p, Glucose2_Pars * pPars );

1
src/sat/glucose2/CGlucose.h
View File

@ -2,5 +2,6 @@
#define Glucose_CGlucose_h
#define CGLUCOSE_EXP 1
#include "sat/glucose2/Heap2.h"
#endif

254
src/sat/glucose2/CGlucoseCore.h
View File

@ -37,7 +37,10 @@ inline Lit Solver::gateJustFanin(Var v) const {
if(val1 == l_True)
return ~getFaninLit0(v);
//assert( jdata[v].act_fanin == activity[getFaninVar0(v)] || jdata[v].act_fanin == activity[getFaninVar1(v)] );
//assert( jdata[v].act_fanin == (jdata[v].adir? activity[getFaninVar1(v)]: activity[getFaninVar0(v)]) );
return maxActiveLit( ~getFaninLit0(v), ~getFaninLit1(v) );
//return jdata[v].adir? ~getFaninLit1(v): ~getFaninLit0(v);
} else { // xor scope
// should be handled by conflict analysis before entering here
assert( value(v) == l_Undef || value(v) != l_False || val0 == val1 );
@ -54,60 +57,68 @@ inline Lit Solver::gateJustFanin(Var v) const {
// a var should at most be enqueued one time
inline void Solver::pushJustQueue(Var v){
inline void Solver::pushJustQueue(Var v, int index){
assert(v < nVars());
assert(isJReason(v));
if( ! isRoundWatch(v) )\
return;
var2NodeData[v].now = true;
jdata[v].act_fanin = activity[getFaninVar0(v)] > activity[getFaninVar1(v)]? activity[getFaninVar0(v)]: activity[getFaninVar1(v)];
jdata[v].now = true;
jheap.update(v);
if( activity[getFaninVar1(v)] > activity[getFaninVar0(v)] )
jheap.update( JustKey( activity[getFaninVar1(v)], v, index ) );
else
jheap.update( JustKey( activity[getFaninVar0(v)], v, index ) );
}
inline void Solver::uncheckedEnqueue2(Lit p, CRef from)
{
//assert( isRoundWatch(var(p)) ); // inplace sorting guarantee this
assert(value(p) == l_Undef);
assigns[var(p)] = lbool(!sign(p));
vardata[var(p)] = mkVarData(from, decisionLevel());
trail.push_(p);
}
inline void Solver::ResetJustData(bool fCleanMemory){
jstack.shrink_( jstack.size() );
jheap .clear(fCleanMemory);
jhead = 0;
jheap .clear_( fCleanMemory );
}
inline Lit Solver::pickJustLit( Var& j_reason ){
inline Lit Solver::pickJustLit( int& index ){
Var next = var_Undef;
Lit jlit = lit_Undef;
for( int i = 0; i < jstack.size(); i ++ ){
Var x = jstack[i];
if( l_Undef != value(getFaninLit0(x)) || l_Undef != value(getFaninLit1(x)) )
continue;
pushJustQueue(x);
for( ; jhead < trail.size() ; jhead++ ){
Var x = var(trail[jhead]);
if( !decisionLevel() && !isRoundWatch(x) ) continue;
if( isJReason(x) && l_Undef == value( getFaninVar0(x) ) && l_Undef == value( getFaninVar1(x) ) )
pushJustQueue(x,jhead);
}
jstack.shrink_( jstack.size() );
while( ! jheap.empty() && var_Undef != (next = jheap.removeMin()) ){
if( ! jdata[next].now )
while( ! jheap.empty() ){
next = jheap.removeMin(index);
if( ! var2NodeData[next].now )
continue;
assert(isJReason(next));
if( lit_Undef != (jlit = gateJustFanin(next)) )
if( lit_Undef != (jlit = gateJustFanin(next)) ){
//assert( jheap.prev.key() == activity[getFaninVar0(next)] || jheap.prev.key() == activity[getFaninVar1(next)] );
break;
gateAddJwatch(next);
}
gateAddJwatch(next,index);
}
j_reason = next;
return jlit;
}
inline void Solver::gateAddJwatch(Var v){
inline void Solver::gateAddJwatch(Var v,int index){
assert(v < nVars());
assert(isJReason(v));
if( var_Undef != jwatch[v].prev ) // already in jwatch
return;
assert( var_Undef == jwatch[v].prev );
lbool val0, val1;
Var var0, var1;
var0 = getFaninVar0(v);
@ -119,73 +130,38 @@ inline void Solver::gateAddJwatch(Var v){
assert( isAND(v) || (l_Undef != val0 && l_Undef != val1) );
if( (val0 == l_False && val1 == l_False) || !isAND(v) ){
addJwatch(vardata[var0].level < vardata[var1].level? var0: var1, v);
addJwatch(vardata[var0].level < vardata[var1].level? var0: var1, v, index);
return;
}
addJwatch(l_False == val0? var0: var1, v);
}
addJwatch(l_False == val0? var0: var1, v, index);
inline void Solver::gateClearJwatch( Var v, int backtrack_level ){
if( var_Undef == jwatch[v].head )
return ;
Var member, next;
member = jwatch[v].head;
while( var_Undef != member ){
next = jwatch[member].next;
delJwatch( member );
if( vardata[member].level <= backtrack_level )
pushJustQueue(member);
member = next;
}
return;
}
inline void Solver::updateJustActivity( Var v ){
for(Lit lfo = var2Fanout0[ v ]; lfo != toLit(~0); lfo = var2FanoutN[ toInt(lfo) ] ){
if( ! var2NodeData[v].sort )
inplace_sort(v);
int nFanout = 0;
for(Lit lfo = var2Fanout0[ v ]; nFanout < var2NodeData[v].sort; lfo = var2FanoutN[ toInt(lfo) ], nFanout ++ ){
Var x = var(lfo);
if( jdata[x].now && jheap.inHeap(x) ){
jdata[x].act_fanin = activity[getFaninVar0(x)] > activity[getFaninVar1(x)]? activity[getFaninVar0(x)]: activity[getFaninVar1(x)];
jheap.update(x);
if( var2NodeData[x].now && jheap.inHeap(x) ){
if( activity[getFaninVar1(x)] > activity[getFaninVar0(x)] )
jheap.update( JustKey( activity[getFaninVar1(x)], x, jheap.data_attr(x) ) );
else
jheap.update( JustKey( activity[getFaninVar0(x)], x, jheap.data_attr(x) ) );
}
}
}
inline void Solver::addJwatch( Var host, Var member ){
assert( var_Undef == jwatch[member].next && var_Undef == jwatch[member].prev );
if( var_Undef != jwatch[host].head )
jwatch[jwatch[host].head].prev = member;
jwatch[member].next = jwatch[host].head;
jwatch[member].prev = host;
jwatch[host].head = member;
inline void Solver::addJwatch( Var host, Var member, int index ){
assert(level(host) >= level(member));
jnext[index] = jlevel[level(host)];
jlevel[level(host)] = index;
}
inline void Solver::delJwatch( Var member ){
Var prev = jwatch[member].prev;
Var next = jwatch[member].next;
assert( var_Undef != prev ); // must be in a list to be deleted
assert( jwatch[prev].next == member || jwatch[prev].head == member );
if( jwatch[prev].next == member )
jwatch[prev].next = next;
else
jwatch[prev].head = next;
if( var_Undef != next )
jwatch[next].prev = prev;
jwatch[member].prev = var_Undef;
jwatch[member].next = var_Undef;
}
/*
* circuit propagation
*/
@ -270,23 +246,12 @@ inline void Solver::setVarFaninLits( Var v, Lit lit1, Lit lit2 ){
int mincap = var(lit1) < var(lit2)? var(lit2): var(lit1);
mincap = (v < mincap? mincap: v) + 1;
if( var2FaninLits.size() < (mincap<<1) )
var2FaninLits.growTo( (mincap<<1), toLit(~0));
assert( (toLit(~0) == lit1 && toLit(~0) == lit2) || ((v<<1)+1 < var2FaninLits.size()) );
var2FaninLits[ (v<<1) + 0 ] = lit1;
var2FaninLits[ (v<<1) + 1 ] = lit2;
var2NodeData[ v ].lit0 = lit1;
var2NodeData[ v ].lit1 = lit2;
assert( toLit(~0) != lit1 && toLit(~0) != lit2 );
if( var2FanoutN.size() < (mincap<<1) )
var2FanoutN.growTo( (mincap<<1), toLit(~0));
//if( var2FanoutP.size() < (mincap<<1) )
// var2FanoutP.growTo( (mincap<<1), toLit(~0));
if( var2Fanout0.size() < mincap )
var2Fanout0.growTo( mincap, toLit(~0));
var2FanoutN[ (v<<1) + 0 ] = var2Fanout0[ var(lit1) ];
var2FanoutN[ (v<<1) + 1 ] = var2Fanout0[ var(lit2) ];
var2Fanout0[ var(lit1) ] = toLit( (v<<1) + 0 );
@ -301,22 +266,19 @@ inline void Solver::setVarFaninLits( Var v, Lit lit1, Lit lit2 ){
inline bool Solver::isTwoFanin( Var v ) const {
assert(v < nVars());
if( var2FaninLits.size() <= (v<<1)+1 )
return false;
Lit lit0 = var2FaninLits[ (v<<1) + 0 ];
Lit lit1 = var2FaninLits[ (v<<1) + 1 ];
Lit lit0 = var2NodeData[ v ].lit0;
Lit lit1 = var2NodeData[ v ].lit1;
assert( toLit(~0) == lit0 || var(lit0) < nVars() );
assert( toLit(~0) == lit1 || var(lit1) < nVars() );
lit0.x = lit1.x = 0; // suppress the warning - alanmi
return toLit(~0) != var2FaninLits[ (v<<1) + 0 ] && toLit(~0) != var2FaninLits[ (v<<1) + 1 ];
return toLit(~0) != var2NodeData[ v ].lit0 && toLit(~0) != var2NodeData[ v ].lit1;
}
// this implementation return the last conflict encountered
// which follows minisat concept
inline CRef Solver::gatePropagate( Lit p ){
CRef confl = CRef_Undef, stats;
if( justUsage() < 2 || var2FaninLits.size() <= var(p) )
if( justUsage() < 2 )
return CRef_Undef;
if( ! isRoundWatch(var(p)) )
@ -337,10 +299,12 @@ inline CRef Solver::gatePropagate( Lit p ){
check_fanout:
assert( var(p) < var2Fanout0.size() );
for( Lit lfo = var2Fanout0[ var(p) ]; lfo != toLit(~0); lfo = var2FanoutN[ toInt(lfo) ] )
{
if( ! isRoundWatch(var(lfo)) ) continue;
if( ! var2NodeData[var(p)].sort )
inplace_sort(var(p));
int nFanout = 0;
for( Lit lfo = var2Fanout0[ var(p) ]; nFanout < var2NodeData[var(p)].sort; lfo = var2FanoutN[ toInt(lfo) ], nFanout ++ )
{
if( CRef_Undef != (stats = gatePropagateCheckFanout( var(p), lfo )) ){
confl = stats;
if( l_True == value(var(lfo)) )
@ -363,8 +327,8 @@ inline CRef Solver::gatePropagateCheckFanout( Var v, Lit lfo ){
if( l_True == value(var(lfo)) )
return Var2CRef(var(lfo));
jwatch[var(lfo)].header.dir = sign(lfo);
uncheckedEnqueue(~mkLit(var(lfo)), Var2CRef( var(lfo) ) );
var2NodeData[var(lfo)].dir = sign(lfo);
uncheckedEnqueue2(~mkLit(var(lfo)), Var2CRef( var(lfo) ) );
} else {
assert( l_True == value(faninLit) );
@ -381,11 +345,11 @@ inline CRef Solver::gatePropagateCheckFanout( Var v, Lit lfo ){
if( l_True == value(faninLitP) )
return Var2CRef(var(lfo));
uncheckedEnqueue( ~faninLitP, Var2CRef( var(lfo) ) );
uncheckedEnqueue2( ~faninLitP, Var2CRef( var(lfo) ) );
}
else
if( l_True == value(faninLitP) )
uncheckedEnqueue( mkLit(var(lfo)), Var2CRef( var(lfo) ) );
uncheckedEnqueue2( mkLit(var(lfo)), Var2CRef( var(lfo) ) );
}
} else { // xor scope
// check value of the other fanin
@ -400,10 +364,10 @@ inline CRef Solver::gatePropagateCheckFanout( Var v, Lit lfo ){
return CRef_Undef;
else
if( l_Undef == val1 )
uncheckedEnqueue( ~faninLitP ^ ( (l_True == val0) ^ (l_True == valo) ), Var2CRef( var(lfo) ) );
uncheckedEnqueue2( ~faninLitP ^ ( (l_True == val0) ^ (l_True == valo) ), Var2CRef( var(lfo) ) );
else
if( l_Undef == valo )
uncheckedEnqueue( ~mkLit( var(lfo), (l_True == val0) ^ (l_True == val1) ), Var2CRef( var(lfo) ) );
uncheckedEnqueue2( ~mkLit( var(lfo), (l_True == val0) ^ (l_True == val1) ), Var2CRef( var(lfo) ) );
else
if( l_False == (valo ^ (val0 == val1)) )
return Var2CRef(var(lfo));
@ -424,19 +388,19 @@ inline CRef Solver::gatePropagateCheckThis( Var v ){
return CRef_Undef;
if( l_True == value(getFaninLit0(v)) )
uncheckedEnqueue(~getFaninLit1( v ), Var2CRef( v ) );
uncheckedEnqueue2(~getFaninLit1( v ), Var2CRef( v ) );
if( l_True == value(getFaninLit1(v)) )
uncheckedEnqueue(~getFaninLit0( v ), Var2CRef( v ) );
uncheckedEnqueue2(~getFaninLit0( v ), Var2CRef( v ) );
} else {
assert( l_True == value(v) );
if( l_False == value(getFaninLit0(v)) || l_False == value(getFaninLit1(v)) )
confl = Var2CRef(v);
if( l_Undef == value( getFaninLit0( v )) )
uncheckedEnqueue( getFaninLit0( v ), Var2CRef( v ) );
uncheckedEnqueue2( getFaninLit0( v ), Var2CRef( v ) );
if( l_Undef == value( getFaninLit1( v )) )
uncheckedEnqueue( getFaninLit1( v ), Var2CRef( v ) );
uncheckedEnqueue2( getFaninLit1( v ), Var2CRef( v ) );
}
} else { // xor scope
@ -447,10 +411,10 @@ inline CRef Solver::gatePropagateCheckThis( Var v ){
if( l_Undef == val0 && l_Undef == val1 )
return CRef_Undef;
if( l_Undef == val0 )
uncheckedEnqueue(~getFaninLit0( v ) ^ ( (l_True == val1) ^ (l_True == valo) ), Var2CRef( v ) );
uncheckedEnqueue2(~getFaninLit0( v ) ^ ( (l_True == val1) ^ (l_True == valo) ), Var2CRef( v ) );
else
if( l_Undef == val1 )
uncheckedEnqueue(~getFaninLit1( v ) ^ ( (l_True == val0) ^ (l_True == valo) ), Var2CRef( v ) );
uncheckedEnqueue2(~getFaninLit1( v ) ^ ( (l_True == val0) ^ (l_True == valo) ), Var2CRef( v ) );
else
if( l_False == (valo ^ (val0 == val1)) )
return Var2CRef(v);
@ -530,13 +494,7 @@ inline CRef Solver::interpret( Var v, Var t )
Clause& c = ca[itpc];
c[0] = ~mkLit(v);
if( l_False == val0 && l_False == val1 )
c[1] = 0 == jwatch[v].header.dir ? getFaninLit0( v ): getFaninLit1( v );
else
if( l_False == val0 )
c[1] = getFaninLit0( v );
else
c[1] = getFaninLit1( v );
c[1] = var2NodeData[v].dir ? getFaninLit1( v ): getFaninLit0( v );
} else {
setItpcSize(3);
Clause& c = ca[itpc];
@ -594,11 +552,65 @@ inline void Solver::markCone( Var v ){
if( var2TravId[v] >= travId )
return;
var2TravId[v] = travId;
var2NodeData[v].sort = 0;
Var var0, var1;
var0 = getFaninVar0(v);
var1 = getFaninVar1(v);
if( !isTwoFanin(v) )
return;
markCone( getFaninVar0(v) );
markCone( getFaninVar1(v) );
markCone( var0 );
markCone( var1 );
}
inline void Solver::inplace_sort( Var v ){
Lit w, next, prev;
prev= var2Fanout0[v];
if( toLit(~0) == prev ) return;
if( isRoundWatch(var(prev)) )
var2NodeData[v].sort ++ ;
if( toLit(~0) == (w = var2FanoutN[toInt(prev)]) )
return;
while( toLit(~0) != w ){
next = var2FanoutN[toInt(w)];
if( isRoundWatch(var(w)) )
var2NodeData[v].sort ++ ;
if( isRoundWatch(var(w)) && !isRoundWatch(var(prev)) ){
var2FanoutN[toInt(w)] = var2Fanout0[v];
var2Fanout0[v] = w;
var2FanoutN[toInt(prev)] = next;
} else
prev = w;
w = next;
}
}
inline void Solver::prelocate( int base_var_num ){
if( justUsage() ){
var2FanoutN .prelocate( base_var_num << 1 );
var2Fanout0 .prelocate( base_var_num );
var2NodeData.prelocate( base_var_num );
var2TravId .prelocate( base_var_num );
jheap .prelocate( base_var_num );
jlevel .prelocate( base_var_num );
jnext .prelocate( base_var_num );
}
watches .prelocate( base_var_num << 1 );
watchesBin .prelocate( base_var_num << 1 );
decision .prelocate( base_var_num );
trail .prelocate( base_var_num );
assigns .prelocate( base_var_num );
vardata .prelocate( base_var_num );
activity .prelocate( base_var_num );
seen .prelocate( base_var_num );
permDiff .prelocate( base_var_num );
polarity .prelocate( base_var_num );
}
};

390
src/sat/glucose2/Glucose2.cpp
View File

@ -151,7 +151,8 @@ Solver::Solver() :
, nbVarsInitialFormula(INT32_MAX)
#ifdef CGLUCOSE_EXP
, jheap (JustOrderLt(this))
//, jheap (JustOrderLt(this))
, jheap (JustOrderLt2(this))
#endif
{
MYFLAG=0;
@ -175,6 +176,7 @@ Solver::Solver() :
}
#ifdef CGLUCOSE_EXP
jhead= 0;
jftr = 0;
travId = 0;
travId_prev = 0;
@ -233,18 +235,28 @@ Var Solver::newVar(bool sign, bool dvar)
polarity .push(sign);
decision .push();
trail .capacity(v+1);
setDecisionVar(v, dvar);
#ifdef CGLUCOSE_EXP
//jreason .capacity(v+1);
if( justUsage() ){
jdata .push(mkJustData(false));
jwatch .push(mkJustWatch());
var2FanoutN.growTo( nVars()<<1, toLit(~0));
//var2FanoutP.growTo( nVars()<<1, toLit(~0));
var2Fanout0.growTo( nVars(), toLit(~0));
var2TravId .growTo( nVars(), 0);
}
//jdata .push(mkJustData(false));
//jwatch .push(mkJustWatch());
jlevel .push(-1);
jnext .push(-1);
var2FanoutN.growTo( nVars()<<1, toLit(~0));
//var2FanoutP.growTo( nVars()<<1, toLit(~0));
var2Fanout0.growTo( nVars(), toLit(~0));
var2NodeData.growTo( nVars(), mkNodeData());
var2TravId .growTo( nVars(), 0);
setDecisionVar(v, dvar, false);
} else
setDecisionVar(v, dvar);
#else
setDecisionVar(v, dvar);
#endif
return v;
@ -283,7 +295,7 @@ bool Solver::addClause_(vec<Lit>& ps)
return true;
else if (value(ps[i]) != l_False && ps[i] != p)
ps[j++] = p = ps[i];
ps.shrink(i - j);
ps.shrink_(i - j);
if ( 0 ) {
for ( int i = 0; i < ps.size(); i++ )
@ -502,31 +514,45 @@ void Solver::minimisationWithBinaryResolution(vec<Lit> &out_learnt) {
void Solver::cancelUntil(int level) {
if (decisionLevel() > level){
for (int c = trail.size()-1; c >= trail_lim[level]; c--){
Var x = var(trail[c]);
assigns [x] = l_Undef;
if (phase_saving > 1 || ((phase_saving == 1) && c > trail_lim.last()))
polarity[x] = sign(trail[c]);
insertVarOrder(x); }
qhead = trail_lim[level];
#ifdef CGLUCOSE_EXP
if( 0 < justUsage() ){
for (int c = trail.size()-1; c >= trail_lim[level]; c--){
Var x = var(trail[c]);
gateClearJwatch(x, level);
for (int c = trail.size()-1; c >= trail_lim[level]; c--){
Var x = var(trail[c]);
assigns [x] = l_Undef;
if (phase_saving > 1 || ((phase_saving == 1) && c > trail_lim.last()))
polarity[x] = sign(trail[c]);
//gateClearJwatch(x, level);
jdata[x].now = false;
}
}
var2NodeData[x].now = false;
}
for (int l = decisionLevel(); l > level; l -- ){
int q = jlevel[l], k;
jlevel[l] = -1;
while( -1 != q ){
k = jnext[q];
jnext[q] = -1;
Var v = var(trail[q]);
if( Solver::level(v) <= level ){
pushJustQueue(v,q);
}
q = k;
}
}
} else
#endif
for (int c = trail.size()-1; c >= trail_lim[level]; c--){
Var x = var(trail[c]);
assigns [x] = l_Undef;
if (phase_saving > 1 || ((phase_saving == 1) && c > trail_lim.last()))
polarity[x] = sign(trail[c]);
insertVarOrder(x);
}
jhead = qhead = trail_lim[level];
trail.shrink_(trail.size() - trail_lim[level]);
trail_lim.shrink_(trail_lim.size() - level);
jstack.shrink_( jstack.size() );
}
}
@ -577,6 +603,7 @@ Lit Solver::pickBranchLit()
void Solver::analyze(CRef confl, vec<Lit>& out_learnt,vec<Lit>&selectors, int& out_btlevel,unsigned int &lbd,unsigned int &szWithoutSelectors)
{
//double clk = Abc_Clock();
heap_rescale = 0;
int pathC = 0;
Lit p = lit_Undef;
@ -586,22 +613,23 @@ void Solver::analyze(CRef confl, vec<Lit>& out_learnt,vec<Lit>&selectors, int& o
out_learnt.push(); // (leave room for the asserting literal)
int index = trail.size() - 1;
analyze_toclear.shrink_( analyze_toclear.size() );
do{
assert(confl != CRef_Undef); // (otherwise should be UIP)
#ifdef CGLUCOSE_EXP
#ifdef CGLUCOSE_EXP
Clause& c = ca[ lit_Undef != p ? castCRef(p): getConfClause(confl) ];
#else
#else
Clause& c = ca[confl];
#endif
#endif
// Special case for binary clauses
// The first one has to be SAT
if( p != lit_Undef && c.size()==2 && value(c[0])==l_False) {
assert(value(c[1])==l_True);
Lit tmp = c[0];
c[0] = c[1], c[1] = tmp;
assert(value(c[1])==l_True);
Lit tmp = c[0];
c[0] = c[1], c[1] = tmp;
}
if (c.learnt())
@ -610,46 +638,51 @@ void Solver::analyze(CRef confl, vec<Lit>& out_learnt,vec<Lit>&selectors, int& o
#ifdef DYNAMICNBLEVEL
// DYNAMIC NBLEVEL trick (see competition'09 companion paper)
if(c.learnt() && c.lbd()>2) {
unsigned int nblevels = computeLBD(c);
if(nblevels+1<c.lbd() ) { // improve the LBD
if(c.lbd()<=lbLBDFrozenClause) {
c.setCanBeDel(false);
unsigned int nblevels = computeLBD(c);
if(nblevels+1<c.lbd() ) { // improve the LBD
if(c.lbd()<=lbLBDFrozenClause) {
c.setCanBeDel(false);
}
// seems to be interesting : keep it for the next round
c.setLBD(nblevels); // Update it
}
// seems to be interesting : keep it for the next round
c.setLBD(nblevels); // Update it
}
}
#endif
for (int j = (p == lit_Undef) ? 0 : 1; j < c.size(); j++){
Lit q = c[j];
bool fBump = 0;
if (!seen[var(q)] && level(var(q)) > 0){
if(!isSelector(var(q)))
varBumpActivity(var(q));
seen[var(q)] = 1;
if (level(var(q)) >= decisionLevel()) {
pathC++;
#ifdef UPDATEVARACTIVITY
// UPDATEVARACTIVITY trick (see competition'09 companion paper)
#ifdef CGLUCOSE_EXP
if(!isSelector(var(q)) && (reason(var(q))!= CRef_Undef)
&& ! isGateCRef(reason(var(q))) && ca[reason(var(q))].learnt())
lastDecisionLevel.push(q);
#else
if(!isSelector(var(q)) && (reason(var(q))!= CRef_Undef) && ca[reason(var(q))].learnt())
lastDecisionLevel.push(q);
#endif
#endif
} else {
if(isSelector(var(q))) {
assert(value(q) == l_False);
selectors.push(q);
} else
out_learnt.push(q);
}
if(!isSelector(var(q))){
fBump = 1;
varBumpActivity(var(q));
}
seen[var(q)] = 1;
if (level(var(q)) >= decisionLevel()) {
if( fBump )
analyze_toclear.push(q);
pathC++;
#ifdef UPDATEVARACTIVITY
// UPDATEVARACTIVITY trick (see competition'09 companion paper)
#ifdef CGLUCOSE_EXP
if(!isSelector(var(q)) && (reason(var(q))!= CRef_Undef)
&& ! isGateCRef(reason(var(q))) && ca[reason(var(q))].learnt())
lastDecisionLevel.push(q);
#else
if(!isSelector(var(q)) && (reason(var(q))!= CRef_Undef) && ca[reason(var(q))].learnt())
lastDecisionLevel.push(q);
#endif
#endif
} else {
if(isSelector(var(q))) {
assert(value(q) == l_False);
selectors.push(q);
} else
out_learnt.push(q);
}
}
}
@ -667,10 +700,15 @@ void Solver::analyze(CRef confl, vec<Lit>& out_learnt,vec<Lit>&selectors, int& o
//
int i, j;
for(i = 0;i<selectors.size();i++)
out_learnt.push(selectors[i]);
for(i = 0;i<selectors.size();i++) out_learnt.push(selectors[i]);
#ifdef CGLUCOSE_EXP
for(i = 0;i<out_learnt.size();i++)
analyze_toclear.push(out_learnt[i]);
#else
out_learnt.copyTo_(analyze_toclear);
#endif
if (ccmin_mode == 2){
uint32_t abstract_level = 0;
for (i = 1; i < out_learnt.size(); i++)
@ -749,29 +787,51 @@ void Solver::analyze(CRef confl, vec<Lit>& out_learnt,vec<Lit>&selectors, int& o
#ifdef UPDATEVARACTIVITY
// UPDATEVARACTIVITY trick (see competition'09 companion paper)
if(lastDecisionLevel.size()>0) {
for(int i = 0;i<lastDecisionLevel.size();i++) {
#ifdef CGLUCOSE_EXP
Lit t = lastDecisionLevel[i];
if( isGateCRef(reason(var(t))) || ca[reason(var(t))].lbd()<lbd )
varBumpActivity(var(lastDecisionLevel[i]));
#else
if(ca[reason(var(lastDecisionLevel[i]))].lbd()<lbd)
varBumpActivity(var(lastDecisionLevel[i]));
#endif
}
lastDecisionLevel.clear();
}
#endif
// UPDATEVARACTIVITY trick (see competition'09 companion paper)
if(lastDecisionLevel.size()>0) {
for(int i = 0;i<lastDecisionLevel.size();i++) {
Lit t = lastDecisionLevel[i];
//assert( ca[reason(var(t))].learnt() );
if(ca[reason(var(t))].lbd()<lbd)
varBumpActivity(var(t));
}
lastDecisionLevel.shrink_( lastDecisionLevel.size() );
}
#endif
if( justUsage() ){
if( heap_rescale )
{
for (j = 0; j < analyze_toclear.size(); j++) seen[var(analyze_toclear[j])] = 0;
for (j = 0; j < analyze_toclear.size(); j++) seen[var(analyze_toclear[j])] = 0; // ('seen[]' is now cleared)
for(j = 0 ; j<selectors.size() ; j++) seen[var(selectors[j])] = 0;
analyze_toclear.shrink_( analyze_toclear.size() );
for (j = 0; j < jheap.size(); j++){
Var x = jheap[j];
if( var2NodeData[x].now )
analyze_toclear.push(mkLit(x));
}
for (j = 0; j < analyze_toclear.size(); j++){
Var x = var(analyze_toclear[j]);
// jdata[x].act_fanin = activity[getFaninVar0(x)] > activity[getFaninVar1(x)]? activity[getFaninVar0(x)]: activity[getFaninVar1(x)];
// jheap.update(x);
if( activity[getFaninVar1(x)] > activity[getFaninVar0(x)] )
jheap.update( JustKey( activity[getFaninVar1(x)], x, jheap.data_attr(x) ) );
else
jheap.update( JustKey( activity[getFaninVar0(x)], x, jheap.data_attr(x) ) );
}
} else {
for (j = 0; j < analyze_toclear.size(); j++)
{
seen[var(analyze_toclear[j])] = 0;
updateJustActivity(var(analyze_toclear[j]));
}
}
} else
for (j = 0; j < analyze_toclear.size(); j++) seen[var(analyze_toclear[j])] = 0; // ('seen[]' is now cleared)
for(j = 0 ; j<selectors.size() ; j++) seen[var(selectors[j])] = 0;
}
@ -779,7 +839,7 @@ void Solver::analyze(CRef confl, vec<Lit>& out_learnt,vec<Lit>&selectors, int& o
// visiting literals at levels that cannot be removed later.
bool Solver::litRedundant(Lit p, uint32_t abstract_levels)
{
analyze_stack.clear(); analyze_stack.push(p);
analyze_stack.shrink_( analyze_stack.size() ); analyze_stack.push(p);
int top = analyze_toclear.size();
while (analyze_stack.size() > 0){
assert(reason(var(analyze_stack.last())) != CRef_Undef);
@ -826,7 +886,7 @@ bool Solver::litRedundant(Lit p, uint32_t abstract_levels)
|________________________________________________________________________________________________@*/
void Solver::analyzeFinal(Lit p, vec<Lit>& out_conflict)
{
out_conflict.clear();
out_conflict.shrink_( out_conflict.size() );
out_conflict.push(p);
if (decisionLevel() == 0)
@ -863,17 +923,12 @@ void Solver::analyzeFinal(Lit p, vec<Lit>& out_conflict)
void Solver::uncheckedEnqueue(Lit p, CRef from)
{
if( justUsage() && !isRoundWatch(var(p)) )
return;
assert(value(p) == l_Undef);
assigns[var(p)] = lbool(!sign(p));
vardata[var(p)] = mkVarData(from, decisionLevel());
trail.push_(p);
#ifdef CGLUCOSE_EXP
if( 0 < justUsage() ){
jdata[var(p)] = mkJustData( isJReason(var(p)) );
if( isJReason(var(p)) && l_Undef == value( getFaninVar0(var(p)) ) && l_Undef == value( getFaninVar1(var(p)) ) )
jstack.push(var(p));
}
#endif
}
@ -902,13 +957,11 @@ CRef Solver::propagate()
#ifdef CGLUCOSE_EXP
if( 2 <= justUsage() ){
CRef stats;
if( CRef_Undef != (stats = gatePropagate(p)) ){
confl = stats;
if( l_True == value(var(p)) )
return confl;
}
CRef stats;
if( CRef_Undef != (stats = gatePropagate(p)) ){
confl = stats;
if( l_True == value(var(p)) ) return confl;
}
}
#endif
@ -995,7 +1048,7 @@ CRef Solver::propagate()
}
NextClause:;
}
ws.shrink(i - j);
ws.shrink_(i - j);
}
propagations += num_props;
simpDB_props -= num_props;
@ -1065,7 +1118,7 @@ void Solver::reduceDB()
learnts[j++] = learnts[i];
}
}
learnts.shrink(i - j);
learnts.shrink_(i - j);
checkGarbage();
}
@ -1080,7 +1133,7 @@ void Solver::removeSatisfied(vec<CRef>& cs)
else
cs[j++] = cs[i];
}
cs.shrink(i - j);
cs.shrink_(i - j);
}
@ -1119,7 +1172,10 @@ bool Solver::simplify()
checkGarbage();
rebuildOrderHeap();
#ifdef CGLUCOSE_EXP
if( !justUsage() )
#endif
rebuildOrderHeap();
simpDB_assigns = nAssigns();
simpDB_props = clauses_literals + learnts_literals; // (shouldn't depend on stats really, but it will do for now)
@ -1185,8 +1241,8 @@ lbool Solver::search(int nof_conflicts)
if(!blocked) {lastblockatrestart=starts;nbstopsrestartssame++;blocked=true;}
}
learnt_clause.clear();
selectors.clear();
learnt_clause.shrink_( learnt_clause.size() );
selectors .shrink_( selectors.size() );
analyze(confl, learnt_clause, selectors,backtrack_level,nblevels,szWoutSelectors);
lbdQueue.push(nblevels);
@ -1217,31 +1273,30 @@ lbool Solver::search(int nof_conflicts)
claDecayActivity();
}else{
// Our dynamic restart, see the SAT09 competition compagnion paper
if ( (conflictsRestarts && lbdQueue.isvalid() && lbdQueue.getavg()*K > sumLBD/conflictsRestarts) || (pstop && *pstop) ) {
lbdQueue.fastclear();
progress_estimate = progressEstimate();
int bt = 0;
if(incremental) { // DO NOT BACKTRACK UNTIL 0.. USELESS
bt = (decisionLevel()<assumptions.size()) ? decisionLevel() : assumptions.size();
// Our dynamic restart, see the SAT09 competition compagnion paper
if ( (conflictsRestarts && lbdQueue.isvalid() && lbdQueue.getavg()*K > sumLBD/conflictsRestarts) || (pstop && *pstop) ) {
lbdQueue.fastclear();
progress_estimate = progressEstimate();
int bt = 0;
if(incremental) { // DO NOT BACKTRACK UNTIL 0.. USELESS
bt = (decisionLevel()<assumptions.size()) ? decisionLevel() : assumptions.size();
}
cancelUntil(bt);
return l_Undef;
}
cancelUntil(bt);
return l_Undef;
}
// Simplify the set of problem clauses:
if (decisionLevel() == 0 && !simplify()) {
return l_False;
}
// Simplify the set of problem clauses:
if (decisionLevel() == 0 && !simplify()) {
return l_False;
}
// Perform clause database reduction !
if(conflicts>=curRestart* nbclausesbeforereduce)
{
if(conflicts>=curRestart* nbclausesbeforereduce)
{
assert(learnts.size()>0);
curRestart = (conflicts/ nbclausesbeforereduce)+1;
reduceDB();
nbclausesbeforereduce += incReduceDB;
}
}
Lit next = lit_Undef;
while (decisionLevel() < assumptions.size()){
@ -1250,10 +1305,10 @@ lbool Solver::search(int nof_conflicts)
if (value(p) == l_True){
// Dummy decision level:
newDecisionLevel();
}else if (value(p) == l_False){
} else if (value(p) == l_False){
analyzeFinal(~p, conflict);
return l_False;
}else{
} else {
next = p;
break;
}
@ -1261,15 +1316,17 @@ lbool Solver::search(int nof_conflicts)
#ifdef CGLUCOSE_EXP
// pick from JustQueue
Var j_reason = -1;
if (0 < justUsage())
if ( next == lit_Undef ){
decisions++;
next = pickJustLit( j_reason );
if(next == lit_Undef)
return l_True;
addJwatch(var(next), j_reason);
int index = -1;
decisions++;
next = pickJustLit( index );
if(next == lit_Undef)
return l_True;
//addJwatch(var(next), j_reason);
jnext[index] = jlevel[decisionLevel()+1];
jlevel[decisionLevel()+1] = index;
}
#endif
@ -1335,21 +1392,13 @@ lbool Solver::solve_()
#ifdef CGLUCOSE_EXP
ResetJustData(false);
if( 0 < justUsage() )
for(int i=0; i<trail.size(); i++){ // learnt unit clauses
Var v = var(trail[i]);
if( isJReason(v) )
jstack.push(v);
}
#endif
if(incremental && certifiedUNSAT) {
printf("Can not use incremental and certified unsat in the same time\n");
exit(-1);
}
JustModel.shrink_(JustModel.size());
model.shrink_(model.size());
if(incremental && certifiedUNSAT) {
printf("Can not use incremental and certified unsat in the same time\n");
exit(-1);
}
conflict.shrink_(conflict.size());
if (!ok){
travId_prev = travId;
@ -1403,18 +1452,20 @@ printf("c ==================================[ Search Statistics (every %6d confl
if (status == l_True){
if( justUsage() ){
assert(jheap.empty());
//JustModel.growTo(nVars());
int i = 0, j = 0;
JustModel.push(toLit(0));
for (; i < trail.size(); i++)
if( isRoundWatch(var(trail[i])) && !isTwoFanin(var(trail[i])) )
JustModel.push(trail[i]), j++;
JustModel[0] = toLit(j);
JustModel.shrink_(JustModel.size());
assert(jheap.empty());
//JustModel.growTo(nVars());
int i = 0, j = 0;
JustModel.push(toLit(0));
for (; i < trail.size(); i++)
if( isRoundWatch(var(trail[i])) && !isTwoFanin(var(trail[i])) )
JustModel.push(trail[i]), j++;
JustModel[0] = toLit(j);
} else {
// Extend & copy model:
model.growTo(nVars());
for (int i = 0; i < trail.size(); i++) model[ var(trail[i]) ] = value(var(trail[i]));
// Extend & copy model:
model.shrink_(model.size());
model.growTo(nVars());
for (int i = 0; i < trail.size(); i++) model[ var(trail[i]) ] = value(var(trail[i]));
}
}else if (status == l_False && conflict.size() == 0)
ok = false;
@ -1669,25 +1720,28 @@ void Solver::reset()
ResetJustData(false);
jwatch.shrink_(jwatch.size());
jdata .shrink_(jdata .size());
//jwatch.shrink_(jwatch.size());
//jdata .shrink_(jdata .size());
jhead = 0;
travId = 0;
travId_prev = 0;
var2TravId .shrink_(var2TravId.size());
JustModel .shrink_(JustModel .size());
jlevel .shrink_(jlevel.size());
jnext .shrink_(jnext.size());
var2FaninLits.shrink_(var2FaninLits.size());
//var2FaninLits.shrink_(var2FaninLits.size());
var2NodeData .shrink_(var2NodeData .size());
var2Fanout0 .shrink_(var2Fanout0 .size());
var2FanoutN .shrink_(var2FanoutN .size());
//var2FanoutP.clear(false);
if( CRef_Undef != itpc ){
itpc = CRef_Undef; // clause allocator has been cleared, do not worry
// allocate space for clause interpretation
vec<Lit> tmp; tmp.growTo(3);
itpc = ca.alloc(tmp);
ca[itpc].shrink( ca[itpc].size() );
itpc = CRef_Undef; // clause allocator has been cleared, do not worry
// allocate space for clause interpretation
vec<Lit> tmp; tmp.growTo(3);
itpc = ca.alloc(tmp);
ca[itpc].shrink( ca[itpc].size() );
}
#endif
}

11
src/sat/glucose2/Heap.h
View File

@ -85,7 +85,7 @@ class Heap {
void decrease (int n) { assert(inHeap(n)); percolateUp (indices[n]); }
void increase (int n) { assert(inHeap(n)); percolateDown(indices[n]); }
void prelocate (int ext_cap){ indices.prelocate(ext_cap); }
// Safe variant of insert/decrease/increase:
void update(int n)
@ -143,6 +143,15 @@ class Heap {
indices[heap[i]] = -1;
heap.clear(dealloc);
}
void clear_(bool dealloc = false)
{
int i;
for (i = 0; i < heap.size(); i++)
indices[heap[i]] = -1;
if( ! dealloc ) heap.shrink_( heap.size() );
else heap.clear(true);
}
};

169
src/sat/glucose2/Heap2.h Normal file
View File

@ -0,0 +1,169 @@
/******************************************************************************************[Heap.h]
Copyright (c) 2003-2006, Niklas Een, Niklas Sorensson
Copyright (c) 2007-2010, Niklas Sorensson
Permission is hereby granted, free of charge, to any person obtaining a copy of this software and
associated documentation files (the "Software"), to deal in the Software without restriction,
including without limitation the rights to use, copy, modify, merge, publish, distribute,
sublicense, and/or sell copies of the Software, and to permit persons to whom the Software is
furnished to do so, subject to the following conditions:
The above copyright notice and this permission notice shall be included in all copies or
substantial portions of the Software.
THE SOFTWARE IS PROVIDED "AS IS", WITHOUT WARRANTY OF ANY KIND, EXPRESS OR IMPLIED, INCLUDING BUT
NOT LIMITED TO THE WARRANTIES OF MERCHANTABILITY, FITNESS FOR A PARTICULAR PURPOSE AND
NONINFRINGEMENT. IN NO EVENT SHALL THE AUTHORS OR COPYRIGHT HOLDERS BE LIABLE FOR ANY CLAIM,
DAMAGES OR OTHER LIABILITY, WHETHER IN AN ACTION OF CONTRACT, TORT OR OTHERWISE, ARISING FROM, OUT
OF OR IN CONNECTION WITH THE SOFTWARE OR THE USE OR OTHER DEALINGS IN THE SOFTWARE.
**************************************************************************************************/
#ifndef Glucose_Heap2_h
#define Glucose_Heap2_h
#include "sat/glucose2/Vec.h"
ABC_NAMESPACE_CXX_HEADER_START
namespace Gluco2 {
//=================================================================================================
// A heap implementation with support for decrease/increase key.
template<class Comp, class Obj>
class Heap2 {
Comp lt; // The heap is a minimum-heap with respect to this comparator
vec<Obj> heap; // Heap of integers
vec<int> indices; // Each integers position (index) in the Heap
// Index "traversal" functions
static inline int left (int i) { return i*2+1; }
static inline int right (int i) { return (i+1)*2; }
static inline int parent(int i) { return (i-1) >> 1; }
inline int data (int i) const { return heap[i].data();}
void percolateUp(int i)
{
Obj x = heap[i];
int p = parent(i);
while (i != 0 && lt(x, heap[p])){
heap[i] = heap[p];
indices[data(p)] = i;
i = p;
p = parent(p);
}
heap [i] = x;
indices[x.data()] = i;
}
void percolateDown(int i)
{
Obj x = heap[i];
while (left(i) < heap.size()){
int child = right(i) < heap.size() && lt(heap[right(i)], heap[left(i)]) ? right(i) : left(i);
if (!lt(heap[child], x)) break;
heap[i] = heap[child];
indices[data(i)] = i;
i = child;
}
heap [i] = x;
indices[x.data()] = i;
}
public:
Heap2(const Comp& c) : lt(c) { }
int size () const { return heap.size(); }
bool empty () const { return heap.size() == 0; }
bool inHeap (int n) const { return n < indices.size() && indices[n] >= 0; }
int operator[](int index) const { assert(index < heap.size()); return heap[index].data(); }
void decrease (int n) { assert(inHeap(n)); percolateUp (indices[n]); }
void increase (int n) { assert(inHeap(n)); percolateDown(indices[n]); }
void prelocate (int ext_cap){ indices.prelocate(ext_cap); }
int data_attr (int n) const { return heap[indices[n]].attr(); }
// Safe variant of insert/decrease/increase:
void update(const Obj& x)
{
int n = x.data();
if (!inHeap(n))
insert(x);
else {
heap[indices[x.data()]] = x;
percolateUp(indices[n]);
percolateDown(indices[n]); }
}
void insert(const Obj& x)
{
int n = x.data();
indices.growTo(n+1, -1);
assert(!inHeap(n));
indices[n] = heap.size();
heap.push(x);
percolateUp(indices[n]);
}
//Obj prev;
int removeMin(int& _attr)
{
Obj x = heap[0];
heap[0] = heap.last();
indices[heap[0].data()] = 0;
indices[x.data()]= -1;
heap.pop();
if (heap.size() > 1) percolateDown(0);
//prev = x;
_attr = x.attr();
return x.data();
}
// Rebuild the heap from scratch, using the elements in 'ns':
// void build(vec<int>& ns) {
// int i;
// for (i = 0; i < heap.size(); i++)
// indices[heap[i]] = -1;
// heap.clear();
//
// for (i = 0; i < ns.size(); i++){
// indices[ns[i]] = i;
// heap.push(ns[i]); }
//
// for (i = heap.size() / 2 - 1; i >= 0; i--)
// percolateDown(i);
// }
void clear(bool dealloc = false)
{
int i;
for (i = 0; i < heap.size(); i++)
indices[heap[i].data()] = -1;
heap.clear(dealloc);
}
void clear_(bool dealloc = false)
{
int i;
for (i = 0; i < heap.size(); i++)
indices[heap[i].data()] = -1;
if( ! dealloc ) heap.shrink_( heap.size() );
else heap.clear(true);
}
};
//=================================================================================================
}
ABC_NAMESPACE_CXX_HEADER_END
#endif

21
src/sat/glucose2/SimpSolver.h
View File

@ -61,12 +61,25 @@ class SimpSolver : public Solver {
//
bool solve (const vec<Lit>& assumps, bool do_simp = true, bool turn_off_simp = false);
lbool solveLimited(const vec<Lit>& assumps, bool do_simp = true, bool turn_off_simp = false);
int solveLimited(int * lit0, int nlits, bool do_simp = false, bool turn_off_simp = false);
bool solve ( bool do_simp = true, bool turn_off_simp = false);
bool solve (Lit p , bool do_simp = true, bool turn_off_simp = false);
bool solve (Lit p, Lit q, bool do_simp = true, bool turn_off_simp = false);
bool solve (Lit p, Lit q, Lit r, bool do_simp = true, bool turn_off_simp = false);
bool eliminate (bool turn_off_elim = false); // Perform variable elimination based simplification.
void prelocate(int base_var_num){
Solver::prelocate(base_var_num);
frozen .prelocate( base_var_num );
eliminated.prelocate( base_var_num );
if (use_simplification){
n_occ .prelocate( base_var_num << 1 );
occurs .prelocate( base_var_num );
touched .prelocate( base_var_num );
elim_heap .prelocate( base_var_num );
}
}
// Memory managment:
//
virtual void reset();
@ -199,6 +212,14 @@ inline bool SimpSolver::solve (const vec<Lit>& assumps, bool do_simp, boo
inline lbool SimpSolver::solveLimited (const vec<Lit>& assumps, bool do_simp, bool turn_off_simp){
assumps.copyTo(assumptions); return solve_(do_simp, turn_off_simp); }
inline int SimpSolver::solveLimited(int * lit0, int nlits, bool do_simp, bool turn_off_simp){
assumptions.clear();
for(int i = 0; i < nlits; i ++)
assumptions.push(toLit(lit0[i]));
lbool res = solve_(do_simp, turn_off_simp);
return res == l_True ? 1 : (res == l_False ? -1 : 0);
}
inline void SimpSolver::addVar(Var v) { while (v >= nVars()) newVar(); }
//=================================================================================================

20
src/sat/glucose2/SimpSolver2.cpp
View File

@ -707,7 +707,7 @@ void SimpSolver::cleanUpClauses()
for (i = j = 0; i < clauses.size(); i++)
if (ca[clauses[i]].mark() == 0)
clauses[j++] = clauses[i];
clauses.shrink(i - j);
clauses.shrink_(i - j);
}
@ -760,18 +760,22 @@ void SimpSolver::reset()
Solver::reset();
grow = opt_grow;
asymm_lits = eliminated_vars = bwdsub_assigns = n_touched = 0;
elimclauses.clear(false);
touched.clear(false);
occurs.clear(false);
n_occ.clear(false);
elim_heap.clear(false);
subsumption_queue.clear(false);
frozen.clear(false);
eliminated.clear(false);
vec<Lit> dummy(1,lit_Undef);
ca.extra_clause_field = true; // NOTE: must happen before allocating the dummy clause below.
bwdsub_tmpunit = ca.alloc(dummy);
remove_satisfied = false;
occurs.clear(false);
touched .shrink_( touched .size() );
n_occ .shrink_( n_occ .size() );
eliminated .shrink_( eliminated .size() );
frozen .shrink_( frozen .size() );
elimclauses .shrink_( elimclauses .size() );
elim_heap .clear_(false);
}
ABC_NAMESPACE_IMPL_END

133
src/sat/glucose2/Solver.h
View File

@ -71,6 +71,9 @@ public:
void sat_solver_set_var_fanin_lit(int, int, int);
void sat_solver_start_new_round();
void sat_solver_mark_cone(int);
void sat_solver_set_jftr(int);
int sat_solver_jftr();
void sat_solver_reset();
// Problem specification:
//
@ -111,7 +114,7 @@ public:
// Variable mode:
//
void setPolarity (Var v, bool b); // Declare which polarity the decision heuristic should use for a variable. Requires mode 'polarity_user'.
void setDecisionVar (Var v, bool b); // Declare if a variable should be eligible for selection in the decision heuristic.
void setDecisionVar (Var v, bool b, bool use_oheap = true); // Declare if a variable should be eligible for selection in the decision heuristic.
// Read state:
//
@ -365,38 +368,26 @@ protected:
// circuit-based solver
protected:
struct JustData { unsigned now: 1; double act_fanin; };
vec<JustData> jdata;
static inline JustData mkJustData(bool n){ JustData d = {n,0}; return d; }
void uncheckedEnqueue2(Lit p, CRef from = CRef_Undef);
bool heap_rescale;
struct JustOrderLt {
const Solver * pS;
bool operator () (Var x, Var y) const {
if( pS->justActivity(x) != pS->justActivity(y) )
return pS->justActivity(x) > pS->justActivity(y);
if( pS->level(x) != pS->level(y) )
return pS->level(x) < pS->level(y);
return x > y;
}
JustOrderLt(const Solver * _pS) : pS(_pS) { }
};
void addJwatch( Var host, Var member, int index );
//void delJwatch( Var member );
struct JustWatch { struct { unsigned dir:1; } header; Var head; Var next; Var prev; };
vec<JustWatch> jwatch;
static inline JustWatch mkJustWatch(){ JustWatch w = {0, var_Undef, var_Undef, var_Undef}; return w; }
void addJwatch( Var host, Var member );
void delJwatch( Var member );
vec<Lit> var2FaninLits; // (~0): undefine
struct NodeData { Lit lit0; Lit lit1; unsigned sort:30; unsigned dir:1; unsigned now:1; };
static inline NodeData mkNodeData(){ NodeData w; w.lit0 = toLit(~0); w.lit1 = toLit(~0); w.sort = 0; w.dir = 0; w.now = 0; return w; }
vec<NodeData> var2NodeData;
//vec<Lit> var2FaninLits; // (~0): undefine
vec<unsigned> var2TravId;
vec<Lit> var2Fanout0, var2FanoutN, var2FanoutP;
vec<Lit> var2Fanout0, var2FanoutN;//, var2FanoutP;
CRef itpc; // the interpreted clause of a gate
void inplace_sort( Var v );
bool isTwoFanin ( Var v ) const ; // this var has two fanins
bool isAND ( Var v ) const { return getFaninVar0(v) < getFaninVar1(v); }
bool isJReason ( Var v ) const { return isTwoFanin(v) && ( l_False == value(v) || (!isAND(v) && l_Undef != value(v)) ); }
Lit getFaninLit0( Var v ) const { return var2FaninLits[ (v<<1) + 0 ]; }
Lit getFaninLit1( Var v ) const { return var2FaninLits[ (v<<1) + 1 ]; }
Lit getFaninLit0( Var v ) const { return var2NodeData[ v ].lit0; }
Lit getFaninLit1( Var v ) const { return var2NodeData[ v ].lit1; }
bool getFaninC0 ( Var v ) const { return sign(getFaninLit0(v)); }
bool getFaninC1 ( Var v ) const { return sign(getFaninLit1(v)); }
Var getFaninVar0( Var v ) const { return var(getFaninLit0(v)); }
@ -406,7 +397,7 @@ protected:
Lit maxActiveLit(Lit lit0, Lit lit1) const { return activity[var(lit0)] < activity[var(lit1)]? lit1: lit0; }
Lit gateJustFanin(Var v) const ; // l_Undef=satisfied, 0/1 = fanin0/fanin1 requires justify
void gateAddJwatch(Var v);
void gateAddJwatch(Var v,int index);
CRef gatePropagateCheck( Var v, Var t );
CRef gatePropagateCheckThis( Var v );
CRef gatePropagateCheckFanout( Var v, Lit lfo );
@ -415,9 +406,9 @@ protected:
// directly call by original glucose functions
void updateJustActivity( Var v );
void ResetJustData(bool fCleanMemory);
Lit pickJustLit( Var& j_reason );
Lit pickJustLit( int& index );
void justCheck();
void pushJustQueue(Var v);
void pushJustQueue(Var v, int index);
void restoreJustQueue(int level); // call with cancelUntil
void gateClearJwatch( Var v, int backtrack_level );
@ -431,31 +422,58 @@ protected:
Var CRef2Var( CRef cr ) const { return cr & ~(1<<(sizeof(CRef)*8-1)); }
bool isGateCRef( CRef cr ) const { return CRef_Undef != cr && 0 != (cr & (1<<(sizeof(CRef)*8-1))); }
int64_t travId_prev, travId;
unsigned travId_prev, travId;
Heap<JustOrderLt> jheap;
/* jstack
call by unchecked_enqueue
consumed by pickJustLit
cleaned by cancelUntil
*/
vec<Var> jstack;
//Heap<JustOrderLt> jheap;
int jhead;
struct JustKey {
typedef double Key;
typedef Var Data;
typedef int Attr;
Key _key;
Data _data;
Attr _attr;
Data data() const { return _data; }
Key key() const { return _key; }
Attr attr() const { return _attr; }
JustKey():_key(0),_data(0),_attr(0){}
JustKey( const Key& nkey, const Data& ndata, const Attr& nattr ): _key(nkey), _data(ndata), _attr(nattr) {}
};
struct JustOrderLt2 {
const Solver * pS;
bool operator () (const JustKey& x, const JustKey& y) const {
if( x.key() != y.key() ) return x.key() > y.key();
if( pS->level( x.data() ) != pS->level( y.data() ) )
return pS->level( x.data() ) < pS->level( y.data() );
return x.data() > y.data();
}
JustOrderLt2(const Solver * _pS) : pS(_pS) { }
};
Heap2<JustOrderLt2, JustKey> jheap;
vec<int> jlevel;
vec<int> jnext;
public:
void prelocate( int var_num );
void setVarFaninLits( Var v, Lit lit1, Lit lit2 );
void setVarFaninLits( int v, int lit1, int lit2 ){ setVarFaninLits( Var(v), toLit(lit1), toLit(lit2) ); }
//void delVarFaninLits( Var v);
int setNewRound(){ return travId ++ ; }
void setNewRound(){ travId ++ ; }
void markCone( Var v );
void setJust( int njftr ){ jftr = njftr; }
bool isRoundWatch( Var v ) const { return travId==var2TravId[v]; }
void justReset(){ jftr = 0; reset(); }
const JustData& getJustData(int v) const { return jdata[v]; }
//const JustData& getJustData(int v) const { return jdata[v]; }
double varActivity(int v) const { return activity[v];}
double justActivity(int v) const { return jdata[v].act_fanin;}
//double justActivity(int v) const { return jdata[v].act_fanin;}
int varPolarity(int v){ return polarity[v]? 1: 0;}
vec<Lit> JustModel; // model obtained by justification enabled
int justUsage() const ;
int solveLimited( int * , int nlits );
};
@ -466,32 +484,26 @@ inline CRef Solver::reason(Var x) const { return vardata[x].reason; }
inline int Solver::level (Var x) const { return vardata[x].level; }
inline void Solver::insertVarOrder(Var x) {
if (!order_heap.inHeap(x) && decision[x]) order_heap.insert(x); }
#ifdef CGLUCOSE_EXP
if (!justUsage() && !order_heap.inHeap(x) && decision[x]) order_heap.insert(x);
#else
if (!order_heap.inHeap(x) && decision[x]) order_heap.insert(x);
#endif
}
inline void Solver::varDecayActivity() { var_inc *= (1 / var_decay); }
inline void Solver::varBumpActivity(Var v) { varBumpActivity(v, var_inc); }
inline void Solver::varBumpActivity(Var v, double inc) {
if ( (activity[v] += inc) > 1e100 ) {
heap_rescale = 1;
// Rescale:
for (int i = 0; i < nVars(); i++)
activity[i] *= 1e-100;
if( justUsage() )
for (int i = 0; i < jheap.size(); i++){
Var j = jheap[i];
jdata[j].act_fanin = activity[getFaninVar0(j)] > activity[getFaninVar1(j)]? activity[getFaninVar0(j)]: activity[getFaninVar1(j)];
}
var_inc *= 1e-100; }
// Update order_heap with respect to new activity:
if (order_heap.inHeap(v))
if (!justUsage() && order_heap.inHeap(v))
order_heap.decrease(v);
#ifdef CGLUCOSE_EXP
if( justUsage() )
updateJustActivity(v);
#endif
}
inline void Solver::claDecayActivity() { cla_inc *= (1 / clause_decay); }
@ -550,13 +562,13 @@ inline int Solver::nVars () const { return vardata.size(); }
inline int Solver::nFreeVars () const { return (int)dec_vars - (trail_lim.size() == 0 ? trail.size() : trail_lim[0]); }
inline int * Solver::getCex () const { return (int*) &JustModel[0]; }
inline void Solver::setPolarity (Var v, bool b) { polarity[v] = b; }
inline void Solver::setDecisionVar(Var v, bool b)
inline void Solver::setDecisionVar(Var v, bool b, bool use_oheap)
{
if ( b && !decision[v]) dec_vars++;
else if (!b && decision[v]) dec_vars--;
decision[v] = b;
insertVarOrder(v);
if( use_oheap ) insertVarOrder(v);
}
inline void Solver::setConfBudget(int64_t x){ conflict_budget = conflicts + x; }
inline void Solver::setPropBudget(int64_t x){ propagation_budget = propagations + x; }
@ -589,7 +601,16 @@ inline void Solver::addVar(Var v) { while (v >= nVars()) newVar(); }
inline void Solver::sat_solver_set_var_fanin_lit(int v, int lit0, int lit1) { setVarFaninLits( Var(v), toLit(lit0), toLit(lit1) ); }
inline void Solver::sat_solver_start_new_round() { setNewRound(); }
inline void Solver::sat_solver_mark_cone(int v) { markCone(v); }
inline void Solver::sat_solver_set_jftr( int njftr ){ setJust(njftr); }
inline int Solver::sat_solver_jftr(){ return jftr; }
inline void Solver::sat_solver_reset(){ justReset(); }
inline int Solver::solveLimited( int * lit0, int nlits ){
assumptions.clear();
for(int i = 0; i < nlits; i ++)
assumptions.push(toLit(lit0[i]));
lbool res = solve_();
return res == l_True ? 1 : (res == l_False ? -1 : 0);
}
//=================================================================================================
// Debug etc:

5
src/sat/glucose2/SolverTypes.h
View File

@ -298,6 +298,7 @@ class OccLists
OccLists(const Deleted& d) : deleted(d) {}
void init (const Idx& idx){ occs.growTo(toInt(idx)+1); dirty.growTo(toInt(idx)+1, 0); }
void prelocate (const int num){ occs.prelocate(num); dirty.prelocate(num); }
// Vec& operator[](const Idx& idx){ return occs[toInt(idx)]; }
Vec& operator[](const Idx& idx){ return occs[toInt(idx)]; }
Vec& lookup (const Idx& idx){ if (dirty[toInt(idx)]) clean(idx); return occs[toInt(idx)]; }
@ -332,7 +333,7 @@ void OccLists<Idx,Vec,Deleted>::cleanAll()
// Dirties may contain duplicates so check here if a variable is already cleaned:
if (dirty[toInt(dirties[i])])
clean(dirties[i]);
dirties.clear();
dirties.shrink_( dirties.size() );
}
@ -344,7 +345,7 @@ void OccLists<Idx,Vec,Deleted>::clean(const Idx& idx)
for (i = j = 0; i < vec.size(); i++)
if (!deleted(vec[i]))
vec[j++] = vec[i];
vec.shrink(i - j);
vec.shrink_(i - j);
dirty[toInt(idx)] = 0;
}

19
src/sat/glucose2/Vec.h
View File

@ -67,7 +67,9 @@ public:
void shrink_ (int nelems) { assert(nelems <= sz); sz -= nelems; }
int capacity (void) const { return cap; }
void capacity (int min_cap);
void prelocate(int ext_cap);
void growTo (int size);
void growTo_ (int size);
void growTo (int size, const T& pad);
void clear (bool dealloc = false);
@ -90,7 +92,7 @@ public:
// Duplicatation (preferred instead):
void copyTo (vec<T>& copy) const { copy.clear(); copy.growTo(sz); for (int i = 0; i < sz; i++) copy[i] = data[i]; }
void copyTo_(vec<T>& copy) const { copy.shrink_(copy.size()); copy.growTo(sz); for (int i = 0; i < sz; i++) copy[i] = data[i]; }
void copyTo_(vec<T>& copy) const { copy.shrink_(copy.size()); copy.growTo_(sz); for (int i = 0; i < sz; i++) copy[i] = data[i]; }
void moveTo(vec<T>& dest) { dest.clear(true); dest.data = data; dest.sz = sz; dest.cap = cap; data = NULL; sz = 0; cap = 0; }
};
@ -103,6 +105,14 @@ void vec<T>::capacity(int min_cap) {
throw OutOfMemoryException();
}
template<class T>
void vec<T>::prelocate(int ext_cap) {
if (cap >= ext_cap) return;
if (ext_cap > INT_MAX || (((data = (T*)::realloc(data, ext_cap * sizeof(T))) == NULL) && errno == ENOMEM))
throw OutOfMemoryException();
cap = ext_cap;
}
template<class T>
void vec<T>::growTo(int size, const T& pad) {
@ -120,6 +130,13 @@ void vec<T>::growTo(int size) {
sz = size; }
template<class T>
void vec<T>::growTo_(int size) {
if (sz >= size) return;
capacity(size);
sz = size; }
template<class T>
void vec<T>::clear(bool dealloc) {
if (data != NULL){