Fixing the dump of SAT solver into a CNF file.

4 files changed, 30 insertions, 19 deletions

diff --git a/src/opt/mfs/mfsInter.c b/src/opt/mfs/mfsInter.c
index 812e22cf..5e97f0b3 100644
--- a/src/opt/mfs/mfsInter.c
+++ b/src/opt/mfs/mfsInter.c
@@ -329,7 +329,8 @@ int Abc_NtkMfsInterplateEval( Mfs_Man_t * p, int * pCands, int nCands )
 Hop_Obj_t * Abc_NtkMfsInterplate( Mfs_Man_t * p, int * pCands, int nCands )
 {
     extern Hop_Obj_t * Kit_GraphToHop( Hop_Man_t * pMan, Kit_Graph_t * pGraph );
-
+    int fDumpFile = 0;
+    char FileName[32];
     sat_solver * pSat;
     Sto_Man_t * pCnf = NULL;
     unsigned * puTruth;
@@ -338,14 +339,23 @@ Hop_Obj_t * Abc_NtkMfsInterplate( Mfs_Man_t * p, int * pCands, int nCands )
     int nFanins, status;
     int c, i, * pGloVars;
 //    clock_t clk = clock();
-
 //    p->nDcMints += Abc_NtkMfsInterplateEval( p, pCands, nCands );
 
     // derive the SAT solver for interpolation
     pSat = Abc_MfsCreateSolverResub( p, pCands, nCands, 0 );
 
+    // dump CNF file (remember to uncomment two-lit clases in clause_create_new() in 'satSolver.c')
+    if ( fDumpFile )
+    {
+        static int Counter = 0;
+        sprintf( FileName, "cnf\\pj1_if6_mfs%03d.cnf", Counter++ );
+        Sat_SolverWriteDimacs( pSat, FileName, NULL, NULL, 1 );
+    }
+
     // solve the problem
     status = sat_solver_solve( pSat, NULL, NULL, (ABC_INT64_T)p->pPars->nBTLimit, (ABC_INT64_T)0, (ABC_INT64_T)0, (ABC_INT64_T)0 );
+    if ( fDumpFile )
+        printf( "File %s has UNSAT problem with %d conflicts.\n", FileName, (int)pSat->stats.conflicts );
     if ( status != l_False )
     {
         p->nTimeOuts++;
diff --git a/src/sat/bsat/satClause.h b/src/sat/bsat/satClause.h
index c40e5f18..0b1756ff 100644
--- a/src/sat/bsat/satClause.h
+++ b/src/sat/bsat/satClause.h
@@ -113,15 +113,15 @@ static inline double    Sat_MemMemoryAll( Sat_Mem_t * p )            { return 1.
 // i is page number
 // k is page offset
 
-// print problelm clauses NOT in proof mode
+// print problem clauses NOT in proof mode
 #define Sat_MemForEachClause( p, c, i, k )      \
     for ( i = 0; i <= p->iPage[0]; i += 2 )     \
-        for ( k = 2; k < Sat_MemLimit(p->pPages[i]) && ((c) = Sat_MemClause( p, i, k )); k += Sat_MemClauseSize(c) )
+        for ( k = 2; k < Sat_MemLimit(p->pPages[i]) && ((c) = Sat_MemClause( p, i, k )); k += Sat_MemClauseSize(c) ) if ( i == 0 && k == 2 ) {} else
 
-// print problem clauses in proof model
+// print problem clauses in proof mode
 #define Sat_MemForEachClause2( p, c, i, k )      \
     for ( i = 0; i <= p->iPage[0]; i += 2 )     \
-        for ( k = 2; k < Sat_MemLimit(p->pPages[i]) && ((c) = Sat_MemClause( p, i, k )); k += Sat_MemClauseSize2(c) )
+        for ( k = 2; k < Sat_MemLimit(p->pPages[i]) && ((c) = Sat_MemClause( p, i, k )); k += Sat_MemClauseSize2(c) ) if ( i == 0 && k == 2 ) {} else
 
 #define Sat_MemForEachLearned( p, c, i, k )     \
     for ( i = 1; i <= p->iPage[1]; i += 2 )     \
diff --git a/src/sat/bsat/satSolver.c b/src/sat/bsat/satSolver.c
index 0e5c6b91..ab1203ea 100644
--- a/src/sat/bsat/satSolver.c
+++ b/src/sat/bsat/satSolver.c
@@ -401,6 +401,7 @@ static inline int sat_clause_compute_lbd( sat_solver* s, clause* c )
  */
 static int clause_create_new(sat_solver* s, lit* begin, lit* end, int learnt)
 {
+    int fUseBinaryClauses = 1;
     int size;
     clause* c;
     int h;
@@ -410,7 +411,7 @@ static int clause_create_new(sat_solver* s, lit* begin, lit* end, int learnt)
     size           = end - begin;
 
     // do not allocate memory for the two-literal problem clause
-    if ( size == 2 && !learnt )
+    if ( fUseBinaryClauses && size == 2 && !learnt )
     {
         veci_push(sat_solver_read_wlist(s,lit_neg(begin[0])),(clause_from_lit(begin[1])));
         veci_push(sat_solver_read_wlist(s,lit_neg(begin[1])),(clause_from_lit(begin[0])));
diff --git a/src/sat/bsat/satUtil.c b/src/sat/bsat/satUtil.c
index 59eb047d..dc431440 100644
--- a/src/sat/bsat/satUtil.c
+++ b/src/sat/bsat/satUtil.c
@@ -78,7 +78,7 @@ void Sat_SolverWriteDimacs( sat_solver * p, char * pFileName, lit* assumpBegin,
     // count the number of unit clauses
     nUnits = 0;
     for ( i = 0; i < p->size; i++ )
-        if ( p->levels[i] == 0 && p->assigns[i] != l_Undef )
+        if ( p->levels[i] == 0 && p->assigns[i] != 3 )
             nUnits++;
 
     // start the file
@@ -89,21 +89,21 @@ void Sat_SolverWriteDimacs( sat_solver * p, char * pFileName, lit* assumpBegin,
         return;
     }
 //    fprintf( pFile, "c CNF generated by ABC on %s\n", Extra_TimeStamp() );
-    fprintf( pFile, "p cnf %d %d\n", p->size, Sat_MemEntryNum(&p->Mem, 0)+Sat_MemEntryNum(&p->Mem, 1)+nUnits+(int)(assumpEnd-assumpBegin) );
+    fprintf( pFile, "p cnf %d %d\n", p->size, Sat_MemEntryNum(&p->Mem, 0)-1+Sat_MemEntryNum(&p->Mem, 1)+nUnits+(int)(assumpEnd-assumpBegin) );
 
     // write the original clauses
     Sat_MemForEachClause( pMem, c, i, k )
         Sat_SolverClauseWriteDimacs( pFile, c, incrementVars );
 
     // write the learned clauses
-    Sat_MemForEachLearned( pMem, c, i, k )
-        Sat_SolverClauseWriteDimacs( pFile, c, incrementVars );
+//    Sat_MemForEachLearned( pMem, c, i, k )
+//        Sat_SolverClauseWriteDimacs( pFile, c, incrementVars );
 
     // write zero-level assertions
     for ( i = 0; i < p->size; i++ )
-        if ( p->levels[i] == 0 && p->assigns[i] != l_Undef )
+        if ( p->levels[i] == 0 && p->assigns[i] != 3 ) // varX
             fprintf( pFile, "%s%d%s\n",
-                     (p->assigns[i] == l_False)? "-": "",
+                     (p->assigns[i] == 1)? "-": "",    // var0
                      i + (int)(incrementVars>0),
                      (incrementVars) ? " 0" : "");
 
@@ -130,7 +130,7 @@ void Sat_Solver2WriteDimacs( sat_solver2 * p, char * pFileName, lit* assumpBegin
     // count the number of unit clauses
     nUnits = 0;
     for ( i = 0; i < p->size; i++ )
-        if ( p->levels[i] == 0 && p->assigns[i] != l_Undef )
+        if ( p->levels[i] == 0 && p->assigns[i] != 3 )
             nUnits++;
 
     // start the file
@@ -141,21 +141,21 @@ void Sat_Solver2WriteDimacs( sat_solver2 * p, char * pFileName, lit* assumpBegin
         return;
     }
 //    fprintf( pFile, "c CNF generated by ABC on %s\n", Extra_TimeStamp() );
-    fprintf( pFile, "p cnf %d %d\n", p->size, Sat_MemEntryNum(&p->Mem, 0)+Sat_MemEntryNum(&p->Mem, 1)+nUnits+(int)(assumpEnd-assumpBegin) );
+    fprintf( pFile, "p cnf %d %d\n", p->size, Sat_MemEntryNum(&p->Mem, 0)-1+Sat_MemEntryNum(&p->Mem, 1)+nUnits+(int)(assumpEnd-assumpBegin) );
 
     // write the original clauses
     Sat_MemForEachClause2( pMem, c, i, k )
         Sat_SolverClauseWriteDimacs( pFile, c, incrementVars );
 
     // write the learned clauses
-    Sat_MemForEachLearned( pMem, c, i, k )
-        Sat_SolverClauseWriteDimacs( pFile, c, incrementVars );
+//    Sat_MemForEachLearned( pMem, c, i, k )
+//        Sat_SolverClauseWriteDimacs( pFile, c, incrementVars );
 
     // write zero-level assertions
     for ( i = 0; i < p->size; i++ )
-        if ( p->levels[i] == 0 && p->assigns[i] != l_Undef )
+        if ( p->levels[i] == 0 && p->assigns[i] != 3 ) // varX
             fprintf( pFile, "%s%d%s\n",
-                     (p->assigns[i] == l_False)? "-": "",
+                     (p->assigns[i] == 1)? "-": "",    // var0
                      i + (int)(incrementVars>0),
                      (incrementVars) ? " 0" : "");