abc/src/sat/bsat/satSolver.c
// This LEXSAT procedure should be called with a set of literals (pLits, nLits),
// which defines both (1) variable order, and (2) assignment to begin search from.
// It retuns the LEXSAT assigment that is the same or larger than the given one.
// (It assumes that there is no smaller assignment than the one given!)
// The resulting assignment is returned in the same set of literals (pLits, nLits).
// It pushes/pops assumptions internally and will undo them before terminating.
This LEXSAT procedure should be called with a set of literals (pLits, nLits),
which defines both (1) variable order, and (2) assignment to begin search from.
It retuns the LEXSAT assigment that is the same or larger than the given one.
(It assumes that there is no smaller assignment than the one given!)
The resulting assignment is returned in the same set of literals (pLits, nLits).
It pushes/pops assumptions internally and will undo them before terminating.
This LEXSAT procedure should be called with a set of literals ( pLits nLits ) which defines both ( 1 ) variable order and ( 2 ) assignment to begin search from . It retuns the LEXSAT assigment that is the same or larger than the given one . ( It assumes that there is no smaller assignment than the one given! ) The resulting assignment is returned in the same set of literals ( pLits nLits ) . It pushes / pops assumptions internally and will undo them before terminating .
int sat_solver_solve_lexsat( sat_solver* s, int * pLits, int nLits )
{
    int i, iLitFail = -1;
    lbool status;
    assert( nLits > 0 );
    sat_solver_set_literal_polarity( s, pLits, nLits );
    status = sat_solver_solve_internal( s );
    if ( status != l_True ) 
        return status;
    assert( status == l_True );
    for ( i = 0; i < nLits; i++ )
        if ( pLits[i] != sat_solver_var_literal(s, Abc_Lit2Var(pLits[i])) )
            break;
    if ( i == nLits ) 
        return l_True;
    iLitFail = i;
    for ( i = 0; i <= iLitFail; i++ )
        if ( !sat_solver_push(s, pLits[i]) ) 
            break;
    if ( i < iLitFail + 1 ) 
        status = l_False;
    else 
        status = sat_solver_solve_internal( s );
    if ( status == l_True )
    {
        if ( iLitFail + 1 < nLits )
            status = sat_solver_solve_lexsat( s, pLits + iLitFail + 1, nLits - iLitFail - 1 );
    }
    else if ( status == l_False )
    {
        assert( Abc_LitIsCompl(pLits[iLitFail]) ); 
        sat_solver_pop( s );
        pLits[iLitFail] = Abc_LitNot(pLits[iLitFail]);
        if ( !sat_solver_push(s, pLits[iLitFail]) )
            printf( "sat_solver_solve_lexsat(): A satisfying assignment should exist.\n" ); 
        for ( i = iLitFail + 1; i < nLits; i++ )
            pLits[i] = Abc_LitNot( Abc_LitRegular(pLits[i]) );
        if ( iLitFail + 1 < nLits )
            status = sat_solver_solve_lexsat( s, pLits + iLitFail + 1, nLits - iLitFail - 1 );
        else
            status = l_True;
    }
    for ( i = iLitFail; i >= 0; i-- )
        sat_solver_pop( s );
    return status;
}
int sat_solver_solve_lexsat ( sat_solver * s , int * pLits , int nLits ) { int i , iLitFail = -1 ; lbool status ; assert ( nLits > 0 ) ; sat_solver_set_literal_polarity ( s , pLits , nLits ) ; status = sat_solver_solve_internal ( s ) ; if ( status != l_True ) return status ; assert ( status == l_True ) ; for ( i = 0 ; i < nLits ; i ++ ) if ( pLits [ i ] != sat_solver_var_literal ( s , Abc_Lit2Var ( pLits [ i ] ) ) ) break ; if ( i == nLits ) return l_True ; iLitFail = i ; for ( i = 0 ; i <= iLitFail ; i ++ ) if ( ! sat_solver_push ( s , pLits [ i ] ) ) break ; if ( i < iLitFail + 1 ) status = l_False ; else status = sat_solver_solve_internal ( s ) ; if ( status == l_True ) { if ( iLitFail + 1 < nLits ) status = sat_solver_solve_lexsat ( s , pLits + iLitFail + 1 , nLits - iLitFail - 1 ) ; } else if ( status == l_False ) { assert ( Abc_LitIsCompl ( pLits [ iLitFail ] ) ) ; sat_solver_pop ( s ) ; pLits [ iLitFail ] = Abc_LitNot ( pLits [ iLitFail ] ) ; if ( ! sat_solver_push ( s , pLits [ iLitFail ] ) ) printf ( " \n " ) ; for ( i = iLitFail + 1 ; i < nLits ; i ++ ) pLits [ i ] = Abc_LitNot ( Abc_LitRegular ( pLits [ i ] ) ) ; if ( iLitFail + 1 < nLits ) status = sat_solver_solve_lexsat ( s , pLits + iLitFail + 1 , nLits - iLitFail - 1 ) ; else status = l_True ; } for ( i = iLitFail ; i >= 0 ; i -- ) sat_solver_pop ( s ) ; return status ; }
This LEXSAT procedure should be called with a set of literals (pLits, nLits),
which defines both (1) variable order, and (2) assignment to begin search from.
This LEXSAT procedure should be called with a set of literals ( pLits nLits ) which defines both ( 1 ) variable order and ( 2 ) assignment to begin search from .
// help the SAT solver by setting desirable polarity // check if there exists a satisfying assignment // no assignment // there is at least one satisfying assignment // find the first mismatching literal // no mismatch - the current assignment is the minimum one! // mismatch happens in literal i // create assumptions up to this literal (as in pLits) - including this literal! // can become UNSAT while adding the last assumption // the solver became UNSAT while adding assumptions // solve under the assumptions // we proved that there is a sat assignment with literal (iLitFail) having polarity as in pLits // continue solving recursively // we proved that there is no assignment with iLitFail having polarity as in pLits // literal is 0  // (this assert may fail only if there is a sat assignment smaller than one originally given in pLits) // now we flip this literal (make it 1), change the last assumption // and contiue looking for the 000...0-assignment of other literals // because we know that the problem is satisfiable // update other literals to be 000...0 // continue solving recursively // undo the assumptions