From d0286dce37f7ebda77b2f09d3251f2946c441468 Mon Sep 17 00:00:00 2001 From: Alan Mishchenko Date: Mon, 2 Oct 2017 21:31:34 +0300 Subject: Fixing minimize_assuptions using Glucose. --- src/base/io/ioReadPla.c | 1 + src/sat/glucose/AbcGlucose.cpp | 123 +++++++++++++++++++++++------------------ 2 files changed, 71 insertions(+), 53 deletions(-) diff --git a/src/base/io/ioReadPla.c b/src/base/io/ioReadPla.c index 909ff871..bbce0864 100644 --- a/src/base/io/ioReadPla.c +++ b/src/base/io/ioReadPla.c @@ -503,6 +503,7 @@ Abc_Ntk_t * Io_ReadPlaNetwork( Extra_FileReader_t * p, int fZeros, int fBoth, in printf( "%s (line %d): Input cube length (%d) differs from the number of inputs (%d).\n", Extra_FileReaderGetFileName(p), iLine, (int)strlen(pCubeIn), nInputs ); Abc_NtkDelete( pNtk ); + ABC_FREE( ppSops ); return NULL; } if ( (int)strlen(pCubeOut) != nOutputs ) diff --git a/src/sat/glucose/AbcGlucose.cpp b/src/sat/glucose/AbcGlucose.cpp index 7d56cc56..09f3187f 100644 --- a/src/sat/glucose/AbcGlucose.cpp +++ b/src/sat/glucose/AbcGlucose.cpp @@ -251,46 +251,47 @@ int bmcg_sat_solver_conflictnum(bmcg_sat_solver* s) return ((Gluco::SimpSolver*)s)->conflicts; } -int bmcg_sat_solver_minimize_assumptions(bmcg_sat_solver * s, int * plits, int nlits) +int bmcg_sat_solver_minimize_assumptions( bmcg_sat_solver * s, int * plits, int nlits, int pivot ) { vec*array = &((Gluco::SimpSolver*)s)->user_vec; int i, nlitsL, nlitsR, nresL, nresR, status; - if ( nlits == 1 ) + assert( pivot >= 0 ); +// assert( nlits - pivot >= 2 ); + assert( nlits - pivot >= 1 ); + if ( nlits - pivot == 1 ) { // since the problem is UNSAT, we try to solve it without assuming the last literal // if the result is UNSAT, the last literal can be dropped; otherwise, it is needed - status = bmcg_sat_solver_solve( s, NULL, 0 ); - return status != -1; // return 1 if the problem is not UNSAT + status = bmcg_sat_solver_solve( s, plits, pivot ); + return status != GLUCOSE_UNSAT; // return 1 if the problem is not UNSAT } - assert( nlits >= 2 ); - nlitsL = nlits / 2; - nlitsR = nlits - nlitsL; + assert( nlits - pivot >= 2 ); + nlitsL = (nlits - pivot) / 2; + nlitsR = (nlits - pivot) - nlitsL; + assert( nlitsL + nlitsR == nlits - pivot ); // solve with these assumptions - status = bmcg_sat_solver_solve( s, plits, nlitsL ); - if ( status == -1 ) // these are enough - return bmcg_sat_solver_minimize_assumptions( s, plits, nlitsL ); + status = bmcg_sat_solver_solve( s, plits, pivot + nlitsL ); + if ( status == GLUCOSE_UNSAT ) // these are enough + return bmcg_sat_solver_minimize_assumptions( s, plits, pivot + nlitsL, pivot ); // these are not enough // solve for the right lits -// assume left bits - nresL = nlitsR == 1 ? 1 : bmcg_sat_solver_minimize_assumptions( s, plits + nlitsL, nlitsR ); -// unassume left bits +// nResL = nLitsR == 1 ? 1 : sat_solver_minimize_assumptions( s, pLits + nLitsL, nLitsR, nConfLimit ); + nresL = nlitsR == 1 ? 1 : bmcg_sat_solver_minimize_assumptions( s, plits, nlits, pivot + nlitsL ); // swap literals array->clear(); for ( i = 0; i < nlitsL; i++ ) - array->push(plits[i]); + array->push(plits[pivot + i]); for ( i = 0; i < nresL; i++ ) - plits[i] = plits[nlitsL+i]; + plits[pivot + i] = plits[pivot + nlitsL + i]; for ( i = 0; i < nlitsL; i++ ) - plits[nresL+i] = (*array)[i]; + plits[pivot + nresL + i] = (*array)[i]; // solve with these assumptions -// assume right bits - status = bmcg_sat_solver_solve( s, plits, nresL ); - if ( status == -1 ) // these are enough -// unassume right bits + status = bmcg_sat_solver_solve( s, plits, pivot + nresL ); + if ( status == GLUCOSE_UNSAT ) // these are enough return nresL; // solve for the left lits - nresR = nlitsL == 1 ? 1 : bmcg_sat_solver_minimize_assumptions( s, plits + nresL, nlitsL ); -// unassume right bits +// nResR = nLitsL == 1 ? 1 : sat_solver_minimize_assumptions( s, pLits + nResL, nLitsL, nConfLimit ); + nresR = nlitsL == 1 ? 1 : bmcg_sat_solver_minimize_assumptions( s, plits, pivot + nresL + nlitsL, pivot + nresL ); return nresL + nresR; } @@ -490,46 +491,47 @@ int bmcg_sat_solver_conflictnum(bmcg_sat_solver* s) return ((Gluco::Solver*)s)->conflicts; } -int bmcg_sat_solver_minimize_assumptions(bmcg_sat_solver * s, int * plits, int nlits) +int bmcg_sat_solver_minimize_assumptions( bmcg_sat_solver * s, int * plits, int nlits, int pivot ) { vec*array = &((Gluco::Solver*)s)->user_vec; int i, nlitsL, nlitsR, nresL, nresR, status; - if ( nlits == 1 ) + assert( pivot >= 0 ); +// assert( nlits - pivot >= 2 ); + assert( nlits - pivot >= 1 ); + if ( nlits - pivot == 1 ) { // since the problem is UNSAT, we try to solve it without assuming the last literal // if the result is UNSAT, the last literal can be dropped; otherwise, it is needed - status = bmcg_sat_solver_solve( s, NULL, 0 ); - return status != -1; // return 1 if the problem is not UNSAT + status = bmcg_sat_solver_solve( s, plits, pivot ); + return status != GLUCOSE_UNSAT; // return 1 if the problem is not UNSAT } - assert( nlits >= 2 ); - nlitsL = nlits / 2; - nlitsR = nlits - nlitsL; + assert( nlits - pivot >= 2 ); + nlitsL = (nlits - pivot) / 2; + nlitsR = (nlits - pivot) - nlitsL; + assert( nlitsL + nlitsR == nlits - pivot ); // solve with these assumptions - status = bmcg_sat_solver_solve( s, plits, nlitsL ); - if ( status == -1 ) // these are enough - return bmcg_sat_solver_minimize_assumptions( s, plits, nlitsL ); + status = bmcg_sat_solver_solve( s, plits, pivot + nlitsL ); + if ( status == GLUCOSE_UNSAT ) // these are enough + return bmcg_sat_solver_minimize_assumptions( s, plits, pivot + nlitsL, pivot ); // these are not enough // solve for the right lits -// assume left bits - nresL = nlitsR == 1 ? 1 : bmcg_sat_solver_minimize_assumptions( s, plits + nlitsL, nlitsR ); -// unassume left bits +// nResL = nLitsR == 1 ? 1 : sat_solver_minimize_assumptions( s, pLits + nLitsL, nLitsR, nConfLimit ); + nresL = nlitsR == 1 ? 1 : bmcg_sat_solver_minimize_assumptions( s, plits, nlits, pivot + nlitsL ); // swap literals array->clear(); for ( i = 0; i < nlitsL; i++ ) - array->push(plits[i]); + array->push(plits[pivot + i]); for ( i = 0; i < nresL; i++ ) - plits[i] = plits[nlitsL+i]; + plits[pivot + i] = plits[pivot + nlitsL + i]; for ( i = 0; i < nlitsL; i++ ) - plits[nresL+i] = (*array)[i]; + plits[pivot + nresL + i] = (*array)[i]; // solve with these assumptions -// assume right bits - status = bmcg_sat_solver_solve( s, plits, nresL ); - if ( status == -1 ) // these are enough -// unassume right bits + status = bmcg_sat_solver_solve( s, plits, pivot + nresL ); + if ( status == GLUCOSE_UNSAT ) // these are enough return nresL; // solve for the left lits - nresR = nlitsL == 1 ? 1 : bmcg_sat_solver_minimize_assumptions( s, plits + nresL, nlitsL ); -// unassume right bits +// nResR = nLitsL == 1 ? 1 : sat_solver_minimize_assumptions( s, pLits + nResL, nLitsL, nConfLimit ); + nresR = nlitsL == 1 ? 1 : bmcg_sat_solver_minimize_assumptions( s, plits, pivot + nresL + nlitsL, pivot + nresL ); return nresL + nresR; } @@ -723,11 +725,13 @@ Vec_Int_t * Glucose_SolverFromAig2( Gia_Man_t * p, SimpSolver& S ) ***********************************************************************/ void Glucose_GenerateSop( Gia_Man_t * p ) { + int fCreatePrime = 1; + bmcg_sat_solver * pSat[2] = { bmcg_sat_solver_start(), bmcg_sat_solver_start() }; // generate CNF for the on-set and off-set Cnf_Dat_t * pCnf = (Cnf_Dat_t *)Mf_ManGenerateCnf( p, 8 /*nLutSize*/, 0 /*fCnfObjIds*/, 0/*fAddOrCla*/, 0, 0/*verbose*/ ); - int i,n,nVars = Gia_ManCiNum(p); + int i,n,nVars = Gia_ManCiNum(p), Count = 0; int iFirstVar = pCnf->nVars - nVars; assert( Gia_ManCoNum(p) == 1 ); for ( n = 0; n < 2; n++ ) @@ -744,26 +748,39 @@ void Glucose_GenerateSop( Gia_Man_t * p ) // generate assignments Vec_Int_t * vLits = Vec_IntAlloc( nVars ); Vec_Str_t * vCube = Vec_StrAlloc( nVars + 4 ); + Vec_StrFill( vCube, nVars, '-' ); + Vec_StrPrintF( vCube, " 1\n\0" ); while ( 1 ) { + int * pFinal, nFinal; // generate onset minterm int status = bmcg_sat_solver_solve( pSat[1], NULL, 0 ); - if ( status == -1 ) + if ( status == GLUCOSE_UNSAT ) break; - assert( status == 1 ); + assert( status == GLUCOSE_SAT ); Vec_IntClear( vLits ); for ( i = 0; i < nVars; i++ ) Vec_IntPush( vLits, Abc_Var2Lit(iFirstVar+i, !bmcg_sat_solver_read_cex_varvalue(pSat[1], iFirstVar+i)) ); - // expand it against offset - status = bmcg_sat_solver_solve( pSat[0], Vec_IntArray(vLits), Vec_IntSize(vLits) ); - assert( status == -1 ); - int * pFinal, nFinal = bmcg_sat_solver_final( pSat[0], &pFinal ); + // expand against offset + if ( fCreatePrime ) + { + nFinal = bmcg_sat_solver_minimize_assumptions( pSat[0], Vec_IntArray(vLits), Vec_IntSize(vLits), 0 ); + Vec_IntShrink( vLits, nFinal ); + pFinal = Vec_IntArray( vLits ); + for ( i = 0; i < nFinal; i++ ) + pFinal[i] = Abc_LitNot(pFinal[i]); + } + else + { + status = bmcg_sat_solver_solve( pSat[0], Vec_IntArray(vLits), Vec_IntSize(vLits) ); + assert( status == GLUCOSE_UNSAT ); + nFinal = bmcg_sat_solver_final( pSat[0], &pFinal ); + } // print cube Vec_StrFill( vCube, nVars, '-' ); - Vec_StrPrintF( vCube, " 1\n\0" ); for ( i = 0; i < nFinal; i++ ) Vec_StrWriteEntry( vCube, Abc_Lit2Var(pFinal[i]) - iFirstVar, (char)('0' + Abc_LitIsCompl(pFinal[i])) ); - printf( "%s", Vec_StrArray(vCube) ); + printf( "%4d : %s", Count++, Vec_StrArray(vCube) ); // add blocking clause if ( !bmcg_sat_solver_addclause( pSat[1], pFinal, nFinal ) ) break; -- cgit v1.2.3