From fdf00d8044661738aac2eed776520f5511d32607 Mon Sep 17 00:00:00 2001 From: Alan Mishchenko Date: Fri, 18 Sep 2015 08:38:53 -0700 Subject: Tuning SAT solver for QBF instances. --- src/sat/bsat/satUtil.c | 10 ++++++---- src/sat/cnf/cnfUtil.c | 16 ++++++++++++---- 2 files changed, 18 insertions(+), 8 deletions(-) (limited to 'src/sat') diff --git a/src/sat/bsat/satUtil.c b/src/sat/bsat/satUtil.c index dc431440..d782386e 100644 --- a/src/sat/bsat/satUtil.c +++ b/src/sat/bsat/satUtil.c @@ -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 ); } diff --git a/src/sat/cnf/cnfUtil.c b/src/sat/cnf/cnfUtil.c index 7900b08c..a5037718 100644 --- a/src/sat/cnf/cnfUtil.c +++ b/src/sat/cnf/cnfUtil.c @@ -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; } -- cgit v1.2.3