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

Experiments with SAT sweeping.

This commit is contained in:
Alan Mishchenko 2022-04-24 09:29:52 -07:00
parent 8e13245ed0
commit 1f56f20e1b
11 changed files with 3794 additions and 14 deletions
Show Stats Download Patch File Download Diff File Expand all files Collapse all files

12
abclib.dsp
View File

@ -4931,6 +4931,14 @@ SOURCE=.\src\aig\gia\giaCSatOld.c
# End Source File
# Begin Source File
SOURCE=.\src\aig\gia\giaCSatP.c
# End Source File
# Begin Source File
SOURCE=.\src\aig\gia\giaCSatP.h
# End Source File
# Begin Source File
SOURCE=.\src\aig\gia\giaCTas.c
# End Source File
# Begin Source File
@ -5587,6 +5595,10 @@ SOURCE=.\src\proof\cec\cecSatG2.c
# End Source File
# Begin Source File
SOURCE=.\src\proof\cec\cecSatG3.c
# End Source File
# Begin Source File
SOURCE=.\src\proof\cec\cecSeq.c
# End Source File
# Begin Source File

1209
src/aig/gia/giaCSatP.c Normal file
View File

File diff suppressed because it is too large Load Diff

117
src/aig/gia/giaCSatP.h Normal file
View File

@ -0,0 +1,117 @@
#ifndef ABC__aig__gia__giaCSatP_h
#define ABC__aig__gia__giaCSatP_h
////////////////////////////////////////////////////////////////////////
/// INCLUDES ///
////////////////////////////////////////////////////////////////////////
#include "gia.h"
////////////////////////////////////////////////////////////////////////
/// PARAMETERS ///
////////////////////////////////////////////////////////////////////////
ABC_NAMESPACE_HEADER_START
typedef struct CbsP_Par_t_ CbsP_Par_t;
struct CbsP_Par_t_
{
// conflict limits
int nBTLimit; // limit on the number of conflicts
int nJustLimit; // limit on the size of justification queue
// current parameters
int nBTThis; // number of conflicts
int nBTThisNc; // number of conflicts
int nJustThis; // max size of the frontier
int nBTTotal; // total number of conflicts
int nJustTotal; // total size of the frontier
// decision heuristics
int fUseHighest; // use node with the highest ID
int fUseLowest; // use node with the highest ID
int fUseMaxFF; // use node with the largest fanin fanout
// other
int fVerbose;
int fUseProved;
// statistics
int nJscanThis;
int nRscanThis;
int nPropThis;
int maxJscanUndec;
int maxRscanUndec;
int maxPropUndec;
int maxJscanSolved;
int maxRscanSolved;
int maxPropSolved;
int nSat, nUnsat, nUndec;
long accJscanSat;
long accJscanUnsat;
long accJscanUndec;
long accRscanSat;
long accRscanUnsat;
long accRscanUndec;
long accPropSat;
long accPropUnsat;
long accPropUndec;
// other limits
int nJscanLimit;
int nRscanLimit;
int nPropLimit;
};
typedef struct CbsP_Que_t_ CbsP_Que_t;
struct CbsP_Que_t_
{
int iHead; // beginning of the queue
int iTail; // end of the queue
int nSize; // allocated size
Gia_Obj_t ** pData; // nodes stored in the queue
};
typedef struct CbsP_Man_t_ CbsP_Man_t;
struct CbsP_Man_t_
{
CbsP_Par_t Pars; // parameters
Gia_Man_t * pAig; // AIG manager
CbsP_Que_t pProp; // propagation queue
CbsP_Que_t pJust; // justification queue
CbsP_Que_t pClauses; // clause queue
Gia_Obj_t ** pIter; // iterator through clause vars
Vec_Int_t * vLevReas; // levels and decisions
Vec_Int_t * vValue;
Vec_Int_t * vModel; // satisfying assignment
Vec_Ptr_t * vTemp; // temporary storage
// SAT calls statistics
int nSatUnsat; // the number of proofs
int nSatSat; // the number of failure
int nSatUndec; // the number of timeouts
int nSatTotal; // the number of calls
// conflicts
int nConfUnsat; // conflicts in unsat problems
int nConfSat; // conflicts in sat problems
int nConfUndec; // conflicts in undec problems
// runtime stats
abctime timeSatUnsat; // unsat
abctime timeSatSat; // sat
abctime timeSatUndec; // undecided
abctime timeTotal; // total runtime
};
CbsP_Man_t * CbsP_ManAlloc( Gia_Man_t * pGia );
void CbsP_ManStop( CbsP_Man_t * p );
void CbsP_ManSatPrintStats( CbsP_Man_t * p );
void CbsP_PrintRecord( CbsP_Par_t * pPars );
int CbsP_ManSolve2( CbsP_Man_t * p, Gia_Obj_t * pObj, Gia_Obj_t * pObj2 );
#define CBS_UNSAT 1
#define CBS_SAT 0
#define CBS_UNDEC -1
ABC_NAMESPACE_HEADER_END
#endif

1
src/aig/gia/module.make
View File

@ -15,6 +15,7 @@ SRC += src/aig/gia/giaAig.c \
src/aig/gia/giaCSat.c \
src/aig/gia/giaCSat2.c \
src/aig/gia/giaCSat3.c \
src/aig/gia/giaCSatP.c \
src/aig/gia/giaCTas.c \
src/aig/gia/giaCut.c \
src/aig/gia/giaDecs.c \

18
src/base/abci/abc.c
View File

@ -36996,11 +36996,12 @@ int Abc_CommandAbc9Fraig( Abc_Frame_t * pAbc, int argc, char ** argv )
extern Gia_Man_t * Cec2_ManSimulateTest( Gia_Man_t * p, Cec_ParFra_t * pPars );
extern Gia_Man_t * Cec3_ManSimulateTest( Gia_Man_t * p, Cec_ParFra_t * pPars );
extern Gia_Man_t * Cec4_ManSimulateTest( Gia_Man_t * p, Cec_ParFra_t * pPars );
extern Gia_Man_t * Cec5_ManSimulateTest( Gia_Man_t * p, Cec_ParFra_t * pPars );
Cec_ParFra_t ParsFra, * pPars = &ParsFra; Gia_Man_t * pTemp;
int c, fUseAlgo = 0, fUseAlgoG = 0, fUseAlgoG2 = 0;
int c, fUseAlgo = 0, fUseAlgoG = 0, fUseAlgoX = 0, fUseAlgoY = 0;
Cec4_ManSetParams( pPars );
Extra_UtilGetoptReset();
while ( ( c = Extra_UtilGetopt( argc, argv, "JWRILDCNPrmdckngxwvh" ) ) != EOF )
while ( ( c = Extra_UtilGetopt( argc, argv, "JWRILDCNPrmdckngxywvh" ) ) != EOF )
{
switch ( c )
{
@ -37125,7 +37126,10 @@ int Abc_CommandAbc9Fraig( Abc_Frame_t * pAbc, int argc, char ** argv )
fUseAlgoG ^= 1;
break;
case 'x':
fUseAlgoG2 ^= 1;
fUseAlgoX ^= 1;
break;
case 'y':
fUseAlgoY ^= 1;
break;
case 'w':
pPars->fVeryVerbose ^= 1;
@ -37146,15 +37150,17 @@ int Abc_CommandAbc9Fraig( Abc_Frame_t * pAbc, int argc, char ** argv )
pTemp = Cec2_ManSimulateTest( pAbc->pGia, pPars );
else if ( fUseAlgoG )
pTemp = Cec3_ManSimulateTest( pAbc->pGia, pPars );
else if ( fUseAlgoG2 )
else if ( fUseAlgoX )
pTemp = Cec4_ManSimulateTest( pAbc->pGia, pPars );
else if ( fUseAlgoY )
pTemp = Cec5_ManSimulateTest( pAbc->pGia, pPars );
else
pTemp = Cec_ManSatSweeping( pAbc->pGia, pPars, 0 );
Abc_FrameUpdateGia( pAbc, pTemp );
return 0;
usage:
Abc_Print( -2, "usage: &fraig [-JWRILDCNP <num>] [-rmdckngwvh]\n" );
Abc_Print( -2, "usage: &fraig [-JWRILDCNP <num>] [-rmdckngxywvh]\n" );
Abc_Print( -2, "\t performs combinational SAT sweeping\n" );
Abc_Print( -2, "\t-J num : the solver type [default = %d]\n", pPars->jType );
Abc_Print( -2, "\t-W num : the number of simulation words [default = %d]\n", pPars->nWords );
@ -37172,6 +37178,8 @@ usage:
Abc_Print( -2, "\t-k : toggle using logic cones in the SAT solver [default = %s]\n", pPars->fUseCones? "yes": "no" );
Abc_Print( -2, "\t-n : toggle using new implementation [default = %s]\n", fUseAlgo? "yes": "no" );
Abc_Print( -2, "\t-g : toggle using another new implementation [default = %s]\n", fUseAlgoG? "yes": "no" );
Abc_Print( -2, "\t-x : toggle using another new implementation [default = %s]\n", fUseAlgoX? "yes": "no" );
Abc_Print( -2, "\t-y : toggle using another new implementation [default = %s]\n", fUseAlgoY? "yes": "no" );
Abc_Print( -2, "\t-w : toggle printing even more verbose information [default = %s]\n", pPars->fVeryVerbose? "yes": "no" );
Abc_Print( -2, "\t-v : toggle printing verbose information [default = %s]\n", pPars->fVerbose? "yes": "no" );
Abc_Print( -2, "\t-h : print the command usage\n");

2330
src/proof/cec/cecSatG3.c Normal file
View File

File diff suppressed because it is too large Load Diff

1
src/proof/cec/module.make
View File

@ -9,6 +9,7 @@ SRC += src/proof/cec/cecCec.c \
src/proof/cec/cecSat.c \
src/proof/cec/cecSatG.c \
src/proof/cec/cecSatG2.c \
src/proof/cec/cecSatG3.c \
src/proof/cec/cecSeq.c \
src/proof/cec/cecSim.c \
src/proof/cec/cecSolve.c \

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

@ -1536,6 +1536,12 @@ int Glucose2_SolveAig(Gia_Man_t * p, Glucose2_Pars * pPars)
return (ret == l_True ? 10 : ret == l_False ? 20 : 0);
}
extern "C" {
void glucose2_markapprox( void * pSat, int v0, int v1, int nlim ){
((Gluco2::Solver*) pSat)->markApprox(v0, v1, nlim);
}
};
////////////////////////////////////////////////////////////////////////
/// END OF FILE ///
////////////////////////////////////////////////////////////////////////

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

@ -613,6 +613,85 @@ inline void Solver::prelocate( int base_var_num ){
polarity .prelocate( base_var_num );
}
inline void Solver::markTill( Var v, int nlim ){
if( var2TravId[v] == travId )
return;
vMarked.push(v);
if( vMarked.size() >= nlim )
return;
if( var2TravId[v] == travId-1 || !isTwoFanin(v) )
goto finalize;
markTill( getFaninVar0(v), nlim );
markTill( getFaninVar1(v), nlim );
finalize:
var2TravId[v] = travId;
}
inline void Solver::markApprox( Var v0, Var v1, int nlim ){
int i;
if( travId <= 1 || nSkipMark>=4 || 0 == nlim )
goto finalize;
vMarked.shrink_( vMarked.size() );
travId ++ ; // travId = t+1
assert(travId>1);
markTill(v0, nlim);
if( vMarked.size() >= nlim )
goto finalize;
markTill(v1, nlim);
if( vMarked.size() >= nlim )
goto finalize;
travId -- ; // travId = t
for(i = 0; i < vMarked.size(); i ++){
var2TravId [ vMarked[i] ] = travId; // set new nodes to time t
var2NodeData[ vMarked[i] ].sort = 0;
}
nSkipMark ++ ;
return;
finalize:
travId ++ ;
nSkipMark = 0;
markCone(v0);
markCone(v1);
}
inline void Solver::loadJust_rec( Var v ){
//assert( value(v) != l_Undef );
if( var2TravId[v] == travId || value(v) == l_Undef )
return;
assert( var2TravId[v] == travId-1 );
var2TravId[v] = travId;
vMarked.push(v);
if( !isTwoFanin(v) ){
JustModel.push( mkLit( v, value(v) == l_False ) );
return;
}
loadJust_rec( getFaninVar0(v) );
loadJust_rec( getFaninVar1(v) );
}
inline void Solver::loadJust(){
int i;
travId ++ ;
JustModel.shrink_(JustModel.size());
vMarked.shrink_(vMarked.size());
JustModel.push(toLit(0));
for(i = 0; i < assumptions.size(); i ++)
loadJust_rec( var(assumptions[i]) );
JustModel[0] = toLit( JustModel.size()-1 );
travId -- ;
for(i = 0; i < vMarked.size(); i ++)
var2TravId[ vMarked[i] ] = travId;
}
};
ABC_NAMESPACE_IMPL_END

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

@ -186,6 +186,7 @@ Solver::Solver() :
itpc = ca.alloc(tmp);
ca[itpc].shrink( ca[itpc].size() );
nSkipMark = 0;
#endif
}
@ -1452,15 +1453,20 @@ printf("c ==================================[ Search Statistics (every %6d confl
if (status == l_True){
if( justUsage() ){
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);
if( nSkipMark ){
loadJust();
} else {
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.shrink_(model.size());
@ -1743,6 +1749,9 @@ void Solver::reset()
itpc = ca.alloc(tmp);
ca[itpc].shrink( ca[itpc].size() );
}
vMarked.shrink_( vMarked.size() );
nSkipMark = 0;
#endif
}

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

@ -453,7 +453,15 @@ protected:
Heap2<JustOrderLt2, JustKey> jheap;
vec<int> jlevel;
vec<int> jnext;
int nSkipMark;
void loadJust_rec( Var v );
void loadJust();
vec<Var> vMarked;
public:
void markTill( Var v0, int nlim );
void markApprox( Var v0, Var v1, int nlim );
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) ); }