Adding support of candinality clause to the SAT solver.

5 files changed, 52 insertions, 7 deletions

diff --git a/src/base/abci/abc.c b/src/base/abci/abc.c
index afa166fc..1b2e1e2c 100644
--- a/src/base/abci/abc.c
+++ b/src/base/abci/abc.c
@@ -22075,6 +22075,7 @@ int Abc_CommandDSat( Abc_Frame_t * pAbc, int argc, char ** argv )
     int fAndOuts;
     int fNewSolver;
     int fSilent;
+    int fShowPattern;
     int fVerbose;
     int nConfLimit;
     int nLearnedStart;
@@ -22096,7 +22097,7 @@ int Abc_CommandDSat( Abc_Frame_t * pAbc, int argc, char ** argv )
     nLearnedDelta = 0;
     nLearnedPerce = 0;
     Extra_UtilGetoptReset();
-    while ( ( c = Extra_UtilGetopt( argc, argv, "CILDEpansvh" ) ) != EOF )
+    while ( ( c = Extra_UtilGetopt( argc, argv, "CILDEpansvwh" ) ) != EOF )
     {
         switch ( c )
         {
@@ -22170,6 +22171,9 @@ int Abc_CommandDSat( Abc_Frame_t * pAbc, int argc, char ** argv )
         case 'v':
             fVerbose ^= 1;
             break;
+        case 'w':
+            fShowPattern ^= 1;
+            break;
         case 'h':
             goto usage;
         default:
@@ -22180,7 +22184,7 @@ int Abc_CommandDSat( Abc_Frame_t * pAbc, int argc, char ** argv )
     if ( argc == globalUtilOptind + 1 )
     {
         int * pModel = NULL;
-        extern int Cnf_DataSolveFromFile( char * pFileName, int nConfLimit, int nLearnedStart, int nLearnedDelta, int nLearnedPerce, int fVerbose, int ** ppModel, int nPis );
+        extern int Cnf_DataSolveFromFile( char * pFileName, int nConfLimit, int nLearnedStart, int nLearnedDelta, int nLearnedPerce, int fVerbose, int fShowPattern, int ** ppModel, int nPis );
         // get the input file name
         char * pFileName = argv[globalUtilOptind];
         FILE * pFile = fopen( pFileName, "rb" );
@@ -22190,7 +22194,7 @@ int Abc_CommandDSat( Abc_Frame_t * pAbc, int argc, char ** argv )
             return 0;
         }
         fclose( pFile );
-        Cnf_DataSolveFromFile( pFileName, nConfLimit, nLearnedStart, nLearnedDelta, nLearnedPerce, fVerbose, &pModel, pNtk ? Abc_NtkPiNum(pNtk) : 0 );
+        Cnf_DataSolveFromFile( pFileName, nConfLimit, nLearnedStart, nLearnedDelta, nLearnedPerce, fVerbose, fShowPattern, &pModel, pNtk ? Abc_NtkPiNum(pNtk) : 0 );
         if ( pModel && pNtk )
         {
             int * pSimInfo = Abc_NtkVerifySimulatePattern( pNtk, pModel );
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 );
diff --git a/src/sat/cnf/cnfUtil.c b/src/sat/cnf/cnfUtil.c
index 73bcd8a1..96002df8 100644
--- a/src/sat/cnf/cnfUtil.c
+++ b/src/sat/cnf/cnfUtil.c
@@ -399,7 +399,7 @@ finish:
   SeeAlso     []
 
 ***********************************************************************/
-int Cnf_DataSolveFromFile( char * pFileName, int nConfLimit, int nLearnedStart, int nLearnedDelta, int nLearnedPerce, int fVerbose, int ** ppModel, int nPis )
+int Cnf_DataSolveFromFile( char * pFileName, int nConfLimit, int nLearnedStart, int nLearnedDelta, int nLearnedPerce, int fVerbose, int fShowPattern, int ** ppModel, int nPis )
 {
     abctime clk = Abc_Clock();
     Cnf_Dat_t * pCnf = Cnf_DataReadFromFile( pFileName );
@@ -428,6 +428,9 @@ int Cnf_DataSolveFromFile( char * pFileName, int nConfLimit, int nLearnedStart,
         pSat->nLearntRatio = nLearnedPerce;
     if ( fVerbose )
         pSat->fVerbose = fVerbose;
+
+//sat_solver_start_cardinality( pSat, 100 );
+
     // solve the miter
     status = sat_solver_solve( pSat, NULL, NULL, (ABC_INT64_T)nConfLimit, 0, (ABC_INT64_T)0, (ABC_INT64_T)0 );
     if ( status == l_Undef )
@@ -455,6 +458,12 @@ int Cnf_DataSolveFromFile( char * pFileName, int nConfLimit, int nLearnedStart,
         for ( i = 0; i < nPis; i++ )
             (*ppModel)[i] = sat_solver_var_value( pSat, pCnf->nVars - nPis + i );
     }
+    if ( RetValue == 0 && fShowPattern )
+    {
+        for ( i = 0; i < pCnf->nVars; i++ )
+            printf( "%d", sat_solver_var_value(pSat,i) );
+        printf( "\n" );
+    }
     Cnf_DataFree( pCnf );
     sat_solver_delete( pSat );
     return RetValue;