Adding support of candinality clause to the SAT solver.

3 files changed, 35 insertions, 3 deletions

diff --git a/src/sat/bsat/satSolver.c b/src/sat/bsat/satSolver.c
index 24c60dac..1a10ff88 100644
--- a/src/sat/bsat/satSolver.c
+++ b/src/sat/bsat/satSolver.c
@@ -508,6 +508,12 @@ static inline int sat_solver_enqueue(sat_solver* s, lit l, int from)
         s->reasons[v] = from;
         s->trail[s->qtail++] = l;
         order_assigned(s, v);
+        // if cardinality clause is present, add positive literals
+        if ( s->cardinality && !lit_sign(l) && s->nCard >= (int)s->cardinality->size )
+        {
+//printf( "setting trail[%d] = %d\n", s->qtail-1, l );
+            s->cardinality->lits[s->nCard - s->cardinality->size++] = lit_neg(l);
+        }
         return true;
     }
 }
@@ -549,7 +555,15 @@ static void sat_solver_canceluntil(sat_solver* s, int level) {
         s->reasons[x] = 0;
         if ( c < lastLev )
             var_set_polar( s, x, !lit_sign(s->trail[c]) );
+        // if cardinality clause is present, remove positive
+        if ( s->cardinality && s->cardinality->lits[s->nCard+1 - s->cardinality->size] == lit_neg(s->trail[c]) )
+        {
+//printf( "undoing trail[%d] = %d\n", c, s->trail[c] );
+            assert( s->cardinality->size > 0 );
+            s->cardinality->size--;
+        }
     }
+    //printf( "\n" );
 
     for (c = s->qhead-1; c >= bound; c--)
         order_unassigned(s,lit_var(s->trail[c]));
@@ -781,7 +795,7 @@ static void sat_solver_analyze(sat_solver* s, int h, veci* learnt)
     lit      p       = lit_Undef;
     int      ind     = s->qtail-1;
     lit*     lits;
-    int      i, j, minl;
+    int      i, j, minl;// int hTemp = h;
     veci_push(learnt,lit_Undef);
     do{
         assert(h != 0);
@@ -796,7 +810,8 @@ static void sat_solver_analyze(sat_solver* s, int h, veci* learnt)
                     veci_push(learnt,clause_read_lit(h));
             }
         }else{
-            clause* c = clause_read(s, h);
+            clause* c = h == -2 ? s->cardinality : clause_read(s, h);
+            
             if (clause_learnt(c))
                 act_clause_bump(s,c);
             lits = clause_begin(c);
@@ -878,6 +893,8 @@ static void sat_solver_analyze(sat_solver* s, int h, veci* learnt)
         printf(" } at level %d\n", lev);
     }
 #endif
+//    if ( hTemp == -2 )
+//        printf( "%d ", veci_size(learnt) );
 }
 
 //#define TEST_CNF_LOAD
@@ -1183,6 +1200,7 @@ void sat_solver_delete(sat_solver* s)
     }
 
     sat_solver_store_free(s);
+    ABC_FREE(s->cardinality);
     ABC_FREE(s);
 }
 
@@ -1616,6 +1634,8 @@ static lbool sat_solver_search(sat_solver* s, ABC_INT64_T nof_conflicts)
 
     for (;;){
         int hConfl = sat_solver_propagate(s);
+        if ( hConfl == 0 && s->cardinality && (int)s->cardinality->size == s->nCard+1 )
+            hConfl = -2, s->nCardClauses++;
         if (hConfl != 0){
             // CONFLICT
             int blevel;
@@ -1898,6 +1918,7 @@ int sat_solver_solve(sat_solver* s, lit* begin, lit* end, ABC_INT64_T nConfLimit
             fflush(stdout);
         }
         nof_conflicts = (ABC_INT64_T)( 100 * luby(2, restart_iter++) );
+//        assert( s->cardinality->size == 0 );
         status = sat_solver_search(s, nof_conflicts);
 //        nof_learnts    = nof_learnts * 11 / 10; //*= 1.1;
         // quit the loop if reached an external limit
diff --git a/src/sat/bsat/satSolver.h b/src/sat/bsat/satSolver.h
index 89391d2d..f1738eb5 100644
--- a/src/sat/bsat/satSolver.h
+++ b/src/sat/bsat/satSolver.h
@@ -100,6 +100,9 @@ struct sat_solver_t
     int         hLearnts;      // the first learnt clause
     int         hBinary;       // the special binary clause
     clause *    binary;
+    clause *    cardinality;   // cardinality clause
+    int         nCard;         // cardinality size
+    int         nCardClauses;  // cardinality conflicts
     veci*       wlists;        // watcher lists
     veci        act_clas;      // contain clause activities
 
@@ -291,7 +294,13 @@ static inline int sat_solver_count_usedvars(sat_solver* s)
         }
     return nVars;
 }
-
+static inline void sat_solver_start_cardinality(sat_solver* s, int nSize)
+{
+    assert( s->cardinality == NULL );
+    s->cardinality = (clause*)ABC_CALLOC(int, nSize+2);
+    s->nCard = nSize;
+    s->nCardClauses = 0;
+}
 static inline int sat_solver_add_const( sat_solver * pSat, int iVar, int fCompl )
 {
     lit Lits[1];
diff --git a/src/sat/bsat/satUtil.c b/src/sat/bsat/satUtil.c
index f1f03ce2..188c308b 100644
--- a/src/sat/bsat/satUtil.c
+++ b/src/sat/bsat/satUtil.c
@@ -195,6 +195,8 @@ void Sat_SolverPrintStats( FILE * pFile, sat_solver * p )
 //    printf( "calls         : %10d (%d)\n", (int)p->nCalls, (int)p->nCalls2 );
     printf( "starts        : %16.0f\n", Sat_Wrd2Dbl(p->stats.starts) );
     printf( "conflicts     : %16.0f\n", Sat_Wrd2Dbl(p->stats.conflicts) );
+    if ( p->nCardClauses )
+    printf( "conflictsCard : %16.0f\n", Sat_Wrd2Dbl((word)p->nCardClauses) );
     printf( "decisions     : %16.0f\n", Sat_Wrd2Dbl(p->stats.decisions) );
     printf( "propagations  : %16.0f\n", Sat_Wrd2Dbl(p->stats.propagations) );
 //    printf( "inspects      : %10d\n", (int)p->stats.inspects );