From e50fc467fd54420cf262bf5266959f6c02a65bf7 Mon Sep 17 00:00:00 2001 From: Alan Mishchenko Date: Fri, 6 Nov 2015 13:49:23 -0800 Subject: Improvements to 'satclp' (unfinished). --- src/sat/bmc/bmcClp.c | 217 ++++++++++++++++++++++++++++++++++++++------------- 1 file changed, 163 insertions(+), 54 deletions(-) (limited to 'src/sat') diff --git a/src/sat/bmc/bmcClp.c b/src/sat/bmc/bmcClp.c index 57138fce..fbff7679 100644 --- a/src/sat/bmc/bmcClp.c +++ b/src/sat/bmc/bmcClp.c @@ -396,17 +396,17 @@ int Bmc_CollapseExpandRound( sat_solver * pSat, sat_solver * pSatOn, Vec_Int_t * Vec_IntWriteEntry( vLits, k, -1 ); // put into new array Vec_IntClear( vTemp ); + if ( fOnOffSetLit >= 0 ) + Vec_IntPush( vTemp, fOnOffSetLit ); Vec_IntForEachEntry( vLits, iLit, n ) if ( iLit != -1 ) Vec_IntPush( vTemp, iLit ); // check against offset - if ( fOnOffSetLit >= 0 ) - Vec_IntPush( vTemp, fOnOffSetLit ); if ( fProfile ) clk = Abc_Clock(); status = sat_solver_solve( pSat, Vec_IntArray(vTemp), Vec_IntLimit(vTemp), nBTLimit, 0, 0, 0 ); if ( fProfile ) clkCheck2 += Abc_Clock() - clk; - if ( fOnOffSetLit >= 0 ) - Vec_IntPop( vTemp ); +// if ( fOnOffSetLit >= 0 ) +// Vec_IntPop( vTemp ); if ( status == l_Undef ) return -1; if ( status == l_True ) @@ -477,6 +477,105 @@ int Bmc_CollapseExpand( sat_solver * pSat, sat_solver * pSatOn, Vec_Int_t * vLit return 0; } +int Bmc_CollapseExpand2( sat_solver * pSat, sat_solver * pSatOn, Vec_Int_t * vLits, Vec_Int_t * vNums, Vec_Int_t * vTemp, int nBTLimit, int fCanon, int fOnOffSetLit ) +{ + // perform one quick reduction if it is non-canonical + if ( !fCanon ) + { + int i, k, iLit, j, iNum, status, nFinal, * pFinal; + + // check against offset + if ( fOnOffSetLit >= 0 ) + Vec_IntPush( vLits, fOnOffSetLit ); + status = sat_solver_solve( pSat, Vec_IntArray(vLits), Vec_IntLimit(vLits), nBTLimit, 0, 0, 0 ); + if ( fOnOffSetLit >= 0 ) + Vec_IntPop( vLits ); + if ( status == l_Undef ) + return -1; + assert( status == l_False ); + + // get subset of literals + nFinal = sat_solver_final( pSat, &pFinal ); + Vec_IntClear( vNums ); + Vec_IntClear( vTemp ); + if ( fOnOffSetLit >= 0 ) + { + //Vec_IntPush( vNums, -1 ); + Vec_IntPush( vTemp, fOnOffSetLit ); + } + Vec_IntForEachEntry( vLits, iLit, i ) + { + for ( k = 0; k < nFinal; k++ ) + if ( iLit == Abc_LitNot(pFinal[k]) ) + break; + if ( k == nFinal ) + continue; + Vec_IntPush( vNums, i ); + Vec_IntPush( vTemp, iLit ); + } + + // check against offset + status = sat_solver_solve( pSat, Vec_IntArray(vTemp), Vec_IntLimit(vTemp), nBTLimit, 0, 0, 0 ); + if ( status == l_Undef ) + return -1; + assert( status == l_False ); + + // get subset of literals + nFinal = sat_solver_final( pSat, &pFinal ); + j = 0; + Vec_IntForEachEntry( vTemp, iLit, i ) + { + if ( iLit == fOnOffSetLit ) + continue; + for ( k = 0; k < nFinal; k++ ) + if ( iLit == Abc_LitNot(pFinal[k]) ) + break; + if ( k == nFinal ) + continue; + Vec_IntWriteEntry( vNums, j++, Vec_IntEntry(vNums, i) ); + } + Vec_IntShrink( vNums, j ); + + + // try removing each literal + for ( i = 0; i < Vec_IntSize(vNums); i++ ) + { + Vec_IntClear( vTemp ); + if ( fOnOffSetLit >= 0 ) + Vec_IntPush( vTemp, fOnOffSetLit ); + Vec_IntForEachEntry( vNums, iNum, k ) + if ( k != i ) + Vec_IntPush( vTemp, Vec_IntEntry(vLits, iNum) ); + // check against offset + status = sat_solver_solve( pSat, Vec_IntArray(vTemp), Vec_IntLimit(vTemp), nBTLimit, 0, 0, 0 ); + if ( status == l_Undef ) + return -1; + if ( status == l_True ) + continue; + // remove literal + Vec_IntDrop( vNums, i ); + i--; + } + } + else + { + Bmc_CollapseExpandRound( pSat, pSatOn, vLits, vNums, vTemp, nBTLimit, fCanon, -1 ); + Bmc_CollapseExpandRound( pSat, NULL, vLits, vNums, vTemp, nBTLimit, fCanon, -1 ); + } +/* + { + // put into new array + int i, iLit; + Vec_IntClear( vNums ); + Vec_IntForEachEntry( vLits, iLit, i ) + if ( iLit != -1 ) + Vec_IntPush( vNums, i ); + //printf( "%d(%d) ", Vec_IntSize(vNums), Vec_IntSize(vLits) ); + } +*/ + return 0; +} + /**Function************************************************************* Synopsis [Returns SAT solver in the 'sat' state with the given assignment.] @@ -658,8 +757,8 @@ Vec_Str_t * Bmc_CollapseOneInt( Gia_Man_t * p, int nCubeLim, int nBTLimit, int f else Vec_StrWriteEntry( vSop, Start + iVar, (char)('0' + !Abc_LitIsCompl(iLit)) ); } - if ( fVerbose ) - printf( "Cube %4d: %s", Count, Vec_StrArray(vSop) + Start ); + //if ( fVerbose ) + // printf( "Cube %4d: %s", Count, Vec_StrArray(vSop) + Start ); Count++; // add cube status = sat_solver_addclause( pSat[0], Vec_IntArray(vCube), Vec_IntLimit(vCube) ); @@ -687,7 +786,7 @@ cleanup: Bmc_CollapseIrredundant( vSop, Vec_StrSize(vSop)/(nVars +3), nVars ); return vSop; } -Vec_Str_t * Bmc_CollapseOne2( Gia_Man_t * p, int nCubeLim, int nBTLimit, int fCanon, int fReverse, int fVerbose ) +Vec_Str_t * Bmc_CollapseOneOld( Gia_Man_t * p, int nCubeLim, int nBTLimit, int fCanon, int fReverse, int fVerbose ) { Vec_Str_t * vSopOn, * vSopOff; int nCubesOn = ABC_INFINITY; @@ -728,13 +827,11 @@ Vec_Str_t * Bmc_CollapseOne2( Gia_Man_t * p, int nCubeLim, int nBTLimit, int fCa SeeAlso [] ***********************************************************************/ -Vec_Str_t * Bmc_CollapseOne3( Gia_Man_t * p, int nCubeLim, int nBTLimit, int fCanon, int fReverse, int fVerbose ) +Vec_Str_t * Bmc_CollapseOne_int3( sat_solver * pSat0, sat_solver * pSat1, sat_solver * pSat2, sat_solver * pSat3, int nVars, int nCubeLim, int nBTLimit, int fCanon, int fReverse, int fVerbose ) { int fVeryVerbose = fVerbose; - int nVars = Gia_ManCiNum(p); - Cnf_Dat_t * pCnf = Mf_ManGenerateCnf( p, 8, 0, 0, 0 ); - sat_solver * pSat[2] = { (sat_solver *)Cnf_DataWriteIntoSolver(pCnf, 1, 0), (sat_solver *)Cnf_DataWriteIntoSolver(pCnf, 1, 0) }; - sat_solver * pSatClean[2] = { (sat_solver *)Cnf_DataWriteIntoSolver(pCnf, 1, 0), (sat_solver *)Cnf_DataWriteIntoSolver(pCnf, 1, 0) }; + sat_solver * pSat[2] = { pSat0, pSat1 }; + sat_solver * pSatClean[2] = { pSat2, pSat3 }; Vec_Str_t * vSop[2] = { Vec_StrAlloc(1000), Vec_StrAlloc(1000) }, * vRes = NULL; Vec_Int_t * vLitsC[2] = { Vec_IntAlloc(nVars), Vec_IntAlloc(nVars) }; Vec_Int_t * vVars = Vec_IntAlloc( nVars ); @@ -746,7 +843,8 @@ Vec_Str_t * Bmc_CollapseOne3( Gia_Man_t * p, int nCubeLim, int nBTLimit, int fCa int fComplete[2] = {0}; // collect CI variables - iCiVarBeg = pCnf->nVars - nVars;// - 1; +// iCiVarBeg = pCnf->nVars - nVars;// - 1; + iCiVarBeg = sat_solver_nvars(pSat0) - nVars; if ( fReverse ) for ( v = nVars - 1; v >= 0; v-- ) Vec_IntPush( vVars, iCiVarBeg + v ); @@ -855,11 +953,6 @@ cleanup: Vec_IntFree( vLitsC[1] ); Vec_IntFree( vNums ); Vec_IntFree( vCube ); - Cnf_DataFree( pCnf ); - sat_solver_delete( pSat[0] ); - sat_solver_delete( pSat[1] ); - sat_solver_delete( pSatClean[0] ); - sat_solver_delete( pSatClean[1] ); assert( !fComplete[0] || !fComplete[1] ); if ( fComplete[0] || fComplete[1] ) // one of the cover is computed { @@ -892,6 +985,22 @@ cleanup: Vec_StrFreeP( &vSop[1] ); return vRes; } +Vec_Str_t * Bmc_CollapseOne3( Gia_Man_t * p, int nCubeLim, int nBTLimit, int fCanon, int fReverse, int fVerbose ) +{ + Cnf_Dat_t * pCnf = Mf_ManGenerateCnf( p, 8, 0, 0, 0 ); + sat_solver * pSat0 = (sat_solver *)Cnf_DataWriteIntoSolver(pCnf, 1, 0); + sat_solver * pSat1 = (sat_solver *)Cnf_DataWriteIntoSolver(pCnf, 1, 0); + sat_solver * pSat2 = (sat_solver *)Cnf_DataWriteIntoSolver(pCnf, 1, 0); + sat_solver * pSat3 = (sat_solver *)Cnf_DataWriteIntoSolver(pCnf, 1, 0); + Vec_Str_t * vSop = Bmc_CollapseOne_int3( pSat0, pSat1, pSat2, pSat3, Gia_ManCiNum(p), nCubeLim, nBTLimit, fCanon, fReverse, fVerbose ); + sat_solver_delete( pSat0 ); + sat_solver_delete( pSat1 ); + sat_solver_delete( pSat2 ); + sat_solver_delete( pSat3 ); + Cnf_DataFree( pCnf ); + return vSop; +} + /**Function************************************************************* @@ -904,10 +1013,11 @@ cleanup: SeeAlso [] ***********************************************************************/ -Vec_Str_t * Bmc_CollapseOne_int2( sat_solver * pSat, int nVars, int nCubeLim, int nBTLimit, int fCanon, int fReverse, int fVerbose ) +Vec_Str_t * Bmc_CollapseOne_int2( sat_solver * pSat1, sat_solver * pSat2, int nVars, int nCubeLim, int nBTLimit, int fCanon, int fReverse, int fVerbose ) { int fVeryVerbose = fVerbose; - Vec_Str_t * vSop[2] = { Vec_StrAlloc(1000), Vec_StrAlloc(1000) }, * vRes = NULL; + sat_solver * pSat[2] = { pSat1, pSat2 }; + Vec_Str_t * vSop[2] = { Vec_StrAlloc(1000), Vec_StrAlloc(1000) }, * vRes = NULL; Vec_Int_t * vVars = Vec_IntAlloc( nVars+1 ); Vec_Int_t * vLits = Vec_IntAlloc( nVars+1 ); Vec_Int_t * vNums = Vec_IntAlloc( nVars+1 ); @@ -935,7 +1045,7 @@ Vec_Str_t * Bmc_CollapseOne_int2( sat_solver * pSat, int nVars, int nCubeLim, in for ( n = 0; n < 2; n++ ) { pLits[0] = Abc_Var2Lit( iOutVar, n ); // n=0 => F=1 n=1 => F=0 - status = sat_solver_solve( pSat, pLits, pLits + 1, nBTLimit, 0, 0, 0 ); + status = sat_solver_solve( pSat[n], pLits, pLits + 1, nBTLimit, 0, 0, 0 ); if ( status == l_Undef ) goto cleanup; // timeout if ( status == l_False ) @@ -946,6 +1056,9 @@ Vec_Str_t * Bmc_CollapseOne_int2( sat_solver * pSat, int nVars, int nCubeLim, in fComplete[0] = 1; goto cleanup; // const0/1 } + // add literals to the solver + status = sat_solver_addclause( pSat[n], pLits, pLits + 1 ); + assert( status ); // start cover Vec_StrPush( vSop[n], '\0' ); } @@ -957,10 +1070,11 @@ Vec_Str_t * Bmc_CollapseOne_int2( sat_solver * pSat, int nVars, int nCubeLim, in { if ( fVeryVerbose ) clk = Abc_Clock(); // get the assignment - sat_solver_clean_polarity( pSat, Vec_IntArray(vVars), Vec_IntSize(vVars) ); - pLits[0] = Abc_Var2Lit( iOutVar, n ); // set output - pLits[1] = Abc_Var2Lit( iOOVars[n], 1 ); // enable clauses - status = sat_solver_solve( pSat, pLits, pLits + 2, 0, 0, 0, 0 ); + sat_solver_clean_polarity( pSat[n], Vec_IntArray(vVars), Vec_IntSize(vVars) ); + pLits[0] = Abc_Var2Lit( iOOVars[n], 1 ); // enable clauses +// pLits[1] = Abc_Var2Lit( iOutVar, n ); // set output +// status = sat_solver_solve( pSat, pLits, pLits + 2, 0, 0, 0, 0 ); + status = sat_solver_solve( pSat[n], pLits, pLits + 1, 0, 0, 0, 0 ); if ( fVeryVerbose ) Time[n][0] += Abc_Clock() - clk; if ( status == l_Undef ) goto cleanup; // timeout @@ -972,10 +1086,11 @@ Vec_Str_t * Bmc_CollapseOne_int2( sat_solver * pSat, int nVars, int nCubeLim, in // collect values Vec_IntClear( vLits ); Vec_IntForEachEntry( vVars, iVar, v ) - Vec_IntPush( vLits, Abc_Var2Lit(iVar, !sat_solver_var_value(pSat, iVar)) ); + Vec_IntPush( vLits, Abc_Var2Lit(iVar, !sat_solver_var_value(pSat[n], iVar)) ); // expand the values if ( fVeryVerbose ) clk = Abc_Clock(); - status = Bmc_CollapseExpand( pSat, NULL, vLits, vNums, vCube, nBTLimit, fCanon, Abc_Var2Lit(iOutVar, !n) ); +// status = Bmc_CollapseExpand( pSat, NULL, vLits, vNums, vCube, nBTLimit, fCanon, Abc_Var2Lit(iOutVar, !n) ); + status = Bmc_CollapseExpand( pSat[!n], NULL, vLits, vNums, vCube, nBTLimit, fCanon, -1 ); if ( fVeryVerbose ) Time[n][1] += Abc_Clock() - clk; if ( status < 0 ) goto cleanup; // timeout @@ -999,7 +1114,8 @@ Vec_Str_t * Bmc_CollapseOne_int2( sat_solver * pSat, int nVars, int nCubeLim, in } // add cube Vec_IntPush( vCube, Abc_Var2Lit( iOOVars[n], 0 ) ); - status = sat_solver_addclause( pSat, Vec_IntArray(vCube), Vec_IntLimit(vCube) ); +// status = sat_solver_addclause( pSat, Vec_IntArray(vCube), Vec_IntLimit(vCube) ); + status = sat_solver_addclause( pSat[n], Vec_IntArray(vCube), Vec_IntLimit(vCube) ); if ( status == 0 ) { fComplete[n] = 1; @@ -1047,15 +1163,6 @@ cleanup: Vec_StrFreeP( &vSop[1] ); return vRes; } -Vec_Str_t * Bmc_CollapseOne( Gia_Man_t * p, int nCubeLim, int nBTLimit, int fCanon, int fReverse, int fVerbose ) -{ - Cnf_Dat_t * pCnf = Mf_ManGenerateCnf( p, 8, 0, 0, 0 ); - sat_solver * pSat = (sat_solver *)Cnf_DataWriteIntoSolver(pCnf, 1, 0); - Vec_Str_t * vSop = Bmc_CollapseOne_int2( pSat, Gia_ManCiNum(p), nCubeLim, nBTLimit, fCanon, fReverse, fVerbose ); - sat_solver_delete( pSat ); - Cnf_DataFree( pCnf ); - return vSop; -} /**Function************************************************************* @@ -1069,11 +1176,10 @@ Vec_Str_t * Bmc_CollapseOne( Gia_Man_t * p, int nCubeLim, int nBTLimit, int fCan SeeAlso [] ***********************************************************************/ -Vec_Str_t * Bmc_CollapseOne_int( sat_solver * pSat1, sat_solver * pSat2, int nVars, int nCubeLim, int nBTLimit, int fCanon, int fReverse, int fVerbose ) +Vec_Str_t * Bmc_CollapseOne_int( sat_solver * pSat, int nVars, int nCubeLim, int nBTLimit, int fCanon, int fReverse, int fVerbose ) { int fVeryVerbose = fVerbose; - sat_solver * pSat[2] = { pSat1, pSat2 }; - Vec_Str_t * vSop[2] = { Vec_StrAlloc(1000), Vec_StrAlloc(1000) }, * vRes = NULL; + Vec_Str_t * vSop[2] = { Vec_StrAlloc(1000), Vec_StrAlloc(1000) }, * vRes = NULL; Vec_Int_t * vVars = Vec_IntAlloc( nVars+1 ); Vec_Int_t * vLits = Vec_IntAlloc( nVars+1 ); Vec_Int_t * vNums = Vec_IntAlloc( nVars+1 ); @@ -1101,7 +1207,7 @@ Vec_Str_t * Bmc_CollapseOne_int( sat_solver * pSat1, sat_solver * pSat2, int nVa for ( n = 0; n < 2; n++ ) { pLits[0] = Abc_Var2Lit( iOutVar, n ); // n=0 => F=1 n=1 => F=0 - status = sat_solver_solve( pSat[n], pLits, pLits + 1, nBTLimit, 0, 0, 0 ); + status = sat_solver_solve( pSat, pLits, pLits + 1, nBTLimit, 0, 0, 0 ); if ( status == l_Undef ) goto cleanup; // timeout if ( status == l_False ) @@ -1112,9 +1218,6 @@ Vec_Str_t * Bmc_CollapseOne_int( sat_solver * pSat1, sat_solver * pSat2, int nVa fComplete[0] = 1; goto cleanup; // const0/1 } - // add literals to the solver - status = sat_solver_addclause( pSat[n], pLits, pLits + 1 ); - assert( status ); // start cover Vec_StrPush( vSop[n], '\0' ); } @@ -1126,11 +1229,10 @@ Vec_Str_t * Bmc_CollapseOne_int( sat_solver * pSat1, sat_solver * pSat2, int nVa { if ( fVeryVerbose ) clk = Abc_Clock(); // get the assignment - sat_solver_clean_polarity( pSat[n], Vec_IntArray(vVars), Vec_IntSize(vVars) ); + sat_solver_clean_polarity( pSat, Vec_IntArray(vVars), Vec_IntSize(vVars) ); pLits[0] = Abc_Var2Lit( iOOVars[n], 1 ); // enable clauses -// pLits[1] = Abc_Var2Lit( iOutVar, n ); // set output -// status = sat_solver_solve( pSat, pLits, pLits + 2, 0, 0, 0, 0 ); - status = sat_solver_solve( pSat[n], pLits, pLits + 1, 0, 0, 0, 0 ); + pLits[1] = Abc_Var2Lit( iOutVar, n ); // set output + status = sat_solver_solve( pSat, pLits, pLits + 2, 0, 0, 0, 0 ); if ( fVeryVerbose ) Time[n][0] += Abc_Clock() - clk; if ( status == l_Undef ) goto cleanup; // timeout @@ -1142,11 +1244,10 @@ Vec_Str_t * Bmc_CollapseOne_int( sat_solver * pSat1, sat_solver * pSat2, int nVa // collect values Vec_IntClear( vLits ); Vec_IntForEachEntry( vVars, iVar, v ) - Vec_IntPush( vLits, Abc_Var2Lit(iVar, !sat_solver_var_value(pSat[n], iVar)) ); + Vec_IntPush( vLits, Abc_Var2Lit(iVar, !sat_solver_var_value(pSat, iVar)) ); // expand the values if ( fVeryVerbose ) clk = Abc_Clock(); -// status = Bmc_CollapseExpand( pSat, NULL, vLits, vNums, vCube, nBTLimit, fCanon, Abc_Var2Lit(iOutVar, !n) ); - status = Bmc_CollapseExpand( pSat[!n], NULL, vLits, vNums, vCube, nBTLimit, fCanon, -1 ); + status = Bmc_CollapseExpand( pSat, NULL, vLits, vNums, vCube, nBTLimit, fCanon, Abc_Var2Lit(iOutVar, !n) ); if ( fVeryVerbose ) Time[n][1] += Abc_Clock() - clk; if ( status < 0 ) goto cleanup; // timeout @@ -1159,6 +1260,7 @@ Vec_Str_t * Bmc_CollapseOne_int( sat_solver * pSat1, sat_solver * pSat2, int nVa Vec_StrWriteEntry( vSop[n], Start + nVars + 2, '\n' ); Vec_StrWriteEntry( vSop[n], Start + nVars + 3, '\0' ); Vec_IntClear( vCube ); + Vec_IntPush( vCube, Abc_Var2Lit( iOOVars[n], 0 ) ); Vec_IntForEachEntry( vNums, iVar, v ) { int iLit = Vec_IntEntry( vLits, iVar ); @@ -1169,9 +1271,7 @@ Vec_Str_t * Bmc_CollapseOne_int( sat_solver * pSat1, sat_solver * pSat2, int nVa Vec_StrWriteEntry( vSop[n], Start + iVar, (char)('0' + !Abc_LitIsCompl(iLit)) ); } // add cube - Vec_IntPush( vCube, Abc_Var2Lit( iOOVars[n], 0 ) ); -// status = sat_solver_addclause( pSat, Vec_IntArray(vCube), Vec_IntLimit(vCube) ); - status = sat_solver_addclause( pSat[n], Vec_IntArray(vCube), Vec_IntLimit(vCube) ); + status = sat_solver_addclause( pSat, Vec_IntArray(vCube), Vec_IntLimit(vCube) ); if ( status == 0 ) { fComplete[n] = 1; @@ -1219,6 +1319,15 @@ cleanup: Vec_StrFreeP( &vSop[1] ); return vRes; } +Vec_Str_t * Bmc_CollapseOne( Gia_Man_t * p, int nCubeLim, int nBTLimit, int fCanon, int fReverse, int fVerbose ) +{ + Cnf_Dat_t * pCnf = Mf_ManGenerateCnf( p, 8, 0, 0, 0 ); + sat_solver * pSat = (sat_solver *)Cnf_DataWriteIntoSolver(pCnf, 1, 0); + Vec_Str_t * vSop = Bmc_CollapseOne_int( pSat, Gia_ManCiNum(p), nCubeLim, nBTLimit, fCanon, fReverse, fVerbose ); + sat_solver_delete( pSat ); + Cnf_DataFree( pCnf ); + return vSop; +} //////////////////////////////////////////////////////////////////////// /// END OF FILE /// -- cgit v1.2.3