From 9e4f8e9fdf45067659f112acc40c5656a38c2a14 Mon Sep 17 00:00:00 2001 From: Alan Mishchenko Date: Fri, 6 Mar 2015 11:01:18 -0800 Subject: Experiments with SAT-based cube enumeration. --- src/sat/bmc/bmcFx.c | 160 +++++++++++++++++++++++++++++++++------------------- 1 file changed, 103 insertions(+), 57 deletions(-) (limited to 'src/sat') diff --git a/src/sat/bmc/bmcFx.c b/src/sat/bmc/bmcFx.c index d1ff16d0..1d3a9802 100644 --- a/src/sat/bmc/bmcFx.c +++ b/src/sat/bmc/bmcFx.c @@ -391,6 +391,7 @@ Vec_Int_t * Div_CubePairs( Vec_Wec_t * p, int nVars, int nDivs ) int Bmc_FxSolve( sat_solver * pSat, int iOut, int iAuxVar, Vec_Int_t * vVars, int fDumpPla, int fVerbose, int * pCounter, Vec_Wec_t * vCubes ) { int nBTLimit = 1000000; + int fUseOrder = 1; Vec_Int_t * vLevel = NULL; Vec_Int_t * vLits = Vec_IntAlloc( Vec_IntSize(vVars) ); Vec_Int_t * vLits2 = Vec_IntAlloc( Vec_IntSize(vVars) ); @@ -417,73 +418,118 @@ int Bmc_FxSolve( sat_solver * pSat, int iOut, int iAuxVar, Vec_Int_t * vVars, in // collect divisor literals Vec_IntClear( vLits ); Vec_IntPush( vLits, Abc_LitNot(pLits[0]) ); // F = 0 - Vec_IntForEachEntryReverse( vVars, iVar, i ) -// Vec_IntForEachEntry( vVars, iVar, i ) +// Vec_IntForEachEntryReverse( vVars, iVar, i ) + Vec_IntForEachEntry( vVars, iVar, i ) Vec_IntPush( vLits, sat_solver_var_literal(pSat, iVar) ); - // check against offset - status = sat_solver_solve( pSat, Vec_IntArray(vLits), Vec_IntArray(vLits) + Vec_IntSize(vLits), nBTLimit, 0, 0, 0 ); - if ( status == l_Undef ) - { RetValue = -1; break; } - if ( status == l_True ) - break; - assert( status == l_False ); - // get subset of literals - nFinal = sat_solver_final( pSat, &pFinal ); - Before = nFinal; - //printf( "Before %d. ", nFinal ); + + if ( fUseOrder ) + { + ////////////////////////////////////////////////////////////// + // save these literals + Vec_IntClear( vLits2 ); + Vec_IntAppend( vLits2, vLits ); + Before = Vec_IntSize(vLits2); + + // try removing literals from the cube + Vec_IntForEachEntry( vLits2, Lit2, k ) + { + if ( Lit2 == Abc_LitNot(pLits[0]) ) + continue; + Vec_IntClear( vLits ); + Vec_IntForEachEntry( vLits2, Lit, n ) + if ( Lit != -1 && Lit != Lit2 ) + Vec_IntPush( vLits, Lit ); + // call sat + status = sat_solver_solve( pSat, Vec_IntArray(vLits), Vec_IntArray(vLits) + Vec_IntSize(vLits), nBTLimit, 0, 0, 0 ); + if ( status == l_Undef ) + assert( 0 ); + if ( status == l_True ) // SAT + continue; + // Lit2 can be removed + Vec_IntWriteEntry( vLits2, k, -1 ); + } + + // make one final run + Vec_IntClear( vLits ); + Vec_IntForEachEntry( vLits2, Lit2, k ) + if ( Lit2 != -1 ) + Vec_IntPush( vLits, Lit2 ); + status = sat_solver_solve( pSat, Vec_IntArray(vLits), Vec_IntArray(vLits) + Vec_IntSize(vLits), nBTLimit, 0, 0, 0 ); + assert( status == l_False ); + + // get subset of literals + nFinal = sat_solver_final( pSat, &pFinal ); + ////////////////////////////////////////////////////////////// + } + else + { + /////////////////////////////////////////////////////////////// + // check against offset + status = sat_solver_solve( pSat, Vec_IntArray(vLits), Vec_IntArray(vLits) + Vec_IntSize(vLits), nBTLimit, 0, 0, 0 ); + if ( status == l_Undef ) + { RetValue = -1; break; } + if ( status == l_True ) + break; + assert( status == l_False ); + // get subset of literals + nFinal = sat_solver_final( pSat, &pFinal ); + Before = nFinal; + //printf( "Before %d. ", nFinal ); /* - // save these literals - Vec_IntClear( vLits ); - for ( i = 0; i < nFinal; i++ ) - Vec_IntPush( vLits, Abc_LitNot(pFinal[i]) ); - Vec_IntReverseOrder( vLits ); + // save these literals + Vec_IntClear( vLits ); + for ( i = 0; i < nFinal; i++ ) + Vec_IntPush( vLits, Abc_LitNot(pFinal[i]) ); + Vec_IntReverseOrder( vLits ); - // make one final run - status = sat_solver_solve( pSat, Vec_IntArray(vLits), Vec_IntArray(vLits) + Vec_IntSize(vLits), nBTLimit, 0, 0, 0 ); - assert( status == l_False ); - nFinal = sat_solver_final( pSat, &pFinal ); + // make one final run + status = sat_solver_solve( pSat, Vec_IntArray(vLits), Vec_IntArray(vLits) + Vec_IntSize(vLits), nBTLimit, 0, 0, 0 ); + assert( status == l_False ); + nFinal = sat_solver_final( pSat, &pFinal ); */ - // save these literals - Vec_IntClear( vLits2 ); - for ( i = 0; i < nFinal; i++ ) - Vec_IntPush( vLits2, Abc_LitNot(pFinal[i]) ); - Vec_IntSort( vLits2, 1 ); + // save these literals + Vec_IntClear( vLits2 ); + for ( i = 0; i < nFinal; i++ ) + Vec_IntPush( vLits2, Abc_LitNot(pFinal[i]) ); + Vec_IntSort( vLits2, 1 ); - // try removing literals from the cube - Vec_IntForEachEntry( vLits2, Lit2, k ) - { - if ( Lit2 == Abc_LitNot(pLits[0]) ) - continue; + // try removing literals from the cube + Vec_IntForEachEntry( vLits2, Lit2, k ) + { + if ( Lit2 == Abc_LitNot(pLits[0]) ) + continue; + Vec_IntClear( vLits ); + Vec_IntForEachEntry( vLits2, Lit, n ) + if ( Lit != -1 && Lit != Lit2 ) + Vec_IntPush( vLits, Lit ); + // call sat + status = sat_solver_solve( pSat, Vec_IntArray(vLits), Vec_IntArray(vLits) + Vec_IntSize(vLits), nBTLimit, 0, 0, 0 ); + if ( status == l_Undef ) + assert( 0 ); + if ( status == l_True ) // SAT + continue; + // Lit2 can be removed + Vec_IntWriteEntry( vLits2, k, -1 ); + } + + // make one final run Vec_IntClear( vLits ); - Vec_IntForEachEntry( vLits2, Lit, n ) - if ( Lit != -1 && Lit != Lit2 ) - Vec_IntPush( vLits, Lit ); - // call sat + Vec_IntForEachEntry( vLits2, Lit2, k ) + if ( Lit2 != -1 ) + Vec_IntPush( vLits, Lit2 ); status = sat_solver_solve( pSat, Vec_IntArray(vLits), Vec_IntArray(vLits) + Vec_IntSize(vLits), nBTLimit, 0, 0, 0 ); - if ( status == l_Undef ) - assert( 0 ); - if ( status == l_True ) // SAT - continue; - // Lit2 can be removed - Vec_IntWriteEntry( vLits2, k, -1 ); + assert( status == l_False ); + + // put them back + nFinal = 0; + Vec_IntForEachEntry( vLits2, Lit2, k ) + if ( Lit2 != -1 ) + pFinal[nFinal++] = Abc_LitNot(Lit2); + ///////////////////////////////////////////////////////// } - // make one final run - Vec_IntClear( vLits ); - Vec_IntForEachEntry( vLits2, Lit2, k ) - if ( Lit2 != -1 ) - Vec_IntPush( vLits, Lit2 ); - status = sat_solver_solve( pSat, Vec_IntArray(vLits), Vec_IntArray(vLits) + Vec_IntSize(vLits), nBTLimit, 0, 0, 0 ); - assert( status == l_False ); - - // put them back - nFinal = 0; - Vec_IntForEachEntry( vLits2, Lit2, k ) - if ( Lit2 != -1 ) - pFinal[nFinal++] = Abc_LitNot(Lit2); - //printf( "After %d. \n", nFinal ); After = nFinal; @@ -628,7 +674,7 @@ int Bmc_FxComputeOne( Gia_Man_t * p ) { int Extra = 1000; int nIterMax = 5; - int nDiv2Add = 16; + int nDiv2Add = 15; // create SAT solver Cnf_Dat_t * pCnf = Mf_ManGenerateCnf( p, 8, 0, 0, 0 ); sat_solver * pSat = (sat_solver *)Cnf_DataWriteIntoSolver( pCnf, 1, 0 ); -- cgit v1.2.3