Adding efficient procedure to minimize the set of assumptions.

3 files changed, 79 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..3d24161e 100644
--- a/src/sat/bsat/satSolver.c
+++ b/src/sat/bsat/satSolver.c
@@ -2168,6 +2168,58 @@ 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
+        // 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 );
+    nLitsR = nLits / 2;
+    nLitsL = nLits - nLitsR;
+    // 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] );
+    // 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;
+}
+
 
 int sat_solver_nvars(sat_solver* s)
 {
diff --git a/src/sat/bsat/satSolver.h b/src/sat/bsat/satSolver.h
index 5a8483c1..ac0b6e8d 100644
--- a/src/sat/bsat/satSolver.h
+++ b/src/sat/bsat/satSolver.h
@@ -50,6 +50,7 @@ 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_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);