Tuning SAT solver for QBF instances.

3 files changed, 22 insertions, 12 deletions

diff --git a/src/base/abci/abc.c b/src/base/abci/abc.c
index 47da5723..0fb139d3 100644
--- a/src/base/abci/abc.c
+++ b/src/base/abci/abc.c
@@ -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;
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;
 }