abc/src/sat/bsat/satSolver.c
// 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.
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.
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, status;
    if ( nLits == 1 )
    {
        if ( nConfLimit ) s->nConfLimit = s->stats.conflicts + nConfLimit;
        status = sat_solver_solve_internal( s );
        return (int)(status != l_False); 
    }
    assert( nLits >= 2 );
    nLitsL = nLits / 2;
    nLitsR = nLits - nLitsL;
    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 );
        }
    if ( nConfLimit ) s->nConfLimit = s->stats.conflicts + nConfLimit;
    status = sat_solver_solve_internal( s );
    if ( status == l_False ) 
    {
        for ( i = 0; i < nLitsL; i++ )
            sat_solver_pop(s);
        return sat_solver_minimize_assumptions( s, pLits, nLitsL, nConfLimit );
    }
    nResL = nLitsR == 1 ? 1 : sat_solver_minimize_assumptions( s, pLits + nLitsL, nLitsR, nConfLimit );
    for ( i = 0; i < nLitsL; i++ )
        sat_solver_pop(s);
    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];
    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 );
        }
    if ( nConfLimit ) s->nConfLimit = s->stats.conflicts + nConfLimit;
    status = sat_solver_solve_internal( s );
    if ( status == l_False ) 
    {
        for ( i = 0; i < nResL; i++ )
            sat_solver_pop(s);
        return nResL;
    }
    nResR = nLitsL == 1 ? 1 : sat_solver_minimize_assumptions( s, pLits + nResL, nLitsL, nConfLimit );
    for ( i = 0; i < nResL; i++ )
        sat_solver_pop(s);
    return nResL + nResR;
}
int sat_solver_minimize_assumptions ( sat_solver * s , int * pLits , int nLits , int nConfLimit ) { int i , k , nLitsL , nLitsR , nResL , nResR , status ; if ( nLits == 1 ) { if ( nConfLimit ) s -> nConfLimit = s -> stats . conflicts + nConfLimit ; status = sat_solver_solve_internal ( s ) ; return ( int ) ( status != l_False ) ; } assert ( nLits >= 2 ) ; nLitsL = nLits / 2 ; nLitsR = nLits - nLitsL ; 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 ) ; } if ( nConfLimit ) s -> nConfLimit = s -> stats . conflicts + nConfLimit ; status = sat_solver_solve_internal ( s ) ; if ( status == l_False ) { for ( i = 0 ; i < nLitsL ; i ++ ) sat_solver_pop ( s ) ; return sat_solver_minimize_assumptions ( s , pLits , nLitsL , nConfLimit ) ; } nResL = nLitsR == 1 ? 1 : sat_solver_minimize_assumptions ( s , pLits + nLitsL , nLitsR , nConfLimit ) ; for ( i = 0 ; i < nLitsL ; i ++ ) sat_solver_pop ( s ) ; 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 ] ; 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 ) ; } if ( nConfLimit ) s -> nConfLimit = s -> stats . conflicts + nConfLimit ; status = sat_solver_solve_internal ( s ) ; if ( status == l_False ) { for ( i = 0 ; i < nResL ; i ++ ) sat_solver_pop ( s ) ; return nResL ; } nResR = nLitsL == 1 ? 1 : sat_solver_minimize_assumptions ( s , pLits + nResL , nLitsL , nConfLimit ) ; for ( i = 0 ; i < nResL ; i ++ ) sat_solver_pop ( s ) ; return nResL + nResR ; }
This procedure is called on a set of assumptions to minimize their number.
This procedure is called on a set of assumptions to minimize their number .
// 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 //printf( "%c", status == l_False ? 'u' : 's' ); // return 1 if the problem is not UNSAT // assume the left lits // solve with these assumptions // these are enough // solve for the right lits // swap literals //    assert( nResL <= nLitsL ); //    for ( i = 0; i < nResL; i++ ) //        ABC_SWAP( int, pLits[i], pLits[nLitsL+i] ); // assume the right lits // solve with these assumptions // these are enough // solve for the left lits