diff options
Diffstat (limited to 'src/sat')
-rw-r--r-- | src/sat/bmc/bmcClp.c | 26 | ||||
-rw-r--r-- | src/sat/bsat/satSolver.c | 147 | ||||
-rw-r--r-- | src/sat/bsat/satSolver.h | 2 |
3 files changed, 175 insertions, 0 deletions
diff --git a/src/sat/bmc/bmcClp.c b/src/sat/bmc/bmcClp.c index cfc608b1..2ac94da5 100644 --- a/src/sat/bmc/bmcClp.c +++ b/src/sat/bmc/bmcClp.c @@ -353,11 +353,37 @@ int Bmc_CollapseIrredundantFull( Vec_Str_t * vSop, int nCubes, int nVars ) SeeAlso [] ***********************************************************************/ +int Bmc_CollapseExpandRound2( sat_solver * pSat, Vec_Int_t * vLits, Vec_Int_t * vTemp, int nBTLimit, int fOnOffSetLit ) +{ + // put into new array + int i, iLit, nLits; + Vec_IntClear( vTemp ); + Vec_IntForEachEntry( vLits, iLit, i ) + if ( iLit != -1 ) + Vec_IntPush( vTemp, iLit ); + assert( Vec_IntSize(vTemp) > 0 ); + // assume condition literal + if ( fOnOffSetLit >= 0 ) + sat_solver_push( pSat, fOnOffSetLit ); + // minimize + nLits = sat_solver_minimize_assumptions( pSat, Vec_IntArray(vTemp), Vec_IntSize(vTemp), nBTLimit ); + Vec_IntShrink( vTemp, nLits ); + // assume conditional literal + if ( fOnOffSetLit >= 0 ) + sat_solver_pop( pSat ); + // modify output literas + Vec_IntForEachEntry( vLits, iLit, i ) + if ( iLit != -1 && Vec_IntFind(vTemp, iLit) == -1 ) + Vec_IntWriteEntry( vLits, i, -1 ); + return 0; +} + int Bmc_CollapseExpandRound( sat_solver * pSat, sat_solver * pSatOn, Vec_Int_t * vLits, Vec_Int_t * vNums, Vec_Int_t * vTemp, int nBTLimit, int fCanon, int fOnOffSetLit ) { int fProfile = 0; int k, n, iLit, status; abctime clk; + //return Bmc_CollapseExpandRound2( pSat, vLits, vTemp, nBTLimit, fOnOffSetLit ); // try removing one literal at a time for ( k = Vec_IntSize(vLits) - 1; k >= 0; k-- ) { diff --git a/src/sat/bsat/satSolver.c b/src/sat/bsat/satSolver.c index df9ada8e..fe7e65fe 100644 --- a/src/sat/bsat/satSolver.c +++ b/src/sat/bsat/satSolver.c @@ -2168,6 +2168,153 @@ int sat_solver_solve_lexsat( sat_solver* s, int * pLits, int nLits ) return status; } +// This procedure is called on a set of assumptions to minimize their number. +// The procedure relies on the fact that the current set of assumptions is UNSAT. +// It receives and returns SAT solver without assumptions. It returns the number +// of assumptions after minimization. The set of assumptions is returned in pLits. +int sat_solver_minimize_assumptions( sat_solver* s, int * pLits, int nLits, int nConfLimit ) +{ + int i, k, nLitsL, nLitsR, nResL, nResR; + if ( nLits == 1 ) + { + // since the problem is UNSAT, we will try to solve it without assuming the last literal + // if the result is UNSAT, the last literal can be dropped; otherwise, it is needed + int status = l_False; + int Temp = s->nConfLimit; + s->nConfLimit = nConfLimit; + status = sat_solver_solve_internal( s ); + s->nConfLimit = Temp; + return (int)(status != l_False); // return 1 if the problem is not UNSAT + } + assert( nLits >= 2 ); + nLitsL = nLits / 2; + nLitsR = nLits - nLitsL; + // assume the left lits + for ( i = 0; i < nLitsL; i++ ) + if ( !sat_solver_push(s, pLits[i]) ) + { + for ( k = i; k >= 0; k-- ) + sat_solver_pop(s); + return sat_solver_minimize_assumptions( s, pLits, i+1, nConfLimit ); + } + // solve for the right lits + nResL = sat_solver_minimize_assumptions( s, pLits + nLitsL, nLitsR, nConfLimit ); + for ( i = 0; i < nLitsL; i++ ) + sat_solver_pop(s); + // swap literals +// assert( nResL <= nLitsL ); +// for ( i = 0; i < nResL; i++ ) +// ABC_SWAP( int, pLits[i], pLits[nLitsL+i] ); + veci_resize( &s->temp_clause, 0 ); + for ( i = 0; i < nLitsL; i++ ) + veci_push( &s->temp_clause, pLits[i] ); + for ( i = 0; i < nResL; i++ ) + pLits[i] = pLits[nLitsL+i]; + for ( i = 0; i < nLitsL; i++ ) + pLits[nResL+i] = veci_begin(&s->temp_clause)[i]; + // assume the right lits + for ( i = 0; i < nResL; i++ ) + if ( !sat_solver_push(s, pLits[i]) ) + { + for ( k = i; k >= 0; k-- ) + sat_solver_pop(s); + return sat_solver_minimize_assumptions( s, pLits, i+1, nConfLimit ); + } + // solve for the left lits + nResR = sat_solver_minimize_assumptions( s, pLits + nResL, nLitsL, nConfLimit ); + for ( i = 0; i < nResL; i++ ) + sat_solver_pop(s); + return nResL + nResR; +} + +// This is a specialized version of the above procedure with several custom changes: +// - makes sure that at least one of the marked literals is preserved in the clause +// - sets literals to zero when they do not have to be used +// - sets literals to zero for disproved variables +int sat_solver_minimize_assumptions2( sat_solver* s, int * pLits, int nLits, int nConfLimit ) +{ + int i, k, nLitsL, nLitsR, nResL, nResR; + if ( nLits == 1 ) + { + // since the problem is UNSAT, we will try to solve it without assuming the last literal + // if the result is UNSAT, the last literal can be dropped; otherwise, it is needed + int RetValue = 1, LitNot = Abc_LitNot(pLits[0]); + int status = l_False; + int Temp = s->nConfLimit; + s->nConfLimit = nConfLimit; + + RetValue = sat_solver_push( s, LitNot ); assert( RetValue ); + status = sat_solver_solve_internal( s ); + sat_solver_pop( s ); + + // if the problem is UNSAT, add clause + if ( status == l_False ) + { + RetValue = sat_solver_addclause( s, &LitNot, &LitNot+1 ); + assert( RetValue ); + } + + s->nConfLimit = Temp; + return (int)(status != l_False); // return 1 if the problem is not UNSAT + } + assert( nLits >= 2 ); + nLitsL = nLits / 2; + nLitsR = nLits - nLitsL; + // assume the left lits + for ( i = 0; i < nLitsL; i++ ) + if ( !sat_solver_push(s, pLits[i]) ) + { + for ( k = i; k >= 0; k-- ) + sat_solver_pop(s); + + // add clauses for these literal + for ( k = i+1; k > nLitsL; k++ ) + { + int LitNot = Abc_LitNot(pLits[i]); + int RetValue = sat_solver_addclause( s, &LitNot, &LitNot+1 ); + assert( RetValue ); + } + + return sat_solver_minimize_assumptions2( s, pLits, i+1, nConfLimit ); + } + // solve for the right lits + nResL = sat_solver_minimize_assumptions2( s, pLits + nLitsL, nLitsR, nConfLimit ); + for ( i = 0; i < nLitsL; i++ ) + sat_solver_pop(s); + // swap literals +// assert( nResL <= nLitsL ); + veci_resize( &s->temp_clause, 0 ); + for ( i = 0; i < nLitsL; i++ ) + veci_push( &s->temp_clause, pLits[i] ); + for ( i = 0; i < nResL; i++ ) + pLits[i] = pLits[nLitsL+i]; + for ( i = 0; i < nLitsL; i++ ) + pLits[nResL+i] = veci_begin(&s->temp_clause)[i]; + // assume the right lits + for ( i = 0; i < nResL; i++ ) + if ( !sat_solver_push(s, pLits[i]) ) + { + for ( k = i; k >= 0; k-- ) + sat_solver_pop(s); + + // add clauses for these literal + for ( k = i+1; k > nResL; k++ ) + { + int LitNot = Abc_LitNot(pLits[i]); + int RetValue = sat_solver_addclause( s, &LitNot, &LitNot+1 ); + assert( RetValue ); + } + + return sat_solver_minimize_assumptions2( s, pLits, i+1, nConfLimit ); + } + // solve for the left lits + nResR = sat_solver_minimize_assumptions2( s, pLits + nResL, nLitsL, nConfLimit ); + for ( i = 0; i < nResL; i++ ) + sat_solver_pop(s); + return nResL + nResR; +} + + int sat_solver_nvars(sat_solver* s) { diff --git a/src/sat/bsat/satSolver.h b/src/sat/bsat/satSolver.h index 5a8483c1..5191b2cd 100644 --- a/src/sat/bsat/satSolver.h +++ b/src/sat/bsat/satSolver.h @@ -50,6 +50,8 @@ extern int sat_solver_simplify(sat_solver* s); extern int sat_solver_solve(sat_solver* s, lit* begin, lit* end, ABC_INT64_T nConfLimit, ABC_INT64_T nInsLimit, ABC_INT64_T nConfLimitGlobal, ABC_INT64_T nInsLimitGlobal); extern int sat_solver_solve_internal(sat_solver* s); extern int sat_solver_solve_lexsat(sat_solver* s, int * pLits, int nLits); +extern int sat_solver_minimize_assumptions( sat_solver* s, int * pLits, int nLits, int nConfLimit ); +extern int sat_solver_minimize_assumptions2( sat_solver* s, int * pLits, int nLits, int nConfLimit ); extern int sat_solver_push(sat_solver* s, int p); extern void sat_solver_pop(sat_solver* s); extern void sat_solver_set_resource_limits(sat_solver* s, ABC_INT64_T nConfLimit, ABC_INT64_T nInsLimit, ABC_INT64_T nConfLimitGlobal, ABC_INT64_T nInsLimitGlobal); |