abc/src/sat/bsat/satSolver.c
// 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
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
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 )
    {
        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 ( status == l_False )
        {
            RetValue = sat_solver_addclause( s, &LitNot, &LitNot+1 );
            assert( RetValue );
        }
        s->nConfLimit = Temp;
        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);
            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 );
        }
    nResL = sat_solver_minimize_assumptions2( 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);
            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 );
        }
    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_minimize_assumptions2 ( sat_solver * s , int * pLits , int nLits , int nConfLimit ) { int i , k , nLitsL , nLitsR , nResL , nResR ; if ( nLits == 1 ) { 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 ( status == l_False ) { RetValue = sat_solver_addclause ( s , & LitNot , & LitNot + 1 ) ; assert ( RetValue ) ; } s -> nConfLimit = Temp ; 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 ) ; 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 ) ; } nResL = sat_solver_minimize_assumptions2 ( 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 ) ; 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 ) ; } nResR = sat_solver_minimize_assumptions2 ( 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
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
// 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 // if the problem is UNSAT, add clause // return 1 if the problem is not UNSAT // assume the left lits // add clauses for these literal // solve for the right lits // swap literals //    assert( nResL <= nLitsL ); // assume the right lits // add clauses for these literal // solve for the left lits