Started experiments with a new solver.

abclib.dsp

@@ -1275,6 +1275,14 @@ SOURCE=.\src\sat\bsat\satSolver.h
 # End Source File
 # Begin Source File
 
+SOURCE=.\src\sat\bsat\satSolver2.c
+# End Source File
+# Begin Source File
+
+SOURCE=.\src\sat\bsat\satSolver2.h
+# End Source File
+# Begin Source File
+
 SOURCE=.\src\sat\bsat\satStore.c
 # End Source File
 # Begin Source File

src/aig/cnf/cnfMan.c

@@ -20,6 +20,7 @@
 
 #include "cnf.h"
 #include "satSolver.h"
+#include "satSolver2.h"
 #include "zlib.h"
 
 ABC_NAMESPACE_IMPL_START
@@ -416,6 +417,98 @@ void * Cnf_DataWriteIntoSolver( Cnf_Dat_t * p, int nFrames, int fInit )
 
 /**Function*************************************************************
 
+  Synopsis    [Writes CNF into a file.]
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+void * Cnf_DataWriteIntoSolver2( Cnf_Dat_t * p, int nFrames, int fInit )
+{
+    sat_solver2 * pSat;
+    int i, f, status;
+    assert( nFrames > 0 );
+    pSat = sat_solver2_new();
+    sat_solver2_setnvars( pSat, p->nVars * nFrames );
+    for ( i = 0; i < p->nClauses; i++ )
+    {
+        if ( !sat_solver2_addclause( pSat, p->pClauses[i], p->pClauses[i+1] ) )
+        {
+            sat_solver2_delete( pSat );
+            return NULL;
+        }
+    }
+    if ( nFrames > 1 )
+    {
+        Aig_Obj_t * pObjLo, * pObjLi;
+        int nLitsAll, * pLits, Lits[2];
+        nLitsAll = 2 * p->nVars;
+        pLits = p->pClauses[0];
+        for ( f = 1; f < nFrames; f++ )
+        {
+            // add equality of register inputs/outputs for different timeframes
+            Aig_ManForEachLiLoSeq( p->pMan, pObjLi, pObjLo, i )
+            {
+                Lits[0] = (f-1)*nLitsAll + toLitCond( p->pVarNums[pObjLi->Id], 0 );
+                Lits[1] =  f   *nLitsAll + toLitCond( p->pVarNums[pObjLo->Id], 1 );
+                if ( !sat_solver2_addclause( pSat, Lits, Lits + 2 ) )
+                {
+                    sat_solver2_delete( pSat );
+                    return NULL;
+                }
+                Lits[0]++;
+                Lits[1]--;
+                if ( !sat_solver2_addclause( pSat, Lits, Lits + 2 ) )
+                {
+                    sat_solver2_delete( pSat );
+                    return NULL;
+                }
+            }
+            // add clauses for the next timeframe
+            for ( i = 0; i < p->nLiterals; i++ )
+                pLits[i] += nLitsAll;
+            for ( i = 0; i < p->nClauses; i++ )
+            {
+                if ( !sat_solver2_addclause( pSat, p->pClauses[i], p->pClauses[i+1] ) )
+                {
+                    sat_solver2_delete( pSat );
+                    return NULL;
+                }
+            }
+        }
+        // return literals to their original state
+        nLitsAll = (f-1) * nLitsAll;
+        for ( i = 0; i < p->nLiterals; i++ )
+            pLits[i] -= nLitsAll;
+    }
+    if ( fInit )
+    {
+        Aig_Obj_t * pObjLo;
+        int Lits[1];
+        Aig_ManForEachLoSeq( p->pMan, pObjLo, i )
+        {
+            Lits[0] = toLitCond( p->pVarNums[pObjLo->Id], 1 );
+            if ( !sat_solver2_addclause( pSat, Lits, Lits + 1 ) )
+            {
+                sat_solver2_delete( pSat );
+                return NULL;
+            }
+        }
+    }
+    status = sat_solver2_simplify(pSat);
+    if ( status == 0 )
+    {
+        sat_solver2_delete( pSat );
+        return NULL;
+    }
+    return pSat;
+}
+
+/**Function*************************************************************
+
   Synopsis    [Adds the OR-clause.]
 
   Description []
@@ -453,6 +546,34 @@ int Cnf_DataWriteOrClause( void * p, Cnf_Dat_t * pCnf )
   SeeAlso     []
 
 ***********************************************************************/
+int Cnf_DataWriteOrClause2( void * p, Cnf_Dat_t * pCnf )
+{
+    sat_solver2 * pSat = (sat_solver2 *)p;
+    Aig_Obj_t * pObj;
+    int i, * pLits;
+    pLits = ABC_ALLOC( int, Aig_ManPoNum(pCnf->pMan) );
+    Aig_ManForEachPo( pCnf->pMan, pObj, i )
+        pLits[i] = toLitCond( pCnf->pVarNums[pObj->Id], 0 );
+    if ( !sat_solver2_addclause( pSat, pLits, pLits + Aig_ManPoNum(pCnf->pMan) ) )
+    {
+        ABC_FREE( pLits );
+        return 0;
+    }
+    ABC_FREE( pLits );
+    return 1;
+}
+
+/**Function*************************************************************
+
+  Synopsis    [Adds the OR-clause.]
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
 int Cnf_DataWriteAndClauses( void * p, Cnf_Dat_t * pCnf )
 {
     sat_solver * pSat = (sat_solver *)p;

src/aig/fra/fra.h

@@ -286,7 +286,7 @@ static inline int          Fra_ImpCreate( int Left, int Right )
 ////////////////////////////////////////////////////////////////////////
 
 /*=== fraCec.c ========================================================*/
-extern int                 Fra_FraigSat( Aig_Man_t * pMan, ABC_INT64_T nConfLimit, ABC_INT64_T nInsLimit, int fFlipBits, int fAndOuts, int fVerbose );
+extern int                 Fra_FraigSat( Aig_Man_t * pMan, ABC_INT64_T nConfLimit, ABC_INT64_T nInsLimit, int fFlipBits, int fAndOuts, int fNewSolver, int fVerbose );
 extern int                 Fra_FraigCec( Aig_Man_t ** ppAig, int nConfLimit, int fVerbose );
 extern int                 Fra_FraigCecPartitioned( Aig_Man_t * pMan1, Aig_Man_t * pMan2, int nConfLimit, int nPartSize, int fSmart, int fVerbose );
 /*=== fraClass.c ========================================================*/

src/aig/fra/fraCec.c

@@ -20,6 +20,7 @@
 
 #include "fra.h"
 #include "cnf.h"
+#include "satSolver2.h"
 
 ABC_NAMESPACE_IMPL_START
 
@@ -43,8 +44,119 @@ ABC_NAMESPACE_IMPL_START
   SeeAlso     []
 
 ***********************************************************************/
-int Fra_FraigSat( Aig_Man_t * pMan, ABC_INT64_T nConfLimit, ABC_INT64_T nInsLimit, int fFlipBits, int fAndOuts, int fVerbose )
+int Fra_FraigSat( Aig_Man_t * pMan, ABC_INT64_T nConfLimit, ABC_INT64_T nInsLimit, int fFlipBits, int fAndOuts, int fNewSolver, int fVerbose )
 {
+    if ( fNewSolver )
+    {
+        extern void * Cnf_DataWriteIntoSolver2( Cnf_Dat_t * p, int nFrames, int fInit );
+        extern int    Cnf_DataWriteOrClause2( void * pSat, Cnf_Dat_t * pCnf );
+
+        sat_solver2 * pSat;
+        Cnf_Dat_t * pCnf;
+        int status, RetValue, clk = clock();
+        Vec_Int_t * vCiIds;
+
+        assert( Aig_ManRegNum(pMan) == 0 );
+        pMan->pData = NULL;
+
+        // derive CNF
+        pCnf = Cnf_Derive( pMan, Aig_ManPoNum(pMan) );
+    //    pCnf = Cnf_DeriveSimple( pMan, Aig_ManPoNum(pMan) );
+
+        if ( fFlipBits ) 
+            Cnf_DataTranformPolarity( pCnf, 0 );
+
+        // convert into SAT solver
+        pSat = (sat_solver2 *)Cnf_DataWriteIntoSolver2( pCnf, 1, 0 );
+        if ( pSat == NULL )
+        {
+            Cnf_DataFree( pCnf );
+            return 1;
+        }
+
+
+        if ( fAndOuts )
+        {
+            // assert each output independently
+            if ( !Cnf_DataWriteAndClauses( pSat, pCnf ) )
+            {
+                sat_solver2_delete( pSat );
+                Cnf_DataFree( pCnf );
+                return 1;
+            }
+        }
+        else
+        {
+            // add the OR clause for the outputs
+            if ( !Cnf_DataWriteOrClause2( pSat, pCnf ) )
+            {
+                sat_solver2_delete( pSat );
+                Cnf_DataFree( pCnf );
+                return 1;
+            }
+        }
+        vCiIds = Cnf_DataCollectPiSatNums( pCnf, pMan );
+        Cnf_DataFree( pCnf );
+
+
+        printf( "Created SAT problem with %d variable and %d clauses. ", sat_solver2_nvars(pSat), sat_solver2_nclauses(pSat) );
+        ABC_PRT( "Time", clock() - clk );
+
+        // simplify the problem
+        clk = clock();
+        status = sat_solver2_simplify(pSat);
+        printf( "Simplified the problem to %d variables and %d clauses. ", sat_solver2_nvars(pSat), sat_solver2_nclauses(pSat) );
+        ABC_PRT( "Time", clock() - clk );
+        if ( status == 0 )
+        {
+            Vec_IntFree( vCiIds );
+            sat_solver2_delete( pSat );
+    //        printf( "The problem is UNSATISFIABLE after simplification.\n" );
+            return 1;
+        }
+
+        // solve the miter
+        clk = clock();
+        if ( fVerbose )
+            pSat->verbosity = 1;
+        status = sat_solver2_solve( pSat, NULL, NULL, (ABC_INT64_T)nConfLimit, (ABC_INT64_T)nInsLimit, (ABC_INT64_T)0, (ABC_INT64_T)0 );
+        if ( status == l_Undef )
+        {
+    //        printf( "The problem timed out.\n" );
+            RetValue = -1;
+        }
+        else if ( status == l_True )
+        {
+    //        printf( "The problem is SATISFIABLE.\n" );
+            RetValue = 0;
+        }
+        else if ( status == l_False )
+        {
+    //        printf( "The problem is UNSATISFIABLE.\n" );
+            RetValue = 1;
+        }
+        else
+            assert( 0 );
+
+    //    Abc_Print( 1, "The number of conflicts = %6d.  ", (int)pSat->stats.conflicts );
+    //    Abc_PrintTime( 1, "Solving time", clock() - clk );
+ 
+        // if the problem is SAT, get the counterexample
+        if ( status == l_True )
+        {
+            pMan->pData = Sat_Solver2GetModel( pSat, vCiIds->pArray, vCiIds->nSize );
+        }
+        // free the sat_solver2
+//        if ( fVerbose )
+            Sat_Solver2PrintStats( stdout, pSat );
+    //sat_solver2_store_write( pSat, "trace.cnf" );
+    //sat_solver2_store_free( pSat );
+        sat_solver2_delete( pSat );
+        Vec_IntFree( vCiIds );
+        return RetValue;
+    }
+    else
+    {
         sat_solver * pSat;
         Cnf_Dat_t * pCnf;
         int status, RetValue, clk = clock();
@@ -55,7 +167,7 @@ int Fra_FraigSat( Aig_Man_t * pMan, ABC_INT64_T nConfLimit, ABC_INT64_T nInsLimi
 
         // derive CNF
         pCnf = Cnf_Derive( pMan, Aig_ManPoNum(pMan) );
-//    pCnf = Cnf_DeriveSimple( pMan, Aig_ManPoNum(pMan) );
+    //    pCnf = Cnf_DeriveSimple( pMan, Aig_ManPoNum(pMan) );
 
         if ( fFlipBits ) 
             Cnf_DataTranformPolarity( pCnf, 0 );
@@ -93,19 +205,19 @@ int Fra_FraigSat( Aig_Man_t * pMan, ABC_INT64_T nConfLimit, ABC_INT64_T nInsLimi
         Cnf_DataFree( pCnf );
 
 
-//    printf( "Created SAT problem with %d variable and %d clauses. ", sat_solver_nvars(pSat), sat_solver_nclauses(pSat) );
-//    ABC_PRT( "Time", clock() - clk );
+    //    printf( "Created SAT problem with %d variable and %d clauses. ", sat_solver_nvars(pSat), sat_solver_nclauses(pSat) );
+    //    ABC_PRT( "Time", clock() - clk );
 
         // simplify the problem
         clk = clock();
         status = sat_solver_simplify(pSat);
-//    printf( "Simplified the problem to %d variables and %d clauses. ", sat_solver_nvars(pSat), sat_solver_nclauses(pSat) );
-//    ABC_PRT( "Time", clock() - clk );
+    //    printf( "Simplified the problem to %d variables and %d clauses. ", sat_solver_nvars(pSat), sat_solver_nclauses(pSat) );
+    //    ABC_PRT( "Time", clock() - clk );
         if ( status == 0 )
         {
             Vec_IntFree( vCiIds );
             sat_solver_delete( pSat );
-//        printf( "The problem is UNSATISFIABLE after simplification.\n" );
+    //        printf( "The problem is UNSATISFIABLE after simplification.\n" );
             return 1;
         }
 
@@ -116,24 +228,24 @@ int Fra_FraigSat( Aig_Man_t * pMan, ABC_INT64_T nConfLimit, ABC_INT64_T nInsLimi
         status = sat_solver_solve( pSat, NULL, NULL, (ABC_INT64_T)nConfLimit, (ABC_INT64_T)nInsLimit, (ABC_INT64_T)0, (ABC_INT64_T)0 );
         if ( status == l_Undef )
         {
-//        printf( "The problem timed out.\n" );
+    //        printf( "The problem timed out.\n" );
             RetValue = -1;
         }
         else if ( status == l_True )
         {
-//        printf( "The problem is SATISFIABLE.\n" );
+    //        printf( "The problem is SATISFIABLE.\n" );
             RetValue = 0;
         }
         else if ( status == l_False )
         {
-//        printf( "The problem is UNSATISFIABLE.\n" );
+    //        printf( "The problem is UNSATISFIABLE.\n" );
             RetValue = 1;
         }
         else
             assert( 0 );
 
-//    Abc_Print( 1, "The number of conflicts = %6d.  ", (int)pSat->stats.conflicts );
-//    Abc_PrintTime( 1, "Solving time", clock() - clk );
+    //    Abc_Print( 1, "The number of conflicts = %6d.  ", (int)pSat->stats.conflicts );
+    //    Abc_PrintTime( 1, "Solving time", clock() - clk );
  
         // if the problem is SAT, get the counterexample
         if ( status == l_True )
@@ -141,13 +253,14 @@ int Fra_FraigSat( Aig_Man_t * pMan, ABC_INT64_T nConfLimit, ABC_INT64_T nInsLimi
             pMan->pData = Sat_SolverGetModel( pSat, vCiIds->pArray, vCiIds->nSize );
         }
         // free the sat_solver
-    if ( fVerbose )
+//        if ( fVerbose )
             Sat_SolverPrintStats( stdout, pSat );
-//sat_solver_store_write( pSat, "trace.cnf" );
-//sat_solver_store_free( pSat );
+    //sat_solver_store_write( pSat, "trace.cnf" );
+    //sat_solver_store_free( pSat );
         sat_solver_delete( pSat );
         Vec_IntFree( vCiIds );
         return RetValue;
+    }
 }
 
 /**Function*************************************************************
@@ -187,7 +300,7 @@ int Fra_FraigCec( Aig_Man_t ** ppAig, int nConfLimit, int fVerbose )
 
     // if SAT only, solve without iteration
 clk = clock();
-    RetValue = Fra_FraigSat( pAig, (ABC_INT64_T)2*nBTLimitStart, (ABC_INT64_T)0, 1, 0, 0 );
+    RetValue = Fra_FraigSat( pAig, (ABC_INT64_T)2*nBTLimitStart, (ABC_INT64_T)0, 1, 0, 0, 0 );
     if ( fVerbose )
     {
         printf( "Initial SAT:      Nodes = %6d.  ", Aig_ManNodeNum(pAig) );
@@ -255,7 +368,7 @@ ABC_PRT( "Time", clock() - clk );
     if ( RetValue == -1 )
     {
 clk = clock();
-        RetValue = Fra_FraigSat( pAig, (ABC_INT64_T)nBTLimitLast, (ABC_INT64_T)0, 1, 0, 0 );
+        RetValue = Fra_FraigSat( pAig, (ABC_INT64_T)nBTLimitLast, (ABC_INT64_T)0, 1, 0, 0, 0 );
         if ( fVerbose )
         {
             printf( "Final SAT:            Nodes = %6d.  ", Aig_ManNodeNum(pAig) );

src/aig/gia/giaAig.c

@@ -568,11 +568,11 @@ void Gia_ManSeqCleanupClasses( Gia_Man_t * p, int fConst, int fEquiv, int fVerbo
 ***********************************************************************/
 int Gia_ManSolveSat( Gia_Man_t * p )
 {
-//    extern int Fra_FraigSat( Aig_Man_t * pMan, ABC_INT64_T nConfLimit, ABC_INT64_T nInsLimit, int fFlipBits, int fAndOuts, int fVerbose );
+//    extern int Fra_FraigSat( Aig_Man_t * pMan, ABC_INT64_T nConfLimit, ABC_INT64_T nInsLimit, int fFlipBits, int fAndOuts, int fNewSolver, int fVerbose );
     Aig_Man_t * pNew;
     int RetValue, clk = clock();
     pNew = Gia_ManToAig( p, 0 );
-    RetValue = Fra_FraigSat( pNew, 10000000, 0, 1, 1, 0 );
+    RetValue = Fra_FraigSat( pNew, 10000000, 0, 1, 1, 0, 0 );
     if ( RetValue == 0 )
     {
         Gia_Obj_t * pObj;

src/aig/int/intContain.c

@@ -57,7 +57,7 @@ int Inter_ManCheckContainment( Aig_Man_t * pNew, Aig_Man_t * pOld )
         pAigTemp = Fra_FraigEquivence( pMiter, 1000000, 1 );
         RetValue = Fra_FraigMiterStatus( pAigTemp );
         Aig_ManStop( pAigTemp );
-//        RetValue = Fra_FraigSat( pMiter, 1000000, 0, 0, 0 );
+//        RetValue = Fra_FraigSat( pMiter, 1000000, 0, 0, 0, 0 );
     }
     assert( RetValue != -1 );
     Aig_ManStop( pMiter );
@@ -88,7 +88,7 @@ int Inter_ManCheckEquivalence( Aig_Man_t * pNew, Aig_Man_t * pOld )
         pAigTemp = Fra_FraigEquivence( pMiter, 1000000, 1 );
         RetValue = Fra_FraigMiterStatus( pAigTemp );
         Aig_ManStop( pAigTemp );
-//        RetValue = Fra_FraigSat( pMiter, 1000000, 0, 0, 0 );
+//        RetValue = Fra_FraigSat( pMiter, 1000000, 0, 0, 0, 0 );
     }
     assert( RetValue != -1 );
     Aig_ManStop( pMiter );

src/aig/ivy/ivyFraig.c

@@ -2907,14 +2907,14 @@ printf( "***************\n" );
 ***********************************************************************/
 int Ivy_FraigCheckCone( Ivy_FraigMan_t * pGlo, Ivy_Man_t * p, Ivy_Obj_t * pObj1, Ivy_Obj_t * pObj2, int nConfLimit )
 {
-    extern int Fra_FraigSat( Aig_Man_t * pMan, ABC_INT64_T nConfLimit, ABC_INT64_T nInsLimit, int fFlipBits, int fAndOuts, int fVerbose );
+    extern int Fra_FraigSat( Aig_Man_t * pMan, ABC_INT64_T nConfLimit, ABC_INT64_T nInsLimit, int fFlipBits, int fAndOuts, int fNewSolver, int fVerbose );
     Vec_Int_t * vLeaves;
     Aig_Man_t * pMan;
     Aig_Obj_t * pObj;
     int i, RetValue;
     vLeaves  = Vec_IntAlloc( 100 );
     pMan     = Ivy_FraigExtractCone( p, pObj1, pObj2, vLeaves );
-    RetValue = Fra_FraigSat( pMan, nConfLimit, 0, 0, 0, 1 ); 
+    RetValue = Fra_FraigSat( pMan, nConfLimit, 0, 0, 0, 0, 1 ); 
     if ( RetValue == 0 )
     {
         int Counter = 0;

src/aig/saig/saigGlaPba.c

@@ -558,6 +558,7 @@ Vec_Int_t * Aig_Gla2ManPerform( Aig_Man_t * pAig, int nStart, int nFramesMax, in
     Aig_Gla2Man_t * p;
     Vec_Int_t * vCore, * vResult;
     int nTimeToStop = time(NULL) + TimeLimit;
+    int clk, clk2 = clock();
     assert( Saig_ManPoNum(pAig) == 1 );
 
     Abc_Clock(0,1); 
@@ -570,6 +571,7 @@ Vec_Int_t * Aig_Gla2ManPerform( Aig_Man_t * pAig, int nStart, int nFramesMax, in
     }
 
     // start the solver
+    clk = clock();
     Abc_Clock(1,1); 
     p = Aig_Gla2ManStart( pAig, nStart, nFramesMax, fVerbose );
     if ( !Aig_Gla2CreateSatSolver( p ) )
@@ -579,13 +581,15 @@ Vec_Int_t * Aig_Gla2ManPerform( Aig_Man_t * pAig, int nStart, int nFramesMax, in
         return NULL;
     }
     sat_solver_set_random( p->pSat, fSkipRand );
-    p->timePre += (Abc_Clock(1,0)/ABC_CPS)*CLOCKS_PER_SEC;
+//    p->timePre += (Abc_Clock(1,0)/ABC_CPS)*CLOCKS_PER_SEC;
+    p->timePre += clock() - clk;
 
     // set runtime limit
     if ( TimeLimit )
         sat_solver_set_runtime_limit( p->pSat, nTimeToStop );
 
     // compute UNSAT core
+    clk = clock();
     Abc_Clock(1,1); 
     vCore = Saig_AbsSolverUnsatCore( p->pSat, nConfLimit, fVerbose, NULL );
     if ( vCore == NULL )
@@ -593,8 +597,10 @@ Vec_Int_t * Aig_Gla2ManPerform( Aig_Man_t * pAig, int nStart, int nFramesMax, in
         Aig_Gla2ManStop( p );
         return NULL;
     }
-    p->timeSat += (Abc_Clock(1,0)/ABC_CPS)*CLOCKS_PER_SEC;
-    p->timeTotal = (Abc_Clock(0,0)/ABC_CPS)*CLOCKS_PER_SEC;
+//    p->timeSat += (Abc_Clock(1,0)/ABC_CPS)*CLOCKS_PER_SEC;
+//    p->timeTotal = (Abc_Clock(0,0)/ABC_CPS)*CLOCKS_PER_SEC;
+    p->timeSat += clock() - clk;
+    p->timeTotal += clock() - clk2;
 
     // print stats
     if ( fVerbose )

src/base/abci/abc.c

@@ -17038,7 +17038,7 @@ int Abc_CommandDCec( Abc_Frame_t * pAbc, int argc, char ** argv )
     int fPartition;
     int fMiter;
 
-    extern int Abc_NtkDSat( Abc_Ntk_t * pNtk, ABC_INT64_T nConfLimit, ABC_INT64_T nInsLimit, int fAlignPol, int fAndOuts, int fVerbose );
+    extern int Abc_NtkDSat( Abc_Ntk_t * pNtk, ABC_INT64_T nConfLimit, ABC_INT64_T nInsLimit, int fAlignPol, int fAndOuts, int fNewSolver, int fVerbose );
     extern int Abc_NtkDarCec( Abc_Ntk_t * pNtk1, Abc_Ntk_t * pNtk2, int nConfLimit, int fPartition, int fVerbose );
 
     pNtk = Abc_FrameReadNtk(pAbc);
@@ -17143,7 +17143,7 @@ int Abc_CommandDCec( Abc_Frame_t * pAbc, int argc, char ** argv )
 
     // perform equivalence checking
     if ( fSat && fMiter )
-        Abc_NtkDSat( pNtk1, nConfLimit, nInsLimit, 0, 0, fVerbose );
+        Abc_NtkDSat( pNtk1, nConfLimit, nInsLimit, 0, 0, 0, fVerbose );
     else
         Abc_NtkDarCec( pNtk1, pNtk2, nConfLimit, fPartition, fVerbose );
 
@@ -18250,20 +18250,22 @@ int Abc_CommandDSat( Abc_Frame_t * pAbc, int argc, char ** argv )
     int RetValue;
     int fAlignPol;
     int fAndOuts;
+    int fNewSolver;
     int fVerbose;
     int nConfLimit;
     int nInsLimit;
     int clk;
 
-    extern int Abc_NtkDSat( Abc_Ntk_t * pNtk, ABC_INT64_T nConfLimit, ABC_INT64_T nInsLimit, int fAlignPol, int fAndOuts, int fVerbose );
+    extern int Abc_NtkDSat( Abc_Ntk_t * pNtk, ABC_INT64_T nConfLimit, ABC_INT64_T nInsLimit, int fAlignPol, int fAndOuts, int fNewSolver, int fVerbose );
     // set defaults
     fAlignPol  = 0;
     fAndOuts   = 0;
+    fNewSolver = 0;
     fVerbose   = 0;
     nConfLimit = 100000;   
     nInsLimit  = 0;
     Extra_UtilGetoptReset();
-    while ( ( c = Extra_UtilGetopt( argc, argv, "CIpavh" ) ) != EOF )
+    while ( ( c = Extra_UtilGetopt( argc, argv, "CIpanvh" ) ) != EOF )
     {
         switch ( c )
         {
@@ -18295,6 +18297,9 @@ int Abc_CommandDSat( Abc_Frame_t * pAbc, int argc, char ** argv )
         case 'a':
             fAndOuts ^= 1;
             break;
+        case 'n':
+            fNewSolver ^= 1;
+            break;
         case 'v':
             fVerbose ^= 1;
             break;
@@ -18329,7 +18334,7 @@ int Abc_CommandDSat( Abc_Frame_t * pAbc, int argc, char ** argv )
     }
 
     clk = clock();
-    RetValue = Abc_NtkDSat( pNtk, (ABC_INT64_T)nConfLimit, (ABC_INT64_T)nInsLimit, fAlignPol, fAndOuts, fVerbose );
+    RetValue = Abc_NtkDSat( pNtk, (ABC_INT64_T)nConfLimit, (ABC_INT64_T)nInsLimit, fAlignPol, fAndOuts, fNewSolver, fVerbose );
     // verify that the pattern is correct
     if ( RetValue == 0 && Abc_NtkPoNum(pNtk) == 1 )
     {
@@ -18351,13 +18356,14 @@ int Abc_CommandDSat( Abc_Frame_t * pAbc, int argc, char ** argv )
     return 0;
 
 usage:
-    Abc_Print( -2, "usage: dsat [-C num] [-I num] [-pavh]\n" );
+    Abc_Print( -2, "usage: dsat [-C num] [-I num] [-panvh]\n" );
     Abc_Print( -2, "\t         solves the combinational miter using SAT solver MiniSat-1.14\n" );
     Abc_Print( -2, "\t         derives CNF from the current network and leave it unchanged\n" );
     Abc_Print( -2, "\t-C num : limit on the number of conflicts [default = %d]\n",    nConfLimit );
     Abc_Print( -2, "\t-I num : limit on the number of inspections [default = %d]\n", nInsLimit );
     Abc_Print( -2, "\t-p     : alighn polarity of SAT variables [default = %s]\n", fAlignPol? "yes": "no" );  
     Abc_Print( -2, "\t-a     : toggle ANDing/ORing of miter outputs [default = %s]\n", fAndOuts? "ANDing": "ORing" );  
+    Abc_Print( -2, "\t-n     : toggle using new solver [default = %s]\n", fNewSolver? "yes": "no" );  
     Abc_Print( -2, "\t-v     : prints verbose information [default = %s]\n", fVerbose? "yes": "no" );  
     Abc_Print( -2, "\t-h     : print the command usage\n");
     return 1;

src/base/abci/abcDar.c

@@ -1240,7 +1240,7 @@ Abc_Ntk_t * Abc_NtkDarToCnf( Abc_Ntk_t * pNtk, char * pFileName, int fFastAlgo,
   SeeAlso     []
 
 ***********************************************************************/
-int Abc_NtkDSat( Abc_Ntk_t * pNtk, ABC_INT64_T nConfLimit, ABC_INT64_T nInsLimit, int fAlignPol, int fAndOuts, int fVerbose )
+int Abc_NtkDSat( Abc_Ntk_t * pNtk, ABC_INT64_T nConfLimit, ABC_INT64_T nInsLimit, int fAlignPol, int fAndOuts, int fNewSolver, int fVerbose )
 {
     Aig_Man_t * pMan;
     int RetValue;//, clk = clock();
@@ -1248,7 +1248,7 @@ int Abc_NtkDSat( Abc_Ntk_t * pNtk, ABC_INT64_T nConfLimit, ABC_INT64_T nInsLimit
     assert( Abc_NtkLatchNum(pNtk) == 0 );
 //    assert( Abc_NtkPoNum(pNtk) == 1 );
     pMan = Abc_NtkToDar( pNtk, 0, 0 );
-    RetValue = Fra_FraigSat( pMan, nConfLimit, nInsLimit, fAlignPol, fAndOuts, fVerbose ); 
+    RetValue = Fra_FraigSat( pMan, nConfLimit, nInsLimit, fAlignPol, fAndOuts, fNewSolver, fVerbose ); 
     pNtk->pModel = (int *)pMan->pData, pMan->pData = NULL;
     Aig_ManStop( pMan );
     return RetValue;
@@ -1910,7 +1910,7 @@ int Abc_NtkDarBmcInter_int( Aig_Man_t * pMan, Inter_ManParams_t * pPars, Aig_Man
             if ( Aig_ManRegNum(pTemp) == 0 )
             {
                 pTemp->pSeqModel = NULL;
-                RetValue = Fra_FraigSat( pTemp, pPars->nBTLimit, 0, 0, 0, 0 ); 
+                RetValue = Fra_FraigSat( pTemp, pPars->nBTLimit, 0, 0, 0, 0, 0 ); 
                 if ( pTemp->pData )
                     pTemp->pSeqModel = Abc_CexCreate( Aig_ManRegNum(pMan), Saig_ManPiNum(pMan), (int *)pTemp->pData, 0, i, 1 );
 //                pNtk->pModel = pTemp->pData, pTemp->pData = NULL;

src/base/abci/abcIvy.c

@@ -30,7 +30,7 @@ ABC_NAMESPACE_IMPL_START
 
 extern Aig_Man_t * Abc_NtkToDar( Abc_Ntk_t * pNtk, int fExors, int fRegisters );
 extern void   Aig_ManStop( Aig_Man_t * pMan );
-//extern int Fra_FraigSat( Aig_Man_t * pMan, ABC_INT64_T nConfLimit, ABC_INT64_T nInsLimit, int fFlipBits, int fAndOuts, int fVerbose );
+//extern int Fra_FraigSat( Aig_Man_t * pMan, ABC_INT64_T nConfLimit, ABC_INT64_T nInsLimit, int fFlipBits, int fAndOuts, int fNewSolver, int fVerbose );
 extern Ivy_Obj_t * Dec_GraphToNetworkIvy( Ivy_Man_t * pMan, Dec_Graph_t * pGraph );
 extern void Ivy_CutComputeAll( Ivy_Man_t * p, int nInputs );
 
@@ -532,7 +532,7 @@ int Abc_NtkIvyProve( Abc_Ntk_t ** ppNtk, void * pPars )
     // if SAT only, solve without iteration
 //    RetValue = Abc_NtkMiterSat( pNtk, 2*(ABC_INT64_T)pParams->nMiteringLimitStart, (ABC_INT64_T)0, 0, NULL, NULL );
     pMan2 = Abc_NtkToDar( pNtk, 0, 0 );
-    RetValue = Fra_FraigSat( pMan2, (ABC_INT64_T)pParams->nMiteringLimitStart, (ABC_INT64_T)0, 1, 0, 0 ); 
+    RetValue = Fra_FraigSat( pMan2, (ABC_INT64_T)pParams->nMiteringLimitStart, (ABC_INT64_T)0, 1, 0, 0, 0 ); 
     pNtk->pModel = (int *)pMan2->pData, pMan2->pData = NULL;
     Aig_ManStop( pMan2 );
 //    pNtk->pModel = Aig_ManReleaseData( pMan2 );
@@ -582,7 +582,7 @@ int Abc_NtkIvyProve( Abc_Ntk_t ** ppNtk, void * pPars )
             Ioa_WriteAiger( pMan2, pFileName, 0, 0 );
             printf( "Intermediate reduced miter is written into file \"%s\".\n", pFileName );
         }
-        RetValue = Fra_FraigSat( pMan2, pParams->nMiteringLimitLast, 0, 0, 0, pParams->fVerbose ); 
+        RetValue = Fra_FraigSat( pMan2, pParams->nMiteringLimitLast, 0, 0, 0, 0, pParams->fVerbose ); 
         pNtk->pModel = (int *)pMan2->pData, pMan2->pData = NULL;
         Aig_ManStop( pMan2 );
     }

src/base/abci/abcQbf.c

@@ -41,7 +41,7 @@ static void Abc_NtkVectorClearVars( Abc_Ntk_t * pNtk, Vec_Int_t * vPiValues, int
 static void Abc_NtkVectorPrintPars( Vec_Int_t * vPiValues, int nPars );
 static void Abc_NtkVectorPrintVars( Abc_Ntk_t * pNtk, Vec_Int_t * vPiValues, int nPars );
 
-extern int Abc_NtkDSat( Abc_Ntk_t * pNtk, ABC_INT64_T nConfLimit, ABC_INT64_T nInsLimit, int fAlignPol, int fAndOuts, int fVerbose );
+extern int Abc_NtkDSat( Abc_Ntk_t * pNtk, ABC_INT64_T nConfLimit, ABC_INT64_T nInsLimit, int fAlignPol, int fAndOuts, int fNewSolver, int fVerbose );
 
 ////////////////////////////////////////////////////////////////////////
 ///                     FUNCTION DEFINITIONS                         ///
@@ -101,7 +101,7 @@ void Abc_NtkQbf( Abc_Ntk_t * pNtk, int nPars, int nItersMax, int fVerbose )
         // solve the synthesis instance
 clkS = clock();
 //        RetValue = Abc_NtkMiterSat( pNtkSyn, 0, 0, 0, NULL, NULL );
-        RetValue = Abc_NtkDSat( pNtkSyn, (ABC_INT64_T)0, (ABC_INT64_T)0, 1, 0, 0 );
+        RetValue = Abc_NtkDSat( pNtkSyn, (ABC_INT64_T)0, (ABC_INT64_T)0, 1, 0, 0, 0 );
 clkS = clock() - clkS;
         if ( RetValue == 0 )
             Abc_NtkModelToVector( pNtkSyn, vPiValues );

src/sat/bsat/module.make

@@ -4,6 +4,7 @@ SRC +=  src/sat/bsat/satMem.c \
     src/sat/bsat/satInterB.c \
     src/sat/bsat/satInterP.c \
     src/sat/bsat/satSolver.c \
+    src/sat/bsat/satSolver2.c \
     src/sat/bsat/satStore.c \
     src/sat/bsat/satTrace.c \
     src/sat/bsat/satUtil.c

src/sat/bsat/satSolver2.h

+/**************************************************************************************************
+MiniSat -- Copyright (c) 2005, Niklas Sorensson
+http://www.cs.chalmers.se/Cs/Research/FormalMethods/MiniSat/
+
+Permission is hereby granted, free of charge, to any person obtaining a copy of this software and
+associated documentation files (the "Software"), to deal in the Software without restriction,
+including without limitation the rights to use, copy, modify, merge, publish, distribute,
+sublicense, and/or sell copies of the Software, and to permit persons to whom the Software is
+furnished to do so, subject to the following conditions:
+
+The above copyright notice and this permission notice shall be included in all copies or
+substantial portions of the Software.
+
+THE SOFTWARE IS PROVIDED "AS IS", WITHOUT WARRANTY OF ANY KIND, EXPRESS OR IMPLIED, INCLUDING BUT
+NOT LIMITED TO THE WARRANTIES OF MERCHANTABILITY, FITNESS FOR A PARTICULAR PURPOSE AND
+NONINFRINGEMENT. IN NO EVENT SHALL THE AUTHORS OR COPYRIGHT HOLDERS BE LIABLE FOR ANY CLAIM,
+DAMAGES OR OTHER LIABILITY, WHETHER IN AN ACTION OF CONTRACT, TORT OR OTHERWISE, ARISING FROM, OUT
+OF OR IN CONNECTION WITH THE SOFTWARE OR THE USE OR OTHER DEALINGS IN THE SOFTWARE.
+**************************************************************************************************/
+// Modified to compile with MS Visual Studio 6.0 by Alan Mishchenko
+
+#ifndef satSolver2_h
+#define satSolver2_h
+
+
+#include <stdio.h>
+#include <stdlib.h>
+#include <string.h>
+#include <assert.h>
+
+#include "satVec.h"
+
+ABC_NAMESPACE_HEADER_START
+
+
+
+//=================================================================================================
+// Public interface:
+
+struct sat_solver2_t;
+typedef struct sat_solver2_t sat_solver2;
+
+extern sat_solver2* sat_solver2_new(void);
+extern void        sat_solver2_delete(sat_solver2* s);
+
+extern int         sat_solver2_addclause(sat_solver2* s, lit* begin, lit* end);
+extern int         sat_solver2_simplify(sat_solver2* s);
+extern int         sat_solver2_solve(sat_solver2* s, lit* begin, lit* end, ABC_INT64_T nConfLimit, ABC_INT64_T nInsLimit, ABC_INT64_T nConfLimitGlobal, ABC_INT64_T nInsLimitGlobal);
+
+extern int         sat_solver2_nvars(sat_solver2* s);
+extern int         sat_solver2_nclauses(sat_solver2* s);
+extern int         sat_solver2_nconflicts(sat_solver2* s);
+
+extern void        sat_solver2_setnvars(sat_solver2* s,int n);
+
+extern void        Sat_Solver2WriteDimacs( sat_solver2 * p, char * pFileName, lit* assumptionsBegin, lit* assumptionsEnd, int incrementVars );
+extern void        Sat_Solver2PrintStats( FILE * pFile, sat_solver2 * p );
+extern int *       Sat_Solver2GetModel( sat_solver2 * p, int * pVars, int nVars );
+extern void        Sat_Solver2DoubleClauses( sat_solver2 * p, int iVar );
+
+// trace recording
+extern void        sat_solver2TraceStart( sat_solver2 * pSat, char * pName );
+extern void        sat_solver2TraceStop( sat_solver2 * pSat );
+extern void        sat_solver2TraceWrite( sat_solver2 * pSat, int * pBeg, int * pEnd, int fRoot );
+
+// clause storage
+extern void        sat_solver2_store_alloc( sat_solver2 * s );
+extern void        sat_solver2_store_write( sat_solver2 * s, char * pFileName );
+extern void        sat_solver2_store_free( sat_solver2 * s );
+extern void        sat_solver2_store_mark_roots( sat_solver2 * s );
+extern void        sat_solver2_store_mark_clauses_a( sat_solver2 * s );
+extern void *      sat_solver2_store_release( sat_solver2 * s ); 
+
+//=================================================================================================
+// Solver representation:
+
+struct clause_t;
+typedef struct clause_t clause;
+
+struct sat_solver2_t
+{
+    int      size;          // nof variables
+    int      cap;           // size of varmaps
+    int      qhead;         // Head index of queue.
+    int      qtail;         // Tail index of queue.
+
+    // clauses
+    vecp     clauses;       // List of problem constraints. (contains: clause*)
+    vecp     learnts;       // List of learnt clauses. (contains: clause*)
+
+    // activities
+//    double   var_inc;       // Amount to bump next variable with.
+//    double   var_decay;     // INVERSE decay factor for variable activity: stores 1/decay. 
+    int      var_inc;
+//    int      var_decay;
+
+//    float    cla_inc;       // Amount to bump next clause with.
+    int      cla_inc;       // Amount to bump next clause with.
+//    float    cla_decay;     // INVERSE decay factor for clause activity: stores 1/decay.
+
+    vecp*    wlists;        // 
+//    double*  activity;      // A heuristic measurement of the activity of a variable.
+    unsigned*activity;      // A heuristic measurement of the activity of a variable.
+    lbool*   assigns;       // Current values of variables.
+    int*     orderpos;      // Index in variable order.
+    clause** reasons;       //
+    int*     levels;        //
+    lit*     trail;
+    char*    polarity;
+
+    clause*  binary;        // A temporary binary clause
+    lbool*   tags;          //
+    veci     tagged;        // (contains: var)
+    veci     stack;         // (contains: var)
+
+    veci     order;         // Variable order. (heap) (contains: var)
+    veci     trail_lim;     // Separator indices for different decision levels in 'trail'. (contains: int)
+    veci     model;         // If problem is solved, this vector contains the model (contains: lbool).
+    veci     conf_final;    // If problem is unsatisfiable (possibly under assumptions),
+                            // this vector represent the final conflict clause expressed in the assumptions.
+
+    int      root_level;    // Level of first proper decision.
+    int      simpdb_assigns;// Number of top-level assignments at last 'simplifyDB()'.
+    int      simpdb_props;  // Number of propagations before next 'simplifyDB()'.
+    double   random_seed;
+    double   progress_estimate;
+    int      verbosity;     // Verbosity level. 0=silent, 1=some progress report, 2=everything
+
+    stats_t    stats;
+
+    ABC_INT64_T   nConfLimit;    // external limit on the number of conflicts
+    ABC_INT64_T   nInsLimit;     // external limit on the number of implications
+    int           nRuntimeLimit; // external limit on runtime
+
+    // clause memory
+    int *    pMemArray;
+    int      nMemAlloc;
+    int      nMemSize;
+
+//    int      fSkipSimplify; // set to one to skip simplification of the clause database
+    int      fNotUseRandom; // do not allow random decisions with a fixed probability
+
+    veci     temp_clause;    // temporary storage for a CNF clause
+};
+
+static int sat_solver2_var_value( sat_solver2* s, int v ) 
+{
+    assert( s->model.ptr != NULL && v < s->size );
+    return (int)(s->model.ptr[v] == l_True);
+}
+static int sat_solver2_var_literal( sat_solver2* s, int v ) 
+{
+    assert( s->model.ptr != NULL && v < s->size );
+    return toLitCond( v, s->model.ptr[v] != l_True );
+}
+static void sat_solver2_act_var_clear(sat_solver2* s) 
+{
+    int i;
+    for (i = 0; i < s->size; i++)
+        s->activity[i] = 0;//.0;
+    s->var_inc = 1.0;
+}
+static void sat_solver2_compress(sat_solver2* s) 
+{
+    if ( s->qtail != s->qhead )
+    {
+        int RetValue = sat_solver2_simplify(s);
+        assert( RetValue != 0 );
+    }
+}
+
+static int sat_solver2_final(sat_solver2* s, int ** ppArray)
+{
+    *ppArray = s->conf_final.ptr;
+    return s->conf_final.size;
+}
+
+static int sat_solver2_set_runtime_limit(sat_solver2* s, int Limit)
+{
+    int nRuntimeLimit = s->nRuntimeLimit;
+    s->nRuntimeLimit = Limit;
+    return nRuntimeLimit;
+}
+
+static int sat_solver2_set_random(sat_solver2* s, int fNotUseRandom)
+{
+    int fNotUseRandomOld = s->fNotUseRandom;
+    s->fNotUseRandom = fNotUseRandom;
+    return fNotUseRandomOld;
+}
+
+ABC_NAMESPACE_HEADER_END
+
+#endif

src/sat/bsat/satUtil.c

@@ -21,6 +21,7 @@
 #include <stdio.h>
 #include <assert.h>
 #include "satSolver.h"
+#include "satSolver2.h"
 
 ABC_NAMESPACE_IMPL_START
 
@@ -148,13 +149,36 @@ void Sat_SolverClauseWriteDimacs( FILE * pFile, clause * pC, int fIncrement )
 ***********************************************************************/
 void Sat_SolverPrintStats( FILE * pFile, sat_solver * p )
 {
-//    printf( "calls         : %8d (%d)\n", (int)p->nCalls, (int)p->nCalls2 );
-    printf( "starts        : %8d\n", (int)p->stats.starts );
-    printf( "conflicts     : %8d\n", (int)p->stats.conflicts );
-    printf( "decisions     : %8d\n", (int)p->stats.decisions );
-    printf( "propagations  : %8d\n", (int)p->stats.propagations );
-    printf( "inspects      : %8d\n", (int)p->stats.inspects );
-//    printf( "inspects2     : %8d\n", (int)p->stats.inspects2 );
+//    printf( "calls         : %10d (%d)\n", (int)p->nCalls, (int)p->nCalls2 );
+    printf( "starts        : %10d\n", (int)p->stats.starts );
+    printf( "conflicts     : %10d\n", (int)p->stats.conflicts );
+    printf( "decisions     : %10d\n", (int)p->stats.decisions );
+    printf( "propagations  : %10d\n", (int)p->stats.propagations );
+    printf( "inspects      : %10d\n", (int)p->stats.inspects );
+//    printf( "inspects2     : %10d\n", (int)p->stats.inspects2 );
+}
+
+/**Function*************************************************************
+
+  Synopsis    [Writes the given clause in a file in DIMACS format.]
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+void Sat_Solver2PrintStats( FILE * pFile, sat_solver2 * p )
+{
+//    printf( "calls         : %10d (%d)\n", (int)p->nCalls, (int)p->nCalls2 );
+    printf( "starts        : %10d\n", (int)p->stats.starts );
+    printf( "conflicts     : %10d\n", (int)p->stats.conflicts );
+    printf( "decisions     : %10d\n", (int)p->stats.decisions );
+    printf( "propagations  : %10d\n", (int)p->stats.propagations );
+    printf( "inspects      : %10d\n", (int)p->stats.inspects );
+//    printf( "inspects2     : %10d\n", (int)p->stats.inspects2 );
+    printf( "memory        : %10d\n", p->nMemSize );
 }
 
 /**Function*************************************************************
@@ -183,6 +207,30 @@ int * Sat_SolverGetModel( sat_solver * p, int * pVars, int nVars )
 
 /**Function*************************************************************
 
+  Synopsis    [Returns a counter-example.]
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+int * Sat_Solver2GetModel( sat_solver2 * p, int * pVars, int nVars )
+{
+    int * pModel;
+    int i;
+    pModel = ABC_CALLOC( int, nVars+1 );
+    for ( i = 0; i < nVars; i++ )
+    {
+        assert( pVars[i] >= 0 && pVars[i] < p->size );
+        pModel[i] = (int)(p->model.ptr[pVars[i]] == l_True);
+    }
+    return pModel;    
+}
+
+/**Function*************************************************************
+
   Synopsis    [Duplicates all clauses, complements unit clause of the given var.]
 
   Description []