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

Tuning SAT solver for QBF instances.

This commit is contained in:
Alan Mishchenko 2015-09-18 08:38:53 -07:00
parent 3b838b953d
commit fdf00d8044
3 changed files with 22 additions and 12 deletions
Show Stats Download Patch File Download Diff File Expand all files Collapse all files

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

@ -21829,7 +21829,7 @@ int Abc_CommandDSat( Abc_Frame_t * pAbc, int argc, char ** argv )
if ( argc == globalUtilOptind + 1 )
{
int * pModel = NULL;
extern int Cnf_DataSolveFromFile( char * pFileName, int nConfLimit, int nLearnedStart, int nLearnedDelta, int nLearnedPerce, int fVerbose, int ** ppModel );
extern int Cnf_DataSolveFromFile( char * pFileName, int nConfLimit, int nLearnedStart, int nLearnedDelta, int nLearnedPerce, int fVerbose, int ** ppModel, int nPis );
// get the input file name
char * pFileName = argv[globalUtilOptind];
FILE * pFile = fopen( pFileName, "rb" );
@ -21839,14 +21839,14 @@ int Abc_CommandDSat( Abc_Frame_t * pAbc, int argc, char ** argv )
return 0;
}
fclose( pFile );
Cnf_DataSolveFromFile( pFileName, nConfLimit, nLearnedStart, nLearnedDelta, nLearnedPerce, fVerbose, &pModel );
Cnf_DataSolveFromFile( pFileName, nConfLimit, nLearnedStart, nLearnedDelta, nLearnedPerce, fVerbose, &pModel, Abc_NtkPiNum(pNtk) );
if ( pModel && pNtk )
{
int * pSimInfo = Abc_NtkVerifySimulatePattern( pNtk, pModel );
if ( pSimInfo[0] != 1 )
Abc_Print( 1, "ERROR in Abc_NtkMiterSat(): Generated counter example is invalid.\n" );
Abc_Print( 1, "ERROR in mapping PIs into SAT vars: Generated CEX is invalid.\n" );
ABC_FREE( pSimInfo );
pAbc->pCex = Abc_CexCreate( 0, Abc_NtkPiNum(pNtk), pNtk->pModel, 0, 0, 0 );
pAbc->pCex = Abc_CexCreate( 0, Abc_NtkPiNum(pNtk), pModel, 0, 0, 0 );
}
ABC_FREE( pModel );
return 0;

10
src/sat/bsat/satUtil.c
View File

@ -185,13 +185,15 @@ void Sat_Solver2WriteDimacs( sat_solver2 * p, char * pFileName, lit* assumpBegin
SeeAlso []
***********************************************************************/
static inline double Sat_Wrd2Dbl( word w ) { return (double)(unsigned)(w&0x3FFFFFFF) + (double)(1<<30)*(unsigned)(w>>30); }
void Sat_SolverPrintStats( FILE * pFile, sat_solver * p )
{
// printf( "calls : %10d (%d)\n", (int)p->nCalls, (int)p->nCalls2 );
printf( "starts : %10d\n", (int)p->stats.starts );
printf( "conflicts : %10d\n", (int)p->stats.conflicts );
printf( "decisions : %10d\n", (int)p->stats.decisions );
printf( "propagations : %10d\n", (int)p->stats.propagations );
printf( "starts : %16.0f\n", Sat_Wrd2Dbl(p->stats.starts) );
printf( "conflicts : %16.0f\n", Sat_Wrd2Dbl(p->stats.conflicts) );
printf( "decisions : %16.0f\n", Sat_Wrd2Dbl(p->stats.decisions) );
printf( "propagations : %16.0f\n", Sat_Wrd2Dbl(p->stats.propagations) );
// printf( "inspects : %10d\n", (int)p->stats.inspects );
// printf( "inspects2 : %10d\n", (int)p->stats.inspects2 );
}

16
src/sat/cnf/cnfUtil.c
View File

@ -399,12 +399,12 @@ finish:
SeeAlso []
***********************************************************************/
int Cnf_DataSolveFromFile( char * pFileName, int nConfLimit, int nLearnedStart, int nLearnedDelta, int nLearnedPerce, int fVerbose, int ** ppModel )
int Cnf_DataSolveFromFile( char * pFileName, int nConfLimit, int nLearnedStart, int nLearnedDelta, int nLearnedPerce, int fVerbose, int ** ppModel, int nPis )
{
abctime clk = Abc_Clock();
Cnf_Dat_t * pCnf = Cnf_DataReadFromFile( pFileName );
sat_solver * pSat;
int status, RetValue = -1;
int i, status, RetValue = -1;
if ( pCnf == NULL )
return -1;
if ( fVerbose )
@ -414,10 +414,10 @@ int Cnf_DataSolveFromFile( char * pFileName, int nConfLimit, int nLearnedStart,
}
// convert into SAT solver
pSat = (sat_solver *)Cnf_DataWriteIntoSolver( pCnf, 1, 0 );
Cnf_DataFree( pCnf );
if ( pSat == NULL )
{
printf( "The problem is trivially UNSAT.\n" );
Cnf_DataFree( pCnf );
return 1;
}
if ( nLearnedStart )
@ -440,7 +440,6 @@ int Cnf_DataSolveFromFile( char * pFileName, int nConfLimit, int nLearnedStart,
assert( 0 );
if ( fVerbose )
Sat_SolverPrintStats( stdout, pSat );
sat_solver_delete( pSat );
if ( RetValue == -1 )
Abc_Print( 1, "UNDECIDED " );
else if ( RetValue == 0 )
@ -449,6 +448,15 @@ int Cnf_DataSolveFromFile( char * pFileName, int nConfLimit, int nLearnedStart,
Abc_Print( 1, "UNSATISFIABLE " );
//Abc_Print( -1, "\n" );
Abc_PrintTime( 1, "Time", Abc_Clock() - clk );
// derive SAT assignment
if ( RetValue == 0 )
{
*ppModel = ABC_ALLOC( int, nPis );
for ( i = 0; i < nPis; i++ )
(*ppModel)[i] = sat_solver_var_value( pSat, pCnf->nVars - nPis + i );
}
Cnf_DataFree( pCnf );
sat_solver_delete( pSat );
return RetValue;
}