luke
/
abc
mirror of https://github.com/YosysHQ/abc.git
1
0
Fork 0
Code Issues Packages Projects Releases Wiki Activity

Adding support of candinality clause to the SAT solver.

This commit is contained in:
Alan Mishchenko 2016-01-10 10:19:26 -08:00
parent a4f9776388
commit d6178631be
5 changed files with 52 additions and 7 deletions
Show Stats Download Patch File Download Diff File Expand all files Collapse all files

10
src/base/abci/abc.c
View File

@ -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 );

25
src/sat/bsat/satSolver.c
View File

@ -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

11
src/sat/bsat/satSolver.h
View File

@ -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];

2
src/sat/bsat/satUtil.c
View File

@ -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 );

11
src/sat/cnf/cnfUtil.c
View File

@ -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;