From d6178631be82089dc65263cd10293211abad5924 Mon Sep 17 00:00:00 2001 From: Alan Mishchenko Date: Sun, 10 Jan 2016 10:19:26 -0800 Subject: Adding support of candinality clause to the SAT solver. --- src/base/abci/abc.c | 10 +++++++--- src/sat/bsat/satSolver.c | 25 +++++++++++++++++++++++-- src/sat/bsat/satSolver.h | 11 ++++++++++- src/sat/bsat/satUtil.c | 2 ++ src/sat/cnf/cnfUtil.c | 11 ++++++++++- 5 files changed, 52 insertions(+), 7 deletions(-) (limited to 'src') diff --git a/src/base/abci/abc.c b/src/base/abci/abc.c index afa166fc..1b2e1e2c 100644 --- a/src/base/abci/abc.c +++ b/src/base/abci/abc.c @@ -22075,6 +22075,7 @@ int Abc_CommandDSat( Abc_Frame_t * pAbc, int argc, char ** argv ) int fAndOuts; int fNewSolver; int fSilent; + int fShowPattern; int fVerbose; int nConfLimit; int nLearnedStart; @@ -22096,7 +22097,7 @@ int Abc_CommandDSat( Abc_Frame_t * pAbc, int argc, char ** argv ) nLearnedDelta = 0; nLearnedPerce = 0; Extra_UtilGetoptReset(); - while ( ( c = Extra_UtilGetopt( argc, argv, "CILDEpansvh" ) ) != EOF ) + while ( ( c = Extra_UtilGetopt( argc, argv, "CILDEpansvwh" ) ) != EOF ) { switch ( c ) { @@ -22170,6 +22171,9 @@ int Abc_CommandDSat( Abc_Frame_t * pAbc, int argc, char ** argv ) case 'v': fVerbose ^= 1; break; + case 'w': + fShowPattern ^= 1; + break; case 'h': goto usage; default: @@ -22180,7 +22184,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, int nPis ); + extern int Cnf_DataSolveFromFile( char * pFileName, int nConfLimit, int nLearnedStart, int nLearnedDelta, int nLearnedPerce, int fVerbose, int fShowPattern, int ** ppModel, int nPis ); // get the input file name char * pFileName = argv[globalUtilOptind]; FILE * pFile = fopen( pFileName, "rb" ); @@ -22190,7 +22194,7 @@ int Abc_CommandDSat( Abc_Frame_t * pAbc, int argc, char ** argv ) return 0; } fclose( pFile ); - Cnf_DataSolveFromFile( pFileName, nConfLimit, nLearnedStart, nLearnedDelta, nLearnedPerce, fVerbose, &pModel, pNtk ? Abc_NtkPiNum(pNtk) : 0 ); + Cnf_DataSolveFromFile( pFileName, nConfLimit, nLearnedStart, nLearnedDelta, nLearnedPerce, fVerbose, fShowPattern, &pModel, pNtk ? Abc_NtkPiNum(pNtk) : 0 ); if ( pModel && pNtk ) { int * pSimInfo = Abc_NtkVerifySimulatePattern( pNtk, pModel ); diff --git a/src/sat/bsat/satSolver.c b/src/sat/bsat/satSolver.c index 24c60dac..1a10ff88 100644 --- a/src/sat/bsat/satSolver.c +++ b/src/sat/bsat/satSolver.c @@ -508,6 +508,12 @@ static inline int sat_solver_enqueue(sat_solver* s, lit l, int from) s->reasons[v] = from; s->trail[s->qtail++] = l; order_assigned(s, v); + // if cardinality clause is present, add positive literals + if ( s->cardinality && !lit_sign(l) && s->nCard >= (int)s->cardinality->size ) + { +//printf( "setting trail[%d] = %d\n", s->qtail-1, l ); + s->cardinality->lits[s->nCard - s->cardinality->size++] = lit_neg(l); + } return true; } } @@ -549,7 +555,15 @@ static void sat_solver_canceluntil(sat_solver* s, int level) { s->reasons[x] = 0; if ( c < lastLev ) var_set_polar( s, x, !lit_sign(s->trail[c]) ); + // if cardinality clause is present, remove positive + if ( s->cardinality && s->cardinality->lits[s->nCard+1 - s->cardinality->size] == lit_neg(s->trail[c]) ) + { +//printf( "undoing trail[%d] = %d\n", c, s->trail[c] ); + assert( s->cardinality->size > 0 ); + s->cardinality->size--; + } } + //printf( "\n" ); for (c = s->qhead-1; c >= bound; c--) order_unassigned(s,lit_var(s->trail[c])); @@ -781,7 +795,7 @@ static void sat_solver_analyze(sat_solver* s, int h, veci* learnt) lit p = lit_Undef; int ind = s->qtail-1; lit* lits; - int i, j, minl; + int i, j, minl;// int hTemp = h; veci_push(learnt,lit_Undef); do{ assert(h != 0); @@ -796,7 +810,8 @@ static void sat_solver_analyze(sat_solver* s, int h, veci* learnt) veci_push(learnt,clause_read_lit(h)); } }else{ - clause* c = clause_read(s, h); + clause* c = h == -2 ? s->cardinality : clause_read(s, h); + if (clause_learnt(c)) act_clause_bump(s,c); lits = clause_begin(c); @@ -878,6 +893,8 @@ static void sat_solver_analyze(sat_solver* s, int h, veci* learnt) printf(" } at level %d\n", lev); } #endif +// if ( hTemp == -2 ) +// printf( "%d ", veci_size(learnt) ); } //#define TEST_CNF_LOAD @@ -1183,6 +1200,7 @@ void sat_solver_delete(sat_solver* s) } sat_solver_store_free(s); + ABC_FREE(s->cardinality); ABC_FREE(s); } @@ -1616,6 +1634,8 @@ static lbool sat_solver_search(sat_solver* s, ABC_INT64_T nof_conflicts) for (;;){ int hConfl = sat_solver_propagate(s); + if ( hConfl == 0 && s->cardinality && (int)s->cardinality->size == s->nCard+1 ) + hConfl = -2, s->nCardClauses++; if (hConfl != 0){ // CONFLICT int blevel; @@ -1898,6 +1918,7 @@ int sat_solver_solve(sat_solver* s, lit* begin, lit* end, ABC_INT64_T nConfLimit fflush(stdout); } nof_conflicts = (ABC_INT64_T)( 100 * luby(2, restart_iter++) ); +// assert( s->cardinality->size == 0 ); status = sat_solver_search(s, nof_conflicts); // nof_learnts = nof_learnts * 11 / 10; //*= 1.1; // quit the loop if reached an external limit diff --git a/src/sat/bsat/satSolver.h b/src/sat/bsat/satSolver.h index 89391d2d..f1738eb5 100644 --- a/src/sat/bsat/satSolver.h +++ b/src/sat/bsat/satSolver.h @@ -100,6 +100,9 @@ struct sat_solver_t int hLearnts; // the first learnt clause int hBinary; // the special binary clause clause * binary; + clause * cardinality; // cardinality clause + int nCard; // cardinality size + int nCardClauses; // cardinality conflicts veci* wlists; // watcher lists veci act_clas; // contain clause activities @@ -291,7 +294,13 @@ static inline int sat_solver_count_usedvars(sat_solver* s) } return nVars; } - +static inline void sat_solver_start_cardinality(sat_solver* s, int nSize) +{ + assert( s->cardinality == NULL ); + s->cardinality = (clause*)ABC_CALLOC(int, nSize+2); + s->nCard = nSize; + s->nCardClauses = 0; +} static inline int sat_solver_add_const( sat_solver * pSat, int iVar, int fCompl ) { lit Lits[1]; diff --git a/src/sat/bsat/satUtil.c b/src/sat/bsat/satUtil.c index f1f03ce2..188c308b 100644 --- a/src/sat/bsat/satUtil.c +++ b/src/sat/bsat/satUtil.c @@ -195,6 +195,8 @@ void Sat_SolverPrintStats( FILE * pFile, sat_solver * p ) // printf( "calls : %10d (%d)\n", (int)p->nCalls, (int)p->nCalls2 ); printf( "starts : %16.0f\n", Sat_Wrd2Dbl(p->stats.starts) ); printf( "conflicts : %16.0f\n", Sat_Wrd2Dbl(p->stats.conflicts) ); + if ( p->nCardClauses ) + printf( "conflictsCard : %16.0f\n", Sat_Wrd2Dbl((word)p->nCardClauses) ); 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 ); diff --git a/src/sat/cnf/cnfUtil.c b/src/sat/cnf/cnfUtil.c index 73bcd8a1..96002df8 100644 --- a/src/sat/cnf/cnfUtil.c +++ b/src/sat/cnf/cnfUtil.c @@ -399,7 +399,7 @@ finish: SeeAlso [] ***********************************************************************/ -int Cnf_DataSolveFromFile( char * pFileName, int nConfLimit, int nLearnedStart, int nLearnedDelta, int nLearnedPerce, int fVerbose, int ** ppModel, int nPis ) +int Cnf_DataSolveFromFile( char * pFileName, int nConfLimit, int nLearnedStart, int nLearnedDelta, int nLearnedPerce, int fVerbose, int fShowPattern, int ** ppModel, int nPis ) { abctime clk = Abc_Clock(); Cnf_Dat_t * pCnf = Cnf_DataReadFromFile( pFileName ); @@ -428,6 +428,9 @@ int Cnf_DataSolveFromFile( char * pFileName, int nConfLimit, int nLearnedStart, pSat->nLearntRatio = nLearnedPerce; if ( fVerbose ) pSat->fVerbose = fVerbose; + +//sat_solver_start_cardinality( pSat, 100 ); + // solve the miter status = sat_solver_solve( pSat, NULL, NULL, (ABC_INT64_T)nConfLimit, 0, (ABC_INT64_T)0, (ABC_INT64_T)0 ); if ( status == l_Undef ) @@ -455,6 +458,12 @@ int Cnf_DataSolveFromFile( char * pFileName, int nConfLimit, int nLearnedStart, for ( i = 0; i < nPis; i++ ) (*ppModel)[i] = sat_solver_var_value( pSat, pCnf->nVars - nPis + i ); } + if ( RetValue == 0 && fShowPattern ) + { + for ( i = 0; i < pCnf->nVars; i++ ) + printf( "%d", sat_solver_var_value(pSat,i) ); + printf( "\n" ); + } Cnf_DataFree( pCnf ); sat_solver_delete( pSat ); return RetValue; -- cgit v1.2.3