Adding new implementation of LEXSAT.

src/sat/bmc/bmcClp.c

@@ -592,7 +592,7 @@ int Bmc_CollapseExpand2( sat_solver * pSat, sat_solver * pSatOn, Vec_Int_t * vLi
   SeeAlso     []
 
 ***********************************************************************/
-int Bmc_ComputeCanonical( sat_solver * pSat, Vec_Int_t * vLits, Vec_Int_t * vTemp, int nBTLimit )
+int Bmc_ComputeCanonical2( sat_solver * pSat, Vec_Int_t * vLits, Vec_Int_t * vTemp, int nBTLimit )
 {
     int i, k, iLit, status = l_Undef;
     for ( i = 0; i < Vec_IntSize(vLits); i++ )
@@ -621,6 +621,11 @@ int Bmc_ComputeCanonical( sat_solver * pSat, Vec_Int_t * vLits, Vec_Int_t * vTem
     assert( status == l_True );
     return status;
 }
+int Bmc_ComputeCanonical( sat_solver * pSat, Vec_Int_t * vLits, Vec_Int_t * vTemp, int nBTLimit )
+{
+    sat_solver_set_resource_limits( pSat, nBTLimit, 0, 0, 0 );
+    return sat_solver_solve_lexsat( pSat, Vec_IntArray(vLits), Vec_IntSize(vLits) );
+}
 
 /**Function*************************************************************
 

src/sat/bsat/satSolver.c

@@ -1885,6 +1885,74 @@ int sat_solver_solve(sat_solver* s, lit* begin, lit* end, ABC_INT64_T nConfLimit
     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.
+// 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 );
+    // help the SAT solver by setting desirable polarity
+    sat_solver_set_literal_polarity( s, pLits, nLits );
+    // check if there exists a satisfying assignment
+    status = sat_solver_solve_internal( s );
+    if ( status != l_True ) // no assignment
+        return status;
+    // there is at least one satisfying assignment
+    assert( status == l_True );
+    // find the first mismatching literal
+    for ( i = 0; i < nLits; i++ )
+        if ( pLits[i] != sat_solver_var_literal(s, Abc_Lit2Var(pLits[i])) )
+            break;
+    if ( i == nLits ) // no mismatch - the current assignment is the minimum one!
+        return l_True;
+    // mismatch happens in literal i
+    iLitFail = i;
+    // create assumptions up to this literal (as in pLits) - including this literal!
+    for ( i = 0; i <= iLitFail; i++ )
+        if ( !sat_solver_push(s, pLits[i]) ) // can become UNSAT while adding the last assumption
+            break;
+    if ( i < iLitFail + 1 ) // the solver became UNSAT while adding assumptions
+        status = l_False;
+    else // solve under the assumptions
+        status = sat_solver_solve_internal( s );
+    if ( status == l_True )
+    {
+        // we proved that there is a sat assignment with literal (iLitFail) having polarity as in pLits
+        // continue solving recursively
+        if ( iLitFail + 1 < nLits )
+            status = sat_solver_solve_lexsat( s, pLits + iLitFail + 1, nLits - iLitFail - 1 );
+    }
+    else if ( status == l_False )
+    {
+        // we proved that there is no assignment with iLitFail having polarity as in pLits
+        assert( Abc_LitIsCompl(pLits[iLitFail]) ); // 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
+        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" ); // because we know that the problem is satisfiable
+        // update other literals to be 000...0
+        for ( i = iLitFail + 1; i < nLits; i++ )
+            pLits[i] = Abc_LitNot( Abc_LitRegular(pLits[i]) );
+        // continue solving recursively
+        if ( iLitFail + 1 < nLits )
+            status = sat_solver_solve_lexsat( s, pLits + iLitFail + 1, nLits - iLitFail - 1 );
+        else
+            status = l_True;
+    }
+    // undo the assumptions
+    for ( i = iLitFail; i >= 0; i-- )
+        sat_solver_pop( s );
+    return status;
+}
+
 
 int sat_solver_nvars(sat_solver* s)
 {

src/sat/bsat/satSolver.h

@@ -49,6 +49,7 @@ extern int         sat_solver_clause_new(sat_solver* s, lit* begin, lit* end, in
 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_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);