diff options
| author | Alan Mishchenko <alanmi@berkeley.edu> | 2015-09-18 08:38:53 -0700 |
|---|---|---|
| committer | Alan Mishchenko <alanmi@berkeley.edu> | 2015-09-18 08:38:53 -0700 |
| commit | fdf00d8044661738aac2eed776520f5511d32607 (patch) | |
| tree | 8608985cfc5cf04d0a4d0b510d28c4e38179ffda /src/sat/cnf | |
| parent | 3b838b953d36c6293af51ddae55ec061e994b4c7 (diff) | |
| download | abc-fdf00d8044661738aac2eed776520f5511d32607.tar.gz abc-fdf00d8044661738aac2eed776520f5511d32607.tar.bz2 abc-fdf00d8044661738aac2eed776520f5511d32607.zip | |
Tuning SAT solver for QBF instances.
Diffstat (limited to 'src/sat/cnf')
| -rw-r--r-- | src/sat/cnf/cnfUtil.c | 16 |
1 files changed, 12 insertions, 4 deletions
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; } |