Merged alanmi/abc into default

8 files changed, 249 insertions, 3 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..fe7e65fe 100644
--- a/src/sat/bsat/satSolver.c
+++ b/src/sat/bsat/satSolver.c
@@ -2168,6 +2168,153 @@ 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
+        // if 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 );
+    nLitsL = nLits / 2;
+    nLitsR = nLits - nLitsL;
+    // 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] );
+    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];
+    // 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;
+}
+
+// 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 )
+    {
+        // 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
+        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 the problem is UNSAT, add clause
+        if ( status == l_False )
+        {
+            RetValue = sat_solver_addclause( s, &LitNot, &LitNot+1 );
+            assert( RetValue );
+        }
+
+        s->nConfLimit = Temp;
+        return (int)(status != l_False); // return 1 if the problem is not UNSAT
+    }
+    assert( nLits >= 2 );
+    nLitsL = nLits / 2;
+    nLitsR = nLits - nLitsL;
+    // 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);
+
+            // add clauses for these literal
+            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 );
+        }
+    // solve for the right lits
+    nResL = sat_solver_minimize_assumptions2( s, pLits + nLitsL, nLitsR, nConfLimit );
+    for ( i = 0; i < nLitsL; i++ )
+        sat_solver_pop(s);
+    // swap literals
+//    assert( nResL <= nLitsL );
+    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];
+    // 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);
+
+            // add clauses for these literal
+            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 );
+        }
+    // solve for the left lits
+    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_nvars(sat_solver* s)
 {
diff --git a/src/sat/bsat/satSolver.h b/src/sat/bsat/satSolver.h
index 5a8483c1..5191b2cd 100644
--- a/src/sat/bsat/satSolver.h
+++ b/src/sat/bsat/satSolver.h
@@ -50,6 +50,8 @@ 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_minimize_assumptions2( 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);
diff --git a/src/sat/satoko/clause.h b/src/sat/satoko/clause.h
index 2be18cd6..9b05868b 100644
--- a/src/sat/satoko/clause.h
+++ b/src/sat/satoko/clause.h
@@ -59,5 +59,19 @@ static inline void clause_print(struct clause *clause)
     printf("}\n");
 }
 
+static inline void clause_dump(FILE *file, struct clause *clause, int no_zero_var) 
+{
+    unsigned i;
+    for (i = 0; i < clause->size; i++) {
+        int var = (clause->data[i].lit >> 1);
+        char pol = (clause->data[i].lit & 1);
+        fprintf(file, "%d ", pol ? -(var + no_zero_var) : (var + no_zero_var));
+    }
+    if (no_zero_var)
+        fprintf(file, "0\n");
+    else
+        fprintf(file, "\n");
+}
+
 ABC_NAMESPACE_HEADER_END
 #endif /* satoko__clause_h */
diff --git a/src/sat/satoko/cnf_reader.c b/src/sat/satoko/cnf_reader.c
index adb9a47b..8223affd 100644
--- a/src/sat/satoko/cnf_reader.c
+++ b/src/sat/satoko/cnf_reader.c
@@ -150,7 +150,7 @@ int satoko_parse_dimacs(char *fname, satoko_t **solver)
     vec_uint_free(lits);
     satoko_free(buffer);
     *solver = p;
-    return satoko_simplify(p);
+    return SATOKO_OK;
 }
 
 ABC_NAMESPACE_IMPL_END
diff --git a/src/sat/satoko/satoko.h b/src/sat/satoko/satoko.h
index a0c4d216..6634e68e 100644
--- a/src/sat/satoko/satoko.h
+++ b/src/sat/satoko/satoko.h
@@ -60,6 +60,7 @@ struct satoko_opts {
     unsigned clause_min_lbd_bin_resol;
     float garbage_max_ratio;
     char verbose;
+    char no_simplify;
 };
 
 typedef struct satoko_stats satoko_stats_t;
@@ -108,6 +109,16 @@ extern void satoko_unbookmark(satoko_t *);
  */
 extern int satoko_final_conflict(satoko_t *, unsigned *);
 
+/* Procedure to dump a DIMACS file.
+ * - It receives as input the solver, a file name string and two integers.
+ * - If the file name string is NULL the solver will dump in stdout.
+ * - The first argument can be either 0 or 1 and is an option to dump learnt 
+ *   clauses. (value 1 will dump them).
+ * - The seccond argument can be either 0 or 1 and is an option to use 0 as a 
+ *   variable ID or not. Keep in mind that if 0 is used as an ID the generated
+ *   file will not be a DIMACS. (value 1 will use 0 as ID).
+ */
+extern void satoko_write_dimacs(satoko_t *, char *, int, int);
 extern satoko_stats_t satoko_stats(satoko_t *);
 
 ABC_NAMESPACE_HEADER_END
diff --git a/src/sat/satoko/solver.c b/src/sat/satoko/solver.c
index af3dcffb..42bc6448 100644
--- a/src/sat/satoko/solver.c
+++ b/src/sat/satoko/solver.c
@@ -644,7 +644,7 @@ char solver_search(solver_t *s)
                 solver_cancel_until(s, 0);
                 return SATOKO_UNDEC;
             }
-            if (solver_dlevel(s) == 0)
+            if (!s->opts.no_simplify && solver_dlevel(s) == 0)
                 satoko_simplify(s);
 
             /* Reduce the set of learnt clauses */
diff --git a/src/sat/satoko/solver_api.c b/src/sat/satoko/solver_api.c
index 3cb9f3d3..dada33cc 100644
--- a/src/sat/satoko/solver_api.c
+++ b/src/sat/satoko/solver_api.c
@@ -152,6 +152,7 @@ void satoko_default_opts(satoko_opts_t *opts)
 {
     memset(opts, 0, sizeof(satoko_opts_t));
     opts->verbose = 0;
+    opts->no_simplify = 0;
     /* Limits */
     opts->conf_limit = 0;
     opts->prop_limit  = 0;
@@ -290,6 +291,10 @@ int satoko_solve(solver_t *s)
     //if (s->opts.verbose)
     //    print_opts(s);
 
+    if (!s->opts.no_simplify)
+        if (satoko_simplify(s) != SATOKO_OK)
+            return SATOKO_UNDEC;
+
     while (status == SATOKO_UNDEC) {
         status = solver_search(s);
         if (solver_check_limits(s) == 0)
@@ -297,6 +302,7 @@ int satoko_solve(solver_t *s)
     }
     if (s->opts.verbose)
         print_stats(s);
+    
     solver_cancel_until(s, vec_uint_size(s->assumptions));
     return status;
 }
@@ -309,7 +315,6 @@ int satoko_final_conflict(solver_t *s, unsigned *out)
     memcpy(out, vec_uint_data(s->final_conflict),
            sizeof(unsigned) * vec_uint_size(s->final_conflict));
     return vec_uint_size(s->final_conflict);
-
 }
 
 satoko_stats_t satoko_stats(satoko_t *s)
@@ -324,6 +329,7 @@ void satoko_bookmark(satoko_t *s)
     s->book_cl_lrnt = vec_uint_size(s->learnts);
     s->book_vars = vec_char_size(s->assigns);
     s->book_trail = vec_uint_size(s->trail);
+    s->opts.no_simplify = 1;
 }
 
 void satoko_unbookmark(satoko_t *s)
@@ -333,6 +339,7 @@ void satoko_unbookmark(satoko_t *s)
     s->book_cdb = 0;
     s->book_vars = 0;
     s->book_trail = 0;
+    s->opts.no_simplify = 0;
 }
 
 void satoko_reset(satoko_t *s)
@@ -442,4 +449,43 @@ void satoko_unmark_cone(satoko_t *s, int *pvars, int n_vars)
         var_clean_mark(s, pvars[i]);
 }
 
+void satoko_write_dimacs(satoko_t *s, char *fname, int wrt_lrnt, int zero_var)
+{
+    FILE *file;
+    unsigned i;
+    unsigned n_vars = vec_act_size(s->activity);
+    unsigned n_orig = vec_uint_size(s->originals) + vec_uint_size(s->assumptions);
+    unsigned n_lrnts = vec_uint_size(s->learnts);
+    unsigned *array;
+
+    assert(wrt_lrnt == 0 || wrt_lrnt == 1);
+    assert(zero_var == 0 || zero_var == 1);
+    if (fname != NULL)
+        file = fopen(fname, "w");
+    else
+        file = stdout;
+    
+    if (file == NULL) {
+        printf( "Error: Cannot open output file.\n");
+        return;
+    }
+    fprintf(file, "p cnf %d %d\n", n_vars, wrt_lrnt ? n_orig + n_lrnts : n_orig);
+    array = vec_uint_data(s->assumptions);
+    for (i = 0; i < vec_uint_size(s->assumptions); i++)
+        fprintf(file, "%d\n", array[i] & 1 ? -(array[i] + !zero_var) : array[i] + !zero_var);
+    
+    array = vec_uint_data(s->originals);
+    for (i = 0; i < vec_uint_size(s->originals); i++)
+        clause_dump(file, clause_read(s, array[i]), !zero_var);
+    
+    if (wrt_lrnt) {
+        printf(" Lertns %u", n_lrnts);
+        array = vec_uint_data(s->learnts);
+        for (i = 0; i < n_lrnts; i++)
+            clause_dump(file, clause_read(s, array[i]), !zero_var);
+    }
+
+}
+
+
 ABC_NAMESPACE_IMPL_END