Upgrading the SAT solvers.

abcexe.dsp

@@ -88,6 +88,10 @@ LINK32=link.exe
 # PROP Default_Filter "cpp;c;cxx;rc;def;r;odl;idl;hpj;bat"
 # Begin Source File
 
+SOURCE=.\src\proof\cec\cecSatG2.c
+# End Source File
+# Begin Source File
+
 SOURCE=.\src\base\main\main.c
 # End Source File
 # End Group

abclib.dsp

@@ -2395,6 +2395,14 @@ SOURCE=.\src\sat\glucose2\BoundedQueue.h
 # End Source File
 # Begin Source File
 
+SOURCE=.\src\sat\glucose2\CGlucose.h
+# End Source File
+# Begin Source File
+
+SOURCE=.\src\sat\glucose2\CGlucoseCore.h
+# End Source File
+# Begin Source File
+
 SOURCE=.\src\sat\glucose2\Constants.h
 # End Source File
 # Begin Source File

src/base/abci/abc.c

@@ -36290,7 +36290,7 @@ int Abc_CommandAbc9Fraig( Abc_Frame_t * pAbc, int argc, char ** argv )
     Cec_ParFra_t ParsFra, * pPars = &ParsFra; Gia_Man_t * pTemp;
     int c, fUseAlgo = 0, fUseAlgoG = 0, fUseAlgoG2 = 0;
     Cec_ManFraSetDefaultParams( pPars );
-    pPars->jType          =       0;    // solver type
+    pPars->jType          =       2;    // solver type
     pPars->fSatSweeping   =       1;    // conflict limit at a node
     pPars->nWords         =       8;    // simulation words
     pPars->nRounds        =      10;    // simulation rounds
@@ -36300,7 +36300,7 @@ int Abc_CommandAbc9Fraig( Abc_Frame_t * pAbc, int argc, char ** argv )
     pPars->nCallsRecycle  =     500;    // calls to perform before recycling SAT solver
     pPars->nGenIters      =     100;    // pattern generation iterations
     Extra_UtilGetoptReset();
-    while ( ( c = Extra_UtilGetopt( argc, argv, "JWRILDCPrmdckngxwvh" ) ) != EOF )
+    while ( ( c = Extra_UtilGetopt( argc, argv, "JWRILDCNPrmdckngxwvh" ) ) != EOF )
     {
         switch ( c )
         {
@@ -36381,6 +36381,17 @@ int Abc_CommandAbc9Fraig( Abc_Frame_t * pAbc, int argc, char ** argv )
             if ( pPars->nBTLimit < 0 )
                 goto usage;
             break;
+        case 'N':
+            if ( globalUtilOptind >= argc )
+            {
+                Abc_Print( -1, "Command line switch \"-N\" should be followed by an integer.\n" );
+                goto usage;
+            }
+            pPars->nCallsRecycle = atoi(argv[globalUtilOptind]);
+            globalUtilOptind++;
+            if ( pPars->nCallsRecycle < 0 )
+                goto usage;
+            break;
         case 'P':
             if ( globalUtilOptind >= argc )
             {
@@ -36443,7 +36454,7 @@ int Abc_CommandAbc9Fraig( Abc_Frame_t * pAbc, int argc, char ** argv )
     return 0;
 
 usage:
-    Abc_Print( -2, "usage: &fraig [-JWRILDCP <num>] [-rmdckngwvh]\n" );
+    Abc_Print( -2, "usage: &fraig [-JWRILDCNP <num>] [-rmdckngwvh]\n" );
     Abc_Print( -2, "\t         performs combinational SAT sweeping\n" );
     Abc_Print( -2, "\t-J num : the solver type [default = %d]\n", pPars->jType );
     Abc_Print( -2, "\t-W num : the number of simulation words [default = %d]\n", pPars->nWords );
@@ -36452,6 +36463,7 @@ usage:
     Abc_Print( -2, "\t-L num : the max number of levels of nodes to consider [default = %d]\n", pPars->nLevelMax );
     Abc_Print( -2, "\t-D num : the max number of steps of speculative reduction [default = %d]\n", pPars->nDepthMax );
     Abc_Print( -2, "\t-C num : the max number of conflicts at a node [default = %d]\n", pPars->nBTLimit );
+    Abc_Print( -2, "\t-N num : the min number of calls to recycle the solver [default = %d]\n", pPars->nCallsRecycle );
     Abc_Print( -2, "\t-P num : the number of pattern generation iterations [default = %d]\n", pPars->nGenIters );
     Abc_Print( -2, "\t-r     : toggle the use of AIG rewriting [default = %s]\n", pPars->fRewriting? "yes": "no" );
     Abc_Print( -2, "\t-m     : toggle miter vs. any circuit [default = %s]\n", pPars->fCheckMiter? "miter": "circuit" );

src/proof/cec/cecSatG2.c

@@ -1366,7 +1366,7 @@ int Cec4_ManSweepNode( Cec4_Man_t * p, int iObj, int iRepr )
         assert( p->pAig->iPatsPi > 0 && p->pAig->iPatsPi < 64 * p->pAig->nSimWords );
         //Vec_IntForEachEntryDouble( &p->pNew->vCopiesTwo, IdAig, IdSat, i )
         //    Cec4_ObjSimSetInputBit( p->pAig, IdAig, sat_solver_read_cex_varvalue(p->pSat, IdSat) );
-        pCex = sat_solver_read_cex( p->pSat );
+        pCex = NULL;//sat_solver_read_cex( p->pSat );
         Vec_IntClear( p->vPat );
         if ( pCex == NULL )
         {
@@ -1461,8 +1461,8 @@ int Cec4_ManPerformSweeping( Gia_Man_t * p, Cec_ParFra_t * pPars, Gia_Man_t ** p
     Gia_Obj_t * pObj, * pRepr; 
     int i, fSimulate = 1;
     if ( pPars->fVerbose )
-        printf( "Simulate %d words in %d rounds. Easy SAT with %d tries. SAT with %d confs. Recycle after %d SAT calls.\n", 
-            pPars->nWords, pPars->nRounds, pPars->nGenIters, pPars->nBTLimit, pPars->nCallsRecycle );
+        printf( "Solver type = %d. Simulate %d words in %d rounds. SAT with %d confs. Recycle after %d SAT calls.\n", 
+            pPars->jType, pPars->nWords, pPars->nRounds, pPars->nBTLimit, pPars->nCallsRecycle );
 
     // this is currently needed to have a correct mapping
     Gia_ManForEachCi( p, pObj, i )
@@ -1498,7 +1498,7 @@ int Cec4_ManPerformSweeping( Gia_Man_t * p, Cec_ParFra_t * pPars, Gia_Man_t ** p
         Cec4_ManSimulate( p, pMan );
         if ( pPars->fCheckMiter && !Cec4_ManSimulateCos(p) ) // cex detected
             goto finalize;
-        if ( i % (pPars->nRounds / 5) == 0 && pPars->fVerbose )
+        if ( i && i % (pPars->nRounds / 5) == 0 && pPars->fVerbose )
             Cec4_ManPrintStats( p, pPars, pMan, 1 );
     }
 
@@ -1510,9 +1510,11 @@ int Cec4_ManPerformSweeping( Gia_Man_t * p, Cec_ParFra_t * pPars, Gia_Man_t ** p
         Cec4_ManSimulate( p, pMan );
         if ( pPars->fCheckMiter && !Cec4_ManSimulateCos(p) ) // cex detected
             goto finalize;
-        if ( pPars->fVerbose )
+        if ( i && i % 5 == 0 && pPars->fVerbose )
             Cec4_ManPrintStats( p, pPars, pMan, 1 );
     }
+    if ( i && i % 5 && pPars->fVerbose )
+        Cec4_ManPrintStats( p, pPars, pMan, 1 );
 
     p->iPatsPi = 0;
     pMan->nSatSat = 0;

src/sat/glucose/Glucose.cpp

@@ -609,7 +609,7 @@ void Solver::analyze(CRef confl, vec<Lit>& out_learnt,vec<Lit>&selectors, int& o
     for(i = 0;i<selectors.size();i++)  
       out_learnt.push(selectors[i]);       
 
-    out_learnt.copyTo(analyze_toclear);
+    out_learnt.copyTo_(analyze_toclear);
     if (ccmin_mode == 2){
         uint32_t abstract_level = 0;
         for (i = 1; i < out_learnt.size(); i++)

src/sat/glucose/SolverTypes.h

@@ -306,9 +306,15 @@ class OccLists
     }
 
     void  clear(bool free = true){
-        occs   .clear(free);
-        dirty  .clear(free);
-        dirties.clear(free);
+        if(free){
+            occs   .clear(free);
+            dirty  .clear(free);
+            dirties.clear(free);
+        } else {
+            occs   .shrink_(occs   .size());
+            dirty  .shrink_(dirty  .size());
+            dirties.shrink_(dirties.size());
+        }
     }
 };
 

src/sat/glucose/Vec.h

@@ -89,7 +89,8 @@ public:
     T&       operator [] (int index)       { return data[index]; }
 
     // Duplicatation (preferred instead):
-    void copyTo(vec<T>& copy) const { copy.clear(); copy.growTo(sz); for (int i = 0; i < sz; i++) copy[i] = data[i]; }
+    void copyTo (vec<T>& copy) const { copy.clear(); copy.growTo(sz); for (int i = 0; i < sz; i++) copy[i] = data[i]; }
+    void copyTo_(vec<T>& copy) const { copy.shrink_(copy.size()); copy.growTo(sz); for (int i = 0; i < sz; i++) copy[i] = data[i]; }
     void moveTo(vec<T>& dest) { dest.clear(true); dest.data = data; dest.sz = sz; dest.cap = cap; data = NULL; sz = 0; cap = 0; }
 };
 

src/sat/glucose2/CGlucose.h

+#ifndef Glucose_CGlucose_h
+#define Glucose_CGlucose_h
+
+#define CGLUCOSE_EXP 1
+
+#endif
\ No newline at end of file

src/sat/glucose2/SimpSolver.h

@@ -24,6 +24,8 @@ OF OR IN CONNECTION WITH THE SOFTWARE OR THE USE OR OTHER DEALINGS IN THE SOFTWA
 #include "sat/glucose2/Queue.h"
 #include "sat/glucose2/Solver.h"
 
+#include "sat/glucose2/CGlucose.h"
+
 ABC_NAMESPACE_CXX_HEADER_START
 
 namespace Gluco2 {

src/sat/glucose2/SimpSolver2.cpp

@@ -68,6 +68,7 @@ SimpSolver::SimpSolver() :
     ca.extra_clause_field = true; // NOTE: must happen before allocating the dummy clause below.
     bwdsub_tmpunit        = ca.alloc(dummy);
     remove_satisfied      = false;
+    parsing               = 0;
 }
 
 

src/sat/glucose2/Solver.h

@@ -37,6 +37,8 @@ OF OR IN CONNECTION WITH THE SOFTWARE OR THE USE OR OTHER DEALINGS IN THE SOFTWA
 #include "sat/glucose2/BoundedQueue.h"
 #include "sat/glucose2/Constants.h"
 
+#include "sat/glucose2/CGlucose.h"
+
 ABC_NAMESPACE_CXX_HEADER_START
 
 namespace Gluco2 {
@@ -123,6 +125,7 @@ public:
     int     nVars      ()      const;       // The current number of variables.
     int     nFreeVars  ()      const;
     int *   getCex     ()      const;
+    int     level      (Var x) const;       // moved level() to public to compile "struct JustOrderLt" -- alanmi
 
     // Incremental mode
     void setIncrementalMode();
@@ -341,7 +344,6 @@ protected:
     int      decisionLevel    ()      const; // Gives the current decisionlevel.
     uint32_t abstractLevel    (Var x) const; // Used to represent an abstraction of sets of decision levels.
     CRef     reason           (Var x) const;
-    int      level            (Var x) const;
     double   progressEstimate ()      const; // DELETE THIS ?? IT'S NOT VERY USEFUL ...
     bool     withinBudget     ()      const;
     inline bool isSelector(Var v) {return (incremental && v>nbVarsInitialFormula);}
@@ -359,6 +361,99 @@ protected:
     // Returns a random integer 0 <= x < size. Seed must never be 0.
     static inline int irand(double& seed, int size) {
         return (int)(drand(seed) * size); }
+
+
+    // circuit-based solver
+protected:
+    struct JustData { unsigned now: 1; double act_fanin; };
+    vec<JustData> jdata;
+    static inline JustData mkJustData(bool n){ JustData d = {n,0}; return d; }
+
+    struct JustOrderLt {
+        const Solver * pS;
+        bool operator () (Var x, Var y) const {
+            if( pS->justActivity(x) != pS->justActivity(y) )
+                return pS->justActivity(x) > pS->justActivity(y);
+            if( pS->level(x) != pS->level(y) )
+                return pS->level(x) < pS->level(y);
+            return x > y;
+        }
+        JustOrderLt(const Solver * _pS) : pS(_pS) { }
+    };
+
+    struct JustWatch { struct { unsigned dir:1; } header; Var head; Var next; Var prev; };
+    vec<JustWatch> jwatch;
+    static inline JustWatch mkJustWatch(){ JustWatch w = {0, var_Undef, var_Undef, var_Undef}; return w; }
+    void addJwatch( Var host, Var member );
+    void delJwatch( Var member );
+
+    vec<Lit> var2FaninLits; // (~0): undefine
+    vec<unsigned> var2TravId;
+    vec<Lit> var2Fanout0, var2FanoutN, var2FanoutP;
+    CRef itpc; // the interpreted clause of a gate 
+
+    bool isTwoFanin( Var v ) const ; // this var has two fanins 
+    Lit  getFaninLit0( Var v ) const { return var2FaninLits[ (v<<1) + 0 ]; }
+    Lit  getFaninLit1( Var v ) const { return var2FaninLits[ (v<<1) + 1 ]; }
+    bool getFaninC0( Var v )   const { return sign(getFaninLit0(v)); }
+    bool getFaninC1( Var v )   const { return sign(getFaninLit1(v)); }
+    Var  getFaninVar0( Var v ) const { return  var(getFaninLit0(v)); }
+    Var  getFaninVar1( Var v ) const { return  var(getFaninLit1(v)); }
+
+    Lit  maxActiveLit(Lit lit0, Lit lit1) const ;
+
+    Lit  fanin2JustLit(Var v) const ;
+    Lit  gateJustFanin(Var v) const ; // l_Undef=satisfied, 0/1 = fanin0/fanin1 requires justify
+    void gateAddJwatch(Var v);
+    CRef gatePropagateCheck( Var v, Var t );
+    CRef gatePropagateCheckThis( Var v );
+    CRef gatePropagateCheckFanout( Var v, Lit lfo );
+    void setItpcSize( int sz ); // sz <= 3
+
+    // directly call by original glucose functions 
+    void updateJustActivity( Var v );
+    void ResetJustData(bool fCleanMemory);
+    Lit  pickJustLit( Var& j_reason );
+    void justCheck();
+    void pushJustQueue(Var v);
+    void restoreJustQueue(int level); // call with cancelUntil
+    void gateClearJwatch( Var v, int backtrack_level );
+
+    CRef gatePropagate( Lit p );
+
+    CRef interpret( Var v, Var t );
+    CRef castCRef( Lit p );  // interpret a gate into a clause 
+    CRef getConfClause( CRef r );
+
+    CRef Var2CRef( Var  v  ) const { return v  |  (1<<(sizeof(CRef)*8-1)); }
+    Var  CRef2Var( CRef cr ) const { return cr & ~(1<<(sizeof(CRef)*8-1)); }
+    bool isGateCRef( CRef cr ) const { return CRef_Undef != cr && 0 != (cr & (1<<(sizeof(CRef)*8-1))); }
+
+    int64_t travId_prev, travId;
+
+    Heap<JustOrderLt> jheap;
+    /* jstack
+    call by unchecked_enqueue
+    consumed by pickJustLit
+    cleaned by cancelUntil
+    */
+    vec<Var> jstack;
+public:
+    void setVarFaninLits( Var v, Lit lit1, Lit lit2 );
+    //void delVarFaninLits( Var v);
+
+    int setNewRound(){ return travId ++ ; }
+    void markCone( Var v );
+    bool isRoundWatch( Var v ) const { return travId==var2TravId[v]; }
+
+
+    const JustData& getJustData(int v) const { return jdata[v]; }
+    double varActivity(int v) const { return activity[v];}
+    double justActivity(int v) const { return jdata[v].act_fanin;}
+    int varPolarity(int v){ return polarity[v]? 1: 0;}
+    vec<Lit> JustModel; // model obtained by justification enabled
+
+    int justUsage() const ;
 };
 
 
@@ -378,11 +473,24 @@ inline void Solver::varBumpActivity(Var v, double inc) {
         // Rescale:
         for (int i = 0; i < nVars(); i++)
             activity[i] *= 1e-100;
+        
+        if( justUsage() )
+            for (int i = 0; i < jheap.size(); i++){
+                Var j = jheap[i];
+                jdata[j].act_fanin = activity[getFaninVar0(j)] > activity[getFaninVar1(j)]? activity[getFaninVar0(j)]: activity[getFaninVar1(j)];
+            }
         var_inc *= 1e-100; }
 
     // Update order_heap with respect to new activity:
     if (order_heap.inHeap(v))
-        order_heap.decrease(v); }
+        order_heap.decrease(v); 
+
+    #ifdef CGLUCOSE_EXP
+    if( justUsage() )
+        updateJustActivity(v);
+
+    #endif
+}
 
 inline void Solver::claDecayActivity() { cla_inc *= (1 / clause_decay); }
 inline void Solver::claBumpActivity (Clause& c) {
@@ -405,14 +513,27 @@ inline bool     Solver::addClause       (Lit p)                 { add_tmp.clear(
 inline bool     Solver::addClause       (Lit p, Lit q)          { add_tmp.clear(); add_tmp.push(p); add_tmp.push(q); return addClause_(add_tmp); }
 inline bool     Solver::addClause       (Lit p, Lit q, Lit r)   { add_tmp.clear(); add_tmp.push(p); add_tmp.push(q); add_tmp.push(r); return addClause_(add_tmp); }
 inline bool     Solver::locked          (const Clause& c) const { 
+   #ifdef CGLUCOSE_EXP
+
+    if(c.size()>2) 
+     return value(c[0]) == l_True && reason(var(c[0])) != CRef_Undef && !isGateCRef(reason(var(c[0]))) && ca.lea(reason(var(c[0]))) == &c; 
+   return 
+     (value(c[0]) == l_True && reason(var(c[0])) != CRef_Undef && !isGateCRef(reason(var(c[0]))) && ca.lea(reason(var(c[0]))) == &c)
+     || 
+     (value(c[1]) == l_True && reason(var(c[1])) != CRef_Undef && !isGateCRef(reason(var(c[1]))) && ca.lea(reason(var(c[1]))) == &c);
+
+   #else
+   
    if(c.size()>2) 
      return value(c[0]) == l_True && reason(var(c[0])) != CRef_Undef && ca.lea(reason(var(c[0]))) == &c; 
    return 
      (value(c[0]) == l_True && reason(var(c[0])) != CRef_Undef && ca.lea(reason(var(c[0]))) == &c)
      || 
      (value(c[1]) == l_True && reason(var(c[1])) != CRef_Undef && ca.lea(reason(var(c[1]))) == &c);
+
+   #endif
  }
-inline void     Solver::newDecisionLevel()                      { trail_lim.push(trail.size()); }
+inline void     Solver::newDecisionLevel()                      {trail_lim.push(trail.size());}
 
 inline int      Solver::decisionLevel ()      const   { return trail_lim.size(); }
 inline uint32_t Solver::abstractLevel (Var x) const   { return 1 << (level(x) & 31); }
@@ -463,9 +584,9 @@ inline void     Solver::toDimacs      (const char* file, Lit p, Lit q, Lit r){ v
 
 inline void     Solver::addVar(Var v) { while (v >= nVars()) newVar(); }
 
-inline void     Solver::sat_solver_set_var_fanin_lit(int var, int lit0, int lit1) {}  
-inline void     Solver::sat_solver_start_new_round()  {}  
-inline void     Solver::sat_solver_mark_cone(int var) {}  
+inline void     Solver::sat_solver_set_var_fanin_lit(int v, int lit0, int lit1) { setVarFaninLits( Var(v), toLit(lit0), toLit(lit1) ); }
+inline void     Solver::sat_solver_start_new_round()  { setNewRound(); }
+inline void     Solver::sat_solver_mark_cone(int v) { markCone(v); }
 
 //=================================================================================================
 // Debug etc:
@@ -501,6 +622,9 @@ inline void Solver::printInitialClause(CRef cr)
 //=================================================================================================
 }
 
+
 ABC_NAMESPACE_CXX_HEADER_END
 
+#include "sat/glucose2/CGlucoseCore.h"
+
 #endif

src/sat/glucose2/SolverTypes.h

@@ -38,6 +38,8 @@ OF OR IN CONNECTION WITH THE SOFTWARE OR THE USE OR OTHER DEALINGS IN THE SOFTWA
 #include "sat/glucose2/Map.h"
 #include "sat/glucose2/Alloc.h"
 
+#include "sat/glucose2/CGlucose.h"
+
 ABC_NAMESPACE_CXX_HEADER_START
 
 namespace Gluco2 {
@@ -145,6 +147,10 @@ class Clause {
 
     friend class ClauseAllocator;
 
+    #ifdef CGLUCOSE_EXP
+    friend class Solver;
+    #endif
+
     // NOTE: This constructor cannot be used directly (doesn't allocate enough memory).
     template<class V>
     Clause(const V& ps, bool use_extra, bool learnt) {
@@ -306,9 +312,15 @@ class OccLists
     }
 
     void  clear(bool free = true){
-        occs   .clear(free);
-        dirty  .clear(free);
-        dirties.clear(free);
+        if(free){
+            occs   .clear(free);
+            dirty  .clear(free);
+            dirties.clear(free);
+        } else {
+            occs   .shrink_(occs   .size());
+            dirty  .shrink_(dirty  .size());
+            dirties.shrink_(dirties.size());
+        }
     }
 };
 

src/sat/glucose2/Vec.h

@@ -89,7 +89,8 @@ public:
     T&       operator [] (int index)       { return data[index]; }
 
     // Duplicatation (preferred instead):
-    void copyTo(vec<T>& copy) const { copy.clear(); copy.growTo(sz); for (int i = 0; i < sz; i++) copy[i] = data[i]; }
+    void copyTo (vec<T>& copy) const { copy.clear(); copy.growTo(sz); for (int i = 0; i < sz; i++) copy[i] = data[i]; }
+    void copyTo_(vec<T>& copy) const { copy.shrink_(copy.size()); copy.growTo(sz); for (int i = 0; i < sz; i++) copy[i] = data[i]; }
     void moveTo(vec<T>& dest) { dest.clear(true); dest.data = data; dest.sz = sz; dest.cap = cap; data = NULL; sz = 0; cap = 0; }
 };