xSAT is an experimental SAT Solver based on Glucose v3(see Glucose copyrights below) and ABC C version of

MiniSat (bsat) developed by Niklas Sorensson and modified by Alan Mishchenko. It’s development has reached
sufficient maturity to be committed in ABC, but still in a beta state.

TODO:
* Read compressed CNF files.
* Study the use of floating point for variables and clauses activity.
* Better documentation.
* Improve verbose messages.
* Expose parameters for tuning.

1 files changed, 995 insertions, 0 deletions

diff --git a/src/sat/xsat/xsatSolver.c b/src/sat/xsat/xsatSolver.c
new file mode 100644
index 00000000..d6968a2d
--- /dev/null
+++ b/src/sat/xsat/xsatSolver.c
@@ -0,0 +1,995 @@
+/**CFile****************************************************************
+
+  FileName    [xsatSolver.c]
+
+  SystemName  [ABC: Logic synthesis and verification system.]
+
+  PackageName [xSAT - A SAT solver written in C.
+               Read the license file for more info.]
+
+  Synopsis    [Solver internal functions implementation.]
+
+  Author      [Bruno Schmitt <boschmitt@inf.ufrgs.br>]
+
+  Affiliation [UC Berkeley / UFRGS]
+
+  Date        [Ver. 1.0. Started - November 10, 2016.]
+
+  Revision    []
+
+***********************************************************************/
+////////////////////////////////////////////////////////////////////////
+///                          INCLUDES                                ///
+////////////////////////////////////////////////////////////////////////
+#include <stdio.h>
+#include <assert.h>
+#include <string.h>
+#include <math.h>
+
+#include "xsatHeap.h"
+#include "xsatSolver.h"
+#include "xsatUtils.h"
+
+ABC_NAMESPACE_IMPL_START
+
+////////////////////////////////////////////////////////////////////////
+///                     FUNCTION DECLARATIONS                        ///
+////////////////////////////////////////////////////////////////////////
+/**Function*************************************************************
+
+  Synopsis    []
+
+  Description []
+
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+static inline int xSAT_SolverDecide( xSAT_Solver_t* s )
+{
+    int NextVar = VarUndef;
+
+    while ( NextVar == VarUndef || Vec_StrEntry( s->vAssigns, NextVar ) != VarX )
+    {
+        if ( xSAT_HeapSize( s->hOrder ) == 0 )
+        {
+            NextVar = VarUndef;
+            break;
+        }
+        else
+            NextVar = xSAT_HeapRemoveMin( s->hOrder );
+    }
+    return NextVar;
+}
+
+/**Function*************************************************************
+
+  Synopsis    []
+
+  Description []
+
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+void xSAT_SolverRebuildOrderHeap( xSAT_Solver_t* s )
+{
+    Vec_Int_t * vTemp = Vec_IntAlloc( Vec_StrSize( s->vAssigns ) );
+    int Var;
+
+    for ( Var = 0; Var < Vec_StrSize( s->vAssigns ); Var++ )
+        if ( Vec_StrEntry( s->vAssigns, Var ) == VarX )
+            Vec_IntPush( vTemp, Var );
+
+    xSAT_HeapBuild( s->hOrder, vTemp );
+    Vec_IntFree( vTemp );
+}
+
+/**Function*************************************************************
+
+  Synopsis    []
+
+  Description []
+
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+static inline void xSAT_SolverVarActRescale( xSAT_Solver_t * s )
+{
+    unsigned * pActivity = (unsigned *) Vec_IntArray( s->vActivity );
+
+    for ( int i = 0; i < Vec_IntSize( s->vActivity ); i++ )
+        pActivity[i] >>= 19;
+
+    s->nVarActInc >>= 19;
+    s->nVarActInc = Abc_MaxInt( s->nVarActInc, (1 << 5) );
+}
+
+/**Function*************************************************************
+
+  Synopsis    []
+
+  Description []
+
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+static inline void xSAT_SolverVarActBump( xSAT_Solver_t* s, int Var )
+{
+    unsigned * pActivity = (unsigned *) Vec_IntArray( s->vActivity );
+
+    pActivity[Var] += s->nVarActInc;
+    if ( pActivity[Var] & 0x80000000 )
+        xSAT_SolverVarActRescale( s );
+
+    if ( xSAT_HeapInHeap( s->hOrder, Var ) )
+        xSAT_HeapDecrease( s->hOrder, Var );
+}
+
+/**Function*************************************************************
+
+  Synopsis    []
+
+  Description []
+
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+static inline void xSAT_SolverVarActDecay( xSAT_Solver_t * s )
+{
+    s->nVarActInc += ( s->nVarActInc >> 4 );
+}
+
+/**Function*************************************************************
+
+  Synopsis    []
+
+  Description []
+
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+static inline void xSAT_SolverClaActRescale( xSAT_Solver_t * s )
+{
+    xSAT_Clause_t * pC;
+    int i, CRef;
+
+    Vec_IntForEachEntry( s->vLearnts, CRef, i )
+    {
+        pC = xSAT_SolverReadClause( s, (uint32_t) CRef );
+        pC->pData[pC->nSize].Act >>= 14;
+    }
+    s->nClaActInc >>= 14;
+    s->nClaActInc = Abc_MaxInt( s->nClaActInc, ( 1 << 10 ) );
+}
+
+/**Function*************************************************************
+
+  Synopsis    []
+
+  Description []
+
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+static inline void xSAT_SolverClaActBump( xSAT_Solver_t* s, xSAT_Clause_t * pCla )
+{
+    pCla->pData[pCla->nSize].Act += s->nClaActInc;
+    if ( pCla->pData[pCla->nSize].Act & 0x80000000 )
+        xSAT_SolverClaActRescale( s );
+}
+
+/**Function*************************************************************
+
+  Synopsis    []
+
+  Description []
+
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+static inline void xSAT_SolverClaActDecay( xSAT_Solver_t * s )
+{
+    s->nClaActInc += ( s->nClaActInc >> 10 );
+}
+
+/**Function*************************************************************
+
+  Synopsis    []
+
+  Description []
+
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+static inline int xSAT_SolverClaCalcLBD( xSAT_Solver_t * s, xSAT_Clause_t * pCla )
+{
+    int nLBD = 0;
+
+    s->nStamp++;
+    for ( int i = 0; i < pCla->nSize; i++ )
+    {
+        int Level = Vec_IntEntry( s->vLevels, xSAT_Lit2Var( pCla->pData[i].Lit ) );
+        if ( (unsigned) Vec_IntEntry( s->vStamp, Level ) != s->nStamp )
+        {
+            Vec_IntWriteEntry( s->vStamp, Level, (int) s->nStamp );
+            nLBD++;
+        }
+    }
+    return nLBD;
+}
+
+static inline int xSAT_SolverClaCalcLBD2( xSAT_Solver_t * s, Vec_Int_t * vLits )
+{
+    int nLBD = 0;
+
+    s->nStamp++;
+    for ( int i = 0; i < Vec_IntSize( vLits ); i++ )
+    {
+        int Level = Vec_IntEntry( s->vLevels, xSAT_Lit2Var( Vec_IntEntry( vLits, i ) ) );
+        if ( (unsigned) Vec_IntEntry( s->vStamp, Level ) != s->nStamp )
+        {
+            Vec_IntWriteEntry( s->vStamp, Level, (int) s->nStamp );
+            nLBD++;
+        }
+    }
+    return nLBD;
+}
+
+/**Function*************************************************************
+
+  Synopsis    []
+
+  Description []
+
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+uint32_t xSAT_SolverClaNew( xSAT_Solver_t * s, Vec_Int_t * vLits , int fLearnt )
+{
+    assert( Vec_IntSize( vLits ) > 1);
+    assert( fLearnt == 0 || fLearnt == 1 );
+
+    uint32_t CRef;
+    xSAT_Clause_t * pCla;
+    xSAT_Watcher_t w1;
+    xSAT_Watcher_t w2;
+
+    uint32_t nWords = 3 + fLearnt + Vec_IntSize( vLits );
+    CRef = xSAT_MemAppend( s->pMemory, nWords );
+    pCla = xSAT_SolverReadClause( s, CRef );
+    pCla->fLearnt = fLearnt;
+    pCla->fMark = 0;
+    pCla->fReallocd = 0;
+    pCla->fCanBeDel = fLearnt;
+    pCla->nSize = Vec_IntSize( vLits );
+    memcpy( &( pCla->pData[0].Lit ), Vec_IntArray( vLits ), sizeof( int ) * Vec_IntSize( vLits ) );
+
+    if ( fLearnt )
+    {
+        Vec_IntPush( s->vLearnts, CRef );
+        pCla->nLBD = xSAT_SolverClaCalcLBD2( s, vLits );
+        pCla->pData[pCla->nSize].Act = 0;
+        s->Stats.nLearntLits += Vec_IntSize( vLits );
+        xSAT_SolverClaActBump(s, pCla);
+    }
+    else
+    {
+        Vec_IntPush( s->vClauses, CRef );
+        s->Stats.nClauseLits += Vec_IntSize( vLits );
+    }
+
+    w1.CRef = CRef;
+    w2.CRef = CRef;
+    w1.Blocker = pCla->pData[1].Lit;
+    w2.Blocker = pCla->pData[0].Lit;
+
+    if ( Vec_IntSize( vLits ) == 2 )
+    {
+        xSAT_WatchListPush( xSAT_VecWatchListEntry( s->vBinWatches, xSAT_NegLit( pCla->pData[0].Lit ) ), w1 );
+        xSAT_WatchListPush( xSAT_VecWatchListEntry( s->vBinWatches, xSAT_NegLit( pCla->pData[1].Lit ) ), w2 );
+    }
+    else
+    {
+        xSAT_WatchListPush( xSAT_VecWatchListEntry( s->vWatches, xSAT_NegLit( pCla->pData[0].Lit ) ), w1 );
+        xSAT_WatchListPush( xSAT_VecWatchListEntry( s->vWatches, xSAT_NegLit( pCla->pData[1].Lit ) ), w2 );
+    }
+    return CRef;
+}
+
+/**Function*************************************************************
+
+  Synopsis    []
+
+  Description []
+
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+int xSAT_SolverEnqueue( xSAT_Solver_t* s, int Lit, uint32_t Reason )
+{
+    int Var = xSAT_Lit2Var( Lit );
+
+    Vec_StrWriteEntry( s->vAssigns, Var, xSAT_LitSign( Lit ) );
+    Vec_IntWriteEntry( s->vLevels, Var, xSAT_SolverDecisionLevel( s ) );
+    Vec_IntWriteEntry( s->vReasons, Var, (int) Reason );
+    Vec_IntPush( s->vTrail, Lit );
+
+    return true;
+}
+
+/**Function*************************************************************
+
+  Synopsis    []
+
+  Description []
+
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+static inline void xSAT_SolverNewDecision( xSAT_Solver_t* s, int Lit )
+{
+    assert( Vec_StrEntry( s->vAssigns, xSAT_Lit2Var( Lit ) ) == VarX );
+    s->Stats.nDecisions++;
+    Vec_IntPush( s->vTrailLim, Vec_IntSize( s->vTrail ) );
+    xSAT_SolverEnqueue( s, Lit, CRefUndef );
+}
+
+/**Function*************************************************************
+
+  Synopsis    []
+
+  Description []
+
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+void xSAT_SolverCancelUntil( xSAT_Solver_t * s, int Level )
+{
+    if ( xSAT_SolverDecisionLevel( s ) <= Level )
+        return;
+
+    for ( int c = Vec_IntSize( s->vTrail ) - 1; c >= Vec_IntEntry( s->vTrailLim, Level ); c-- )
+    {
+        int Var = xSAT_Lit2Var( Vec_IntEntry( s->vTrail, c ) );
+
+        Vec_StrWriteEntry( s->vAssigns, Var, VarX );
+        Vec_IntWriteEntry( s->vReasons, Var, ( int ) CRefUndef );
+        Vec_StrWriteEntry( s->vPolarity, Var, xSAT_LitSign( Vec_IntEntry( s->vTrail, c ) ) );
+
+        if ( !xSAT_HeapInHeap( s->hOrder, Var ) )
+            xSAT_HeapInsert( s->hOrder, Var );
+    }
+
+    s->iQhead = Vec_IntEntry( s->vTrailLim, Level );
+    Vec_IntShrink( s->vTrail, Vec_IntEntry( s->vTrailLim, Level ) );
+    Vec_IntShrink( s->vTrailLim, Level );
+}
+
+/**Function*************************************************************
+
+  Synopsis    []
+
+  Description []
+
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+static int xSAT_SolverIsLitRemovable( xSAT_Solver_t* s, int Lit, int MinLevel )
+{
+    int top = Vec_IntSize( s->vTagged );
+
+    assert( (uint32_t) Vec_IntEntry( s->vReasons, xSAT_Lit2Var( Lit ) ) != CRefUndef );
+    Vec_IntClear( s->vStack );
+    Vec_IntPush( s->vStack, xSAT_Lit2Var( Lit ) );
+
+    while ( Vec_IntSize( s->vStack ) )
+    {
+        int v = Vec_IntPop(  s->vStack );
+        assert( (uint32_t) Vec_IntEntry( s->vReasons, v ) != CRefUndef);
+        xSAT_Clause_t* c = xSAT_SolverReadClause(s, ( uint32_t ) Vec_IntEntry( s->vReasons, v ) );
+        int* Lits = &( c->pData[0].Lit );
+        int  i;
+
+        if( c->nSize == 2 && Vec_StrEntry( s->vAssigns, xSAT_Lit2Var( Lits[0] ) ) == xSAT_LitSign( xSAT_NegLit( Lits[0] ) ) )
+        {
+            assert( Vec_StrEntry( s->vAssigns, xSAT_Lit2Var( Lits[1] ) ) == xSAT_LitSign( ( Lits[1] ) ) );
+            ABC_SWAP( int, Lits[0], Lits[1] );
+        }
+
+        for (i = 1; i < c->nSize; i++)
+        {
+            int v = xSAT_Lit2Var( Lits[i] );
+            if ( !Vec_StrEntry( s->vSeen, v ) && Vec_IntEntry( s->vLevels, v ) )
+            {
+                if ( (uint32_t) Vec_IntEntry( s->vReasons, v ) != CRefUndef && ((1 << (Vec_IntEntry( s->vLevels, v ) & 31)) & MinLevel))
+                {
+                    Vec_IntPush( s->vStack, v );
+                    Vec_IntPush( s->vTagged, Lits[i] );
+                    Vec_StrWriteEntry( s->vSeen, v, 1 );
+                }
+                else
+                {
+                    int Lit;
+                    Vec_IntForEachEntryStart( s->vTagged, Lit, i, top )
+                        Vec_StrWriteEntry( s->vSeen, xSAT_Lit2Var(Lit), 0 );
+                    Vec_IntShrink( s->vTagged, top );
+                    return 0;
+                }
+            }
+        }
+    }
+    return 1;
+}
+
+/**Function*************************************************************
+
+  Synopsis    []
+
+  Description []
+
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+static void xSAT_SolverClaMinimisation( xSAT_Solver_t * s, Vec_Int_t * vLits )
+{
+    int * pLits = Vec_IntArray( vLits );
+    int MinLevel = 0;
+    int i, j;
+
+    for ( i = 1; i < Vec_IntSize( vLits ); i++ )
+    {
+        int Level = Vec_IntEntry( s->vLevels, xSAT_Lit2Var( pLits[i] ) );
+        MinLevel |= 1 << ( Level & 31 );
+    }
+
+    /* Remove reduntant literals */
+    Vec_IntAppend( s->vTagged, vLits );
+    for ( i = j = 1; i < Vec_IntSize( vLits ); i++ )
+        if ( (uint32_t) Vec_IntEntry( s->vReasons, xSAT_Lit2Var( pLits[i] ) ) == CRefUndef || !xSAT_SolverIsLitRemovable( s, pLits[i], MinLevel ) )
+            pLits[j++] = pLits[i];
+    Vec_IntShrink( vLits, j );
+
+    /* Binary Resolution */
+    if( Vec_IntSize( vLits ) <= 30 && xSAT_SolverClaCalcLBD2( s, vLits ) <= 6 )
+    {
+        int Lit;
+        int FlaseLit = xSAT_NegLit( pLits[0] );
+
+        s->nStamp++;
+        Vec_IntForEachEntry( vLits, Lit, i )
+            Vec_IntWriteEntry( s->vStamp, xSAT_Lit2Var( Lit ), s->nStamp );
+
+        xSAT_WatchList_t * ws = xSAT_VecWatchListEntry( s->vBinWatches, FlaseLit );
+        xSAT_Watcher_t * begin = xSAT_WatchListArray( ws );
+        xSAT_Watcher_t * end   = begin + xSAT_WatchListSize( ws );
+        xSAT_Watcher_t * pWatcher;
+
+        int nb = 0;
+        for ( pWatcher = begin; pWatcher < end; pWatcher++ )
+        {
+            int ImpLit = pWatcher->Blocker;
+
+            if ( Vec_IntEntry( s->vStamp, xSAT_Lit2Var( ImpLit ) ) == s->nStamp && Vec_StrEntry( s->vAssigns, xSAT_Lit2Var( ImpLit ) ) == xSAT_LitSign( ImpLit ) )
+            {
+                nb++;
+                Vec_IntWriteEntry( s->vStamp, xSAT_Lit2Var( ImpLit ), s->nStamp - 1 );
+            }
+        }
+
+        int l = Vec_IntSize( vLits ) - 1;
+        if ( nb > 0 )
+        {
+            for ( i = 1; i < Vec_IntSize( vLits ) - nb; i++ )
+                if ( Vec_IntEntry( s->vStamp, xSAT_Lit2Var( pLits[i] ) ) != s->nStamp )
+                {
+                    int TempLit = pLits[l];
+                    pLits[l] = pLits[i];
+                    pLits[i] = TempLit;
+                    i--; l--;
+                }
+
+            Vec_IntShrink( vLits, Vec_IntSize( vLits ) - nb );
+        }
+    }
+}
+
+/**Function*************************************************************
+
+  Synopsis    []
+
+  Description []
+
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+static void xSAT_SolverAnalyze( xSAT_Solver_t* s, uint32_t ConfCRef, Vec_Int_t * vLearnt, int * OutBtLevel, unsigned * nLBD )
+{
+    int* trail   = Vec_IntArray( s->vTrail );
+    int Count     = 0;
+    int p       = LitUndef;
+    int Idx     = Vec_IntSize( s->vTrail ) - 1;
+    int* Lits;
+    int i, j;
+
+    Vec_IntPush( vLearnt, LitUndef );
+    do
+    {
+        assert( ConfCRef != CRefUndef );
+        xSAT_Clause_t * c = xSAT_SolverReadClause(s, ConfCRef);
+        Lits = &( c->pData[0].Lit );
+
+        if( p != LitUndef && c->nSize == 2 && Vec_StrEntry( s->vAssigns, xSAT_Lit2Var(Lits[0])) == xSAT_LitSign( xSAT_NegLit( Lits[0] ) ) )
+        {
+            assert( Vec_StrEntry( s->vAssigns, xSAT_Lit2Var( Lits[1] ) ) == xSAT_LitSign( ( Lits[1] ) ) );
+            ABC_SWAP( int, Lits[0], Lits[1] );
+        }
+
+        if ( c->fLearnt )
+            xSAT_SolverClaActBump( s, c );
+
+        if ( c->fLearnt && c->nLBD > 2 )
+        {
+            unsigned int nblevels = xSAT_SolverClaCalcLBD(s, c);
+            if ( nblevels + 1 < c->nLBD )
+            {
+                if (c->nLBD <= s->Config.nLBDFrozenClause)
+                    c->fCanBeDel = 0;
+                c->nLBD = nblevels;
+            }
+        }
+
+        for ( j = ( p == LitUndef ? 0 : 1 ); j < c->nSize; j++ )
+        {
+            int Var = xSAT_Lit2Var( Lits[j] );
+
+            if ( Vec_StrEntry( s->vSeen, Var ) == 0 && Vec_IntEntry( s->vLevels, Var ) > 0 )
+            {
+                Vec_StrWriteEntry( s->vSeen, Var, 1 );
+                xSAT_SolverVarActBump( s, Var );
+                if ( Vec_IntEntry( s->vLevels, Var ) >= xSAT_SolverDecisionLevel( s ) )
+                {
+                    Count++;
+                    if (  Vec_IntEntry( s->vReasons, Var ) != CRefUndef && xSAT_SolverReadClause( s, Vec_IntEntry( s->vReasons, Var ) )->fLearnt )
+                        Vec_IntPush( s->vLastDLevel, Var );
+                }
+                else
+                    Vec_IntPush( vLearnt, Lits[j] );
+            }
+        }
+
+        while ( !Vec_StrEntry( s->vSeen, xSAT_Lit2Var( trail[Idx--] ) ) );
+
+        // Next clause to look at
+        p = trail[Idx+1];
+        ConfCRef = (uint32_t) Vec_IntEntry( s->vReasons, xSAT_Lit2Var( p ) );
+        Vec_StrWriteEntry( s->vSeen, xSAT_Lit2Var( p ), 0 );
+        Count--;
+
+    } while ( Count > 0 );
+
+    Vec_IntArray( vLearnt )[0] = xSAT_NegLit( p );
+
+    xSAT_SolverClaMinimisation( s, vLearnt );
+
+    // Find the backtrack level
+    Lits = Vec_IntArray( vLearnt );
+    if ( Vec_IntSize( vLearnt ) == 1 )
+        *OutBtLevel = 0;
+    else
+    {
+        int iMax = 1;
+        int Max   = Vec_IntEntry( s->vLevels, xSAT_Lit2Var( Lits[1] ) );
+        int Tmp;
+
+        for (i = 2; i < Vec_IntSize( vLearnt ); i++)
+            if ( Vec_IntEntry( s->vLevels, xSAT_Lit2Var( Lits[i]) ) > Max)
+            {
+                Max   = Vec_IntEntry( s->vLevels, xSAT_Lit2Var( Lits[i]) );
+                iMax = i;
+            }
+
+        Tmp         = Lits[1];
+        Lits[1]     = Lits[iMax];
+        Lits[iMax]  = Tmp;
+        *OutBtLevel = Vec_IntEntry( s->vLevels, xSAT_Lit2Var( Lits[1] ) );
+    }
+
+    *nLBD = xSAT_SolverClaCalcLBD2( s, vLearnt );
+    if ( Vec_IntSize( s->vLastDLevel ) > 0 )
+    {
+        int Var;
+        Vec_IntForEachEntry( s->vLastDLevel, Var, i )
+        {
+            if ( xSAT_SolverReadClause( s, Vec_IntEntry( s->vReasons, Var ) )->nLBD < *nLBD )
+                xSAT_SolverVarActBump( s, Var );
+        }
+
+        Vec_IntClear( s->vLastDLevel );
+    }
+
+    int Lit;
+    Vec_IntForEachEntry( s->vTagged, Lit, i )
+        Vec_StrWriteEntry( s->vSeen, xSAT_Lit2Var( Lit ), 0 );
+    Vec_IntClear( s->vTagged );
+}
+
+/**Function*************************************************************
+
+  Synopsis    []
+
+  Description []
+
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+uint32_t xSAT_SolverPropagate( xSAT_Solver_t* s )
+{
+    uint32_t hConfl = CRefUndef;
+    int * Lits;
+    int NegLit;
+    int nProp = 0;
+
+    while ( s->iQhead < Vec_IntSize( s->vTrail ) )
+    {
+        int p = Vec_IntEntry( s->vTrail, s->iQhead++ );
+
+        xSAT_WatchList_t* ws = xSAT_VecWatchListEntry( s->vBinWatches, p );
+        xSAT_Watcher_t* begin = xSAT_WatchListArray( ws );
+        xSAT_Watcher_t* end   = begin + xSAT_WatchListSize( ws );
+        xSAT_Watcher_t *i, *j;
+
+        nProp++;
+        for (i = begin; i < end; i++)
+        {
+            if ( Vec_StrEntry( s->vAssigns, xSAT_Lit2Var(i->Blocker)) == xSAT_LitSign(xSAT_NegLit(i->Blocker)))
+            {
+                return i->CRef;
+            }
+            else if ( Vec_StrEntry( s->vAssigns, xSAT_Lit2Var(i->Blocker)) == VarX)
+                xSAT_SolverEnqueue(s, i->Blocker, i->CRef);
+        }
+
+
+        ws    = xSAT_VecWatchListEntry( s->vWatches, p);
+        begin = xSAT_WatchListArray( ws );
+        end   = begin + xSAT_WatchListSize( ws );
+
+        for ( i = j = begin; i < end; )
+        {
+            if ( Vec_StrEntry( s->vAssigns, xSAT_Lit2Var( i->Blocker ) ) == xSAT_LitSign( i->Blocker ) )
+            {
+                *j++ = *i++;
+                continue;
+            }
+
+            xSAT_Clause_t* c = xSAT_SolverReadClause( s, i->CRef );
+            Lits = &( c->pData[0].Lit );
+
+            // Make sure the false literal is data[1]:
+            NegLit = xSAT_NegLit( p );
+            if ( Lits[0] == NegLit )
+            {
+                Lits[0] = Lits[1];
+                Lits[1] = NegLit;
+            }
+            assert( Lits[1] == NegLit );
+
+            xSAT_Watcher_t w = { .CRef = i->CRef,
+                                 .Blocker = Lits[0] };
+            // If 0th watch is true, then clause is already satisfied.
+            if ( Lits[0] != i->Blocker && Vec_StrEntry( s->vAssigns, xSAT_Lit2Var( Lits[0] ) ) == xSAT_LitSign( Lits[0] ) )
+                *j++ = w;
+            else
+            {
+                // Look for new watch:
+                int* stop = Lits + c->nSize;
+                int* k;
+                for ( k = Lits + 2; k < stop; k++ )
+                {
+                    if (Vec_StrEntry( s->vAssigns, xSAT_Lit2Var( *k ) ) != !xSAT_LitSign( *k ) )
+                    {
+                        Lits[1] = *k;
+                        *k = NegLit;
+                        xSAT_WatchListPush( xSAT_VecWatchListEntry( s->vWatches, xSAT_NegLit( Lits[1] ) ), w );
+                        goto next;
+                    }
+                }
+
+                *j++ = w;
+
+                // Clause is unit under assignment:
+                if (Vec_StrEntry( s->vAssigns, xSAT_Lit2Var( Lits[0] ) ) == xSAT_LitSign( xSAT_NegLit( Lits[0] ) ) )
+                {
+                    hConfl = i->CRef;
+                    i++;
+                    s->iQhead = Vec_IntSize( s->vTrail );
+                    // Copy the remaining watches:
+                    while (i < end)
+                        *j++ = *i++;
+                }
+                else
+                    xSAT_SolverEnqueue( s, Lits[0], i->CRef );
+            }
+        next:
+            i++;
+        }
+
+        s->Stats.nInspects += j - xSAT_WatchListArray( ws );
+        xSAT_WatchListShrink( ws, j - xSAT_WatchListArray( ws ) );
+    }
+
+    s->Stats.nPropagations += nProp;
+    s->nPropSimplify -= nProp;
+
+    return hConfl;
+}
+
+/**Function*************************************************************
+
+  Synopsis    []
+
+  Description []
+
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+void xSAT_SolverReduceDB( xSAT_Solver_t * s )
+{
+    static abctime TimeTotal = 0;
+    abctime clk = Abc_Clock();
+    int nLearnedOld = Vec_IntSize( s->vLearnts );
+    int i, limit;
+    uint32_t CRef;
+    xSAT_Clause_t * c;
+    xSAT_Clause_t ** learnts_cls;
+
+    learnts_cls = ABC_ALLOC( xSAT_Clause_t *, nLearnedOld );
+    Vec_IntForEachEntry( s->vLearnts, CRef, i )
+        learnts_cls[i] = xSAT_SolverReadClause(s, CRef);
+
+    limit = nLearnedOld / 2;
+
+    xSAT_UtilSort((void *) learnts_cls, nLearnedOld,
+                  (int (*)( const void *, const void * )) xSAT_ClauseCompare);
+
+    if ( learnts_cls[nLearnedOld / 2]->nLBD <= 3 )
+        s->nRC2 += s->Config.nSpecialIncReduce;
+    if ( learnts_cls[nLearnedOld - 1]->nLBD <= 5 )
+        s->nRC2 += s->Config.nSpecialIncReduce;
+
+    Vec_IntClear( s->vLearnts );
+    for ( i = 0; i < nLearnedOld; i++ )
+    {
+        c = learnts_cls[i];
+        uint32_t CRef = xSAT_MemCRef( s->pMemory, (uint32_t * ) c );
+        assert(c->fMark == 0);
+        if ( c->fCanBeDel && c->nLBD > 2 && c->nSize > 2 && (uint32_t) Vec_IntEntry( s->vReasons, xSAT_Lit2Var( c->pData[0].Lit ) ) != CRef && ( i < limit ) )
+        {
+            c->fMark = 1;
+            s->Stats.nLearntLits -= c->nSize;
+            xSAT_WatchListRemove( xSAT_VecWatchListEntry( s->vWatches, xSAT_NegLit( c->pData[0].Lit ) ), CRef );
+            xSAT_WatchListRemove( xSAT_VecWatchListEntry( s->vWatches, xSAT_NegLit( c->pData[1].Lit ) ), CRef );
+        }
+        else
+        {
+            if (!c->fCanBeDel)
+                limit++;
+            c->fCanBeDel = 1;
+            Vec_IntPush( s->vLearnts, CRef );
+        }
+    }
+    ABC_FREE( learnts_cls );
+
+    TimeTotal += Abc_Clock() - clk;
+    if ( s->Config.fVerbose )
+    {
+        Abc_Print(1, "reduceDB: Keeping %7d out of %7d clauses (%5.2f %%)  ",
+            Vec_IntSize( s->vLearnts ), nLearnedOld, 100.0 * Vec_IntSize( s->vLearnts ) / nLearnedOld );
+        Abc_PrintTime( 1, "Time", TimeTotal );
+    }
+    xSAT_SolverGarbageCollect(s);
+}
+
+/**Function*************************************************************
+
+  Synopsis    []
+
+  Description []
+
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+char xSAT_SolverSearch( xSAT_Solver_t * s )
+{
+    ABC_INT64_T conflictC  = 0;
+
+    s->Stats.nStarts++;
+    for (;;)
+    {
+        uint32_t hConfl = xSAT_SolverPropagate( s );
+
+        if ( hConfl != CRefUndef )
+        {
+            /* Conflict */
+            int BacktrackLevel;
+            unsigned nLBD;
+            uint32_t CRef;
+
+            s->Stats.nConflicts++;
+            conflictC++;
+
+            if ( xSAT_SolverDecisionLevel( s ) == 0 )
+                return LBoolFalse;
+
+            xSAT_BQueuePush( s->bqTrail, Vec_IntSize( s->vTrail ) );
+            if ( s->Stats.nConflicts > s->Config.nFirstBlockRestart && xSAT_BQueueIsValid( s->bqLBD ) && ( Vec_IntSize( s->vTrail ) > ( s->Config.R * xSAT_BQueueAvg( s->bqTrail ) ) ) )
+                xSAT_BQueueClean(s->bqLBD);
+
+            Vec_IntClear( s->vLearntClause );
+            xSAT_SolverAnalyze( s, hConfl, s->vLearntClause, &BacktrackLevel, &nLBD );
+
+            s->nSumLBD += nLBD;
+            xSAT_BQueuePush( s->bqLBD, nLBD );
+            xSAT_SolverCancelUntil( s, BacktrackLevel );
+
+            CRef = Vec_IntSize( s->vLearntClause ) == 1 ? CRefUndef : xSAT_SolverClaNew( s, s->vLearntClause , 1 );
+            xSAT_SolverEnqueue( s, Vec_IntEntry( s->vLearntClause , 0 ), CRef );
+
+            xSAT_SolverVarActDecay( s );
+            xSAT_SolverClaActDecay( s );
+        }
+        else
+        {
+            /* No conflict */
+            int NextVar;
+            if ( xSAT_BQueueIsValid( s->bqLBD ) && ( ( xSAT_BQueueAvg( s->bqLBD ) * s->Config.K ) > ( s->nSumLBD / s->Stats.nConflicts ) ) )
+            {
+                xSAT_BQueueClean( s->bqLBD );
+                xSAT_SolverCancelUntil( s, 0 );
+                return LBoolUndef;
+            }
+
+            // Simplify the set of problem clauses:
+            if ( xSAT_SolverDecisionLevel( s ) == 0 )
+                xSAT_SolverSimplify( s );
+
+            // Reduce the set of learnt clauses:
+            if ( s->Stats.nConflicts >= s->nConfBeforeReduce )
+            {
+                s->nRC1 = ( s->Stats.nConflicts / s->nRC2 ) + 1;
+                xSAT_SolverReduceDB(s);
+                s->nRC2 += s->Config.nIncReduce;
+                s->nConfBeforeReduce = s->nRC1 * s->nRC2;
+            }
+
+            // New variable decision:
+            NextVar = xSAT_SolverDecide( s );
+
+            if ( NextVar == VarUndef )
+                return LBoolTrue;
+
+            xSAT_SolverNewDecision( s, xSAT_Var2Lit( NextVar, ( int ) Vec_StrEntry( s->vPolarity, NextVar ) ) );
+        }
+    }
+
+    return LBoolUndef; // cannot happen
+}
+
+/**Function*************************************************************
+
+  Synopsis    []
+
+  Description []
+
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+void xSAT_SolverClaRealloc( xSAT_Mem_t * pDest, xSAT_Mem_t * pSrc, uint32_t * pCRef )
+{
+    xSAT_Clause_t * pOldCla = xSAT_MemClauseHand( pSrc, *pCRef );
+    if ( pOldCla->fReallocd )
+    {
+        *pCRef = (uint32_t) pOldCla->nSize;
+        return;
+    }
+
+    uint32_t nNewCRef = xSAT_MemAppend( pDest, 3 + pOldCla->fLearnt + pOldCla->nSize );
+    xSAT_Clause_t * pNewCla = xSAT_MemClauseHand( pDest, nNewCRef );
+
+    memcpy( pNewCla, pOldCla, ( 3 + pOldCla->fLearnt + pOldCla->nSize ) * 4 );
+
+    pOldCla->fReallocd = 1;
+    pOldCla->nSize = (unsigned) nNewCRef;
+    *pCRef = nNewCRef;
+}
+
+/**Function*************************************************************
+
+  Synopsis    []
+
+  Description []
+
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+void xSAT_SolverGarbageCollect( xSAT_Solver_t * s )
+{
+    int i;
+    uint32_t * pArray;
+    xSAT_Mem_t * pNewMemMngr = xSAT_MemAlloc(  xSAT_MemCap( s->pMemory ) - xSAT_MemWastedCap( s->pMemory ) );
+
+    for ( i = 0; i < 2 * Vec_StrSize( s->vAssigns ); i++ )
+    {
+        xSAT_WatchList_t* ws = xSAT_VecWatchListEntry( s->vWatches, i);
+        xSAT_Watcher_t* begin = xSAT_WatchListArray(ws);
+        xSAT_Watcher_t* end   = begin + xSAT_WatchListSize(ws);
+        xSAT_Watcher_t *w;
+
+        for ( w = begin; w != end; w++ )
+            xSAT_SolverClaRealloc( pNewMemMngr, s->pMemory, &(w->CRef) );
+
+        ws = xSAT_VecWatchListEntry( s->vBinWatches, i);
+        begin = xSAT_WatchListArray(ws);
+        end   = begin + xSAT_WatchListSize(ws);
+        for ( w = begin; w != end; w++ )
+            xSAT_SolverClaRealloc( pNewMemMngr, s->pMemory, &(w->CRef) );
+    }
+
+    for ( i = 0; i < Vec_IntSize( s->vTrail ); i++ )
+        if ( (uint32_t) Vec_IntEntry( s->vReasons, xSAT_Lit2Var( Vec_IntEntry( s->vTrail, i ) ) ) != CRefUndef )
+            xSAT_SolverClaRealloc( pNewMemMngr, s->pMemory, &( Vec_IntArray( s->vReasons )[xSAT_Lit2Var( Vec_IntEntry( s->vTrail, i ) )] ) );
+
+    pArray = ( uint32_t * ) Vec_IntArray( s->vLearnts );
+    for ( i = 0; i < Vec_IntSize( s->vLearnts ); i++ )
+        xSAT_SolverClaRealloc( pNewMemMngr, s->pMemory, &(pArray[i]) );
+
+    pArray = (uint32_t *) Vec_IntArray( s->vClauses );
+    for ( i = 0; i < Vec_IntSize( s->vClauses ); i++ )
+        xSAT_SolverClaRealloc( pNewMemMngr, s->pMemory, &(pArray[i]) );
+
+    xSAT_MemFree( s->pMemory );
+    s->pMemory = pNewMemMngr;
+}
+
+ABC_NAMESPACE_IMPL_END