Adding support of candinality clause to the SAT solver.

1 files changed, 23 insertions, 2 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