From dfb065fa553e54fe00891fbeefb866be2c6dfa9d Mon Sep 17 00:00:00 2001 From: Alan Mishchenko Date: Tue, 26 Mar 2013 18:42:47 -0700 Subject: Fixing the dump of SAT solver into a CNF file. --- src/opt/mfs/mfsInter.c | 14 ++++++++++++-- src/sat/bsat/satClause.h | 8 ++++---- src/sat/bsat/satSolver.c | 3 ++- src/sat/bsat/satUtil.c | 24 ++++++++++++------------ 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" : ""); -- cgit v1.2.3