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.

13 files changed, 3151 insertions, 0 deletions

diff --git a/src/sat/xsat/license b/src/sat/xsat/license
new file mode 100644
index 00000000..a6389ab1
--- /dev/null
+++ b/src/sat/xsat/license
@@ -0,0 +1,39 @@
+xSAT - Copyright (c) 2016, Bruno Schmitt - UC Berkeley / UFRGS (boschmitt@inf.ufrgs.br)
+
+xSAT is based on Glucose v3(see Glucose copyrights below) and ABC C version of
+MiniSat (bsat) developed by Niklas Sorensson and modified by Alan Mishchenko.
+Permissions and copyrights of xSAT are exactly the same as Glucose v3/Minisat.
+(see below).
+
+---------------
+
+Glucose -- Copyright (c) 2013, Gilles Audemard, Laurent Simon
+                               CRIL - Univ. Artois, France
+                               LRI  - Univ. Paris Sud, France
+
+Glucose sources are based on MiniSat (see below MiniSat copyrights). Permissions
+and copyrights of Glucose are exactly the same as Minisat on which it is based
+on. (see below).
+
+---------------
+
+Copyright (c) 2003-2006, Niklas Een, Niklas Sorensson
+Copyright (c) 2007-2010, Niklas Sorensson
+
+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.
+*******************************************************************************/
diff --git a/src/sat/xsat/module.make b/src/sat/xsat/module.make
new file mode 100644
index 00000000..1d7352e2
--- /dev/null
+++ b/src/sat/xsat/module.make
@@ -0,0 +1,3 @@
+SRC +=  src/sat/xsat/xsatSolver.c \
+    src/sat/xsat/xsatSolverAPI.c \
+    src/sat/xsat/xsatCnfReader.c
diff --git a/src/sat/xsat/xsat.h b/src/sat/xsat/xsat.h
new file mode 100644
index 00000000..b2962d91
--- /dev/null
+++ b/src/sat/xsat/xsat.h
@@ -0,0 +1,59 @@
+/**CFile****************************************************************
+
+  FileName    [xsat.h]
+
+  SystemName  [ABC: Logic synthesis and verification system.]
+
+  PackageName [xSAT - A SAT solver written in C. 
+               Read the license file for more info.]
+
+  Synopsis    [External definitions of the solver.]
+
+  Author      [Bruno Schmitt <boschmitt@inf.ufrgs.br>]
+
+  Affiliation [UC Berkeley / UFRGS]
+
+  Date        [Ver. 1.0. Started - November 10, 2016.]
+
+  Revision    []
+
+***********************************************************************/
+#ifndef ABC__sat__xSAT__xSAT_h
+#define ABC__sat__xSAT__xSAT_h
+
+////////////////////////////////////////////////////////////////////////
+///                          INCLUDES                                ///
+////////////////////////////////////////////////////////////////////////
+#include "misc/util/abc_global.h"
+#include "misc/vec/vecInt.h"
+
+ABC_NAMESPACE_HEADER_START
+
+////////////////////////////////////////////////////////////////////////
+///                    STRUCTURE DEFINITIONS                         ///
+////////////////////////////////////////////////////////////////////////
+struct xSAT_Solver_t_;
+typedef struct xSAT_Solver_t_ xSAT_Solver_t;
+
+////////////////////////////////////////////////////////////////////////
+///                     FUNCTION DECLARATIONS                        ///
+////////////////////////////////////////////////////////////////////////
+/*=== xsatCnfReader.c ================================================*/
+extern int xSAT_SolverParseDimacs( FILE *, xSAT_Solver_t ** );
+
+/*=== xsatSolverAPI.c ================================================*/
+extern xSAT_Solver_t * xSAT_SolverCreate();
+extern void xSAT_SolverDestroy( xSAT_Solver_t * );
+
+extern int xSAT_SolverAddClause( xSAT_Solver_t *, Vec_Int_t * );
+extern int xSAT_SolverSimplify( xSAT_Solver_t * );
+extern int xSAT_SolverSolve( xSAT_Solver_t * );
+
+extern void xSAT_SolverPrintStats( xSAT_Solver_t * );
+
+ABC_NAMESPACE_HEADER_END
+
+#endif
+////////////////////////////////////////////////////////////////////////
+///                       END OF FILE                                ///
+////////////////////////////////////////////////////////////////////////
diff --git a/src/sat/xsat/xsatBQueue.h b/src/sat/xsat/xsatBQueue.h
new file mode 100644
index 00000000..37951684
--- /dev/null
+++ b/src/sat/xsat/xsatBQueue.h
@@ -0,0 +1,189 @@
+/**CFile****************************************************************
+
+  FileName    [xsatBQueue.h]
+
+  SystemName  [ABC: Logic synthesis and verification system.]
+
+  PackageName [xSAT - A SAT solver written in C.
+               Read the license file for more info.]
+
+  Synopsis    [Bounded queue implementation.]
+
+  Author      [Bruno Schmitt <boschmitt@inf.ufrgs.br>]
+
+  Affiliation [UC Berkeley / UFRGS]
+
+  Date        [Ver. 1.0. Started - November 10, 2016.]
+
+  Revision    []
+
+***********************************************************************/
+#ifndef ABC__sat__xSAT__xsatBQueue_h
+#define ABC__sat__xSAT__xsatBQueue_h
+
+////////////////////////////////////////////////////////////////////////
+///                          INCLUDES                                ///
+////////////////////////////////////////////////////////////////////////
+#include "misc/util/abc_global.h"
+
+ABC_NAMESPACE_HEADER_START
+
+////////////////////////////////////////////////////////////////////////
+///                    STRUCTURE DEFINITIONS                         ///
+////////////////////////////////////////////////////////////////////////
+typedef struct xSAT_BQueue_t_ xSAT_BQueue_t;
+struct xSAT_BQueue_t_
+{
+    int nSize;
+    int nCap;
+    int iFirst;
+    int iEmpty;
+    uint64_t nSum;
+    uint32_t * pData;
+};
+
+////////////////////////////////////////////////////////////////////////
+///                     FUNCTION DECLARATIONS                        ///
+////////////////////////////////////////////////////////////////////////
+/**Function*************************************************************
+
+  Synopsis    []
+
+  Description []
+
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+static inline xSAT_BQueue_t * xSAT_BQueueNew( int nCap )
+{
+    xSAT_BQueue_t * p = ABC_CALLOC( xSAT_BQueue_t, 1 );
+    p->nCap = nCap;
+    p->pData = ABC_CALLOC( uint32_t, nCap );
+    return p;
+}
+
+/**Function*************************************************************
+
+  Synopsis    []
+
+  Description []
+
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+static inline void xSAT_BQueueFree( xSAT_BQueue_t * p )
+{
+    ABC_FREE( p->pData );
+    ABC_FREE( p );
+}
+
+/**Function*************************************************************
+
+  Synopsis    []
+
+  Description []
+
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+static inline void xSAT_BQueuePush( xSAT_BQueue_t * p, uint32_t Value )
+{
+    if ( p->nSize == p->nCap )
+    {
+        assert(p->iFirst == p->iEmpty);
+        p->nSum -= p->pData[p->iFirst];
+        p->iFirst = ( p->iFirst + 1 ) % p->nCap;
+    }
+    else
+        p->nSize++;
+
+    p->nSum += Value;
+    p->pData[p->iEmpty] = Value;
+    if ( ( ++p->iEmpty ) == p->nCap )
+    {
+        p->iEmpty = 0;
+        p->iFirst = 0;
+    }
+}
+
+/**Function*************************************************************
+
+  Synopsis    []
+
+  Description []
+
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+static inline int xSAT_BQueuePop( xSAT_BQueue_t * p )
+{
+    assert( p->nSize >= 1 );
+    int RetValue = p->pData[p->iFirst];
+    p->nSum -= RetValue;
+    p->iFirst = ( p->iFirst + 1 ) % p->nCap;
+    p->nSize--;
+    return RetValue;
+}
+
+/**Function*************************************************************
+
+  Synopsis    []
+
+  Description []
+
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+static inline uint32_t xSAT_BQueueAvg( xSAT_BQueue_t * p )
+{
+    return ( uint32_t )( p->nSum / ( ( uint64_t ) p->nSize ) );
+}
+
+/**Function*************************************************************
+
+  Synopsis    []
+
+  Description []
+
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+static inline int xSAT_BQueueIsValid( xSAT_BQueue_t * p )
+{
+    return ( p->nCap == p->nSize );
+}
+
+/**Function*************************************************************
+
+  Synopsis    []
+
+  Description []
+
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+static inline void xSAT_BQueueClean( xSAT_BQueue_t * p )
+{
+    p->iFirst = 0;
+    p->iEmpty = 0;
+    p->nSize = 0;
+    p->nSum = 0;
+}
+
+ABC_NAMESPACE_HEADER_END
+
+#endif
diff --git a/src/sat/xsat/xsatClause.h b/src/sat/xsat/xsatClause.h
new file mode 100644
index 00000000..39f0a0c8
--- /dev/null
+++ b/src/sat/xsat/xsatClause.h
@@ -0,0 +1,109 @@
+/**CFile****************************************************************
+
+  FileName    [xsatClause.h]
+
+  SystemName  [ABC: Logic synthesis and verification system.]
+
+  PackageName [xSAT - A SAT solver written in C.
+               Read the license file for more info.]
+
+  Synopsis    [Clause data type definition.]
+
+  Author      [Bruno Schmitt <boschmitt@inf.ufrgs.br>]
+
+  Affiliation [UC Berkeley / UFRGS]
+
+  Date        [Ver. 1.0. Started - November 10, 2016.]
+
+  Revision    []
+
+***********************************************************************/
+#ifndef ABC__sat__xSAT__xsatClause_h
+#define ABC__sat__xSAT__xsatClause_h
+
+////////////////////////////////////////////////////////////////////////
+///                          INCLUDES                                ///
+////////////////////////////////////////////////////////////////////////
+#include "misc/util/abc_global.h"
+
+ABC_NAMESPACE_HEADER_START
+
+////////////////////////////////////////////////////////////////////////
+///                    STRUCTURE DEFINITIONS                         ///
+////////////////////////////////////////////////////////////////////////
+typedef struct xSAT_Clause_t_ xSAT_Clause_t;
+struct xSAT_Clause_t_
+{
+    unsigned fLearnt   :  1;
+    unsigned fMark     :  1;
+    unsigned fReallocd :  1;
+    unsigned fCanBeDel :  1;
+    unsigned nLBD      : 28;
+    unsigned nSize;
+    union {
+        int Lit;
+        unsigned Act;
+    } pData[0];
+};
+
+////////////////////////////////////////////////////////////////////////
+///                     FUNCTION DECLARATIONS                        ///
+////////////////////////////////////////////////////////////////////////
+/**Function*************************************************************
+
+  Synopsis    []
+
+  Description []
+
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+static int xSAT_ClauseCompare( const void * p1, const void * p2 )
+{
+    xSAT_Clause_t * pC1 = ( xSAT_Clause_t * ) p1;
+    xSAT_Clause_t * pC2 = ( xSAT_Clause_t * ) p2;
+
+    if ( pC1->nSize > 2 && pC2->nSize == 2 )
+        return 1;
+    if ( pC1->nSize == 2 && pC2->nSize > 2 )
+        return 0;
+    if ( pC1->nSize == 2 && pC2->nSize == 2 )
+        return 0;
+
+    if ( pC1->nLBD > pC2->nLBD )
+        return 1;
+    if ( pC1->nLBD < pC2->nLBD )
+        return 0;
+
+    return pC1->pData[pC1->nSize].Act < pC2->pData[pC2->nSize].Act;
+}
+
+/**Function*************************************************************
+
+  Synopsis    []
+
+  Description []
+
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+static void xSAT_ClausePrint( xSAT_Clause_t * pCla )
+{
+    int i;
+
+    printf("{ ");
+    for ( i = 0; i < pCla->nSize; i++ )
+        printf("%d ", pCla->pData[i].Lit );
+    printf("}\n");
+}
+
+ABC_NAMESPACE_HEADER_END
+
+#endif
+////////////////////////////////////////////////////////////////////////
+///                       END OF FILE                                ///
+////////////////////////////////////////////////////////////////////////
diff --git a/src/sat/xsat/xsatCnfReader.c b/src/sat/xsat/xsatCnfReader.c
new file mode 100644
index 00000000..d23e8a0a
--- /dev/null
+++ b/src/sat/xsat/xsatCnfReader.c
@@ -0,0 +1,236 @@
+/**CFile****************************************************************
+
+  FileName    [xsatCnfReader.h]
+
+  SystemName  [ABC: Logic synthesis and verification system.]
+
+  PackageName [xSAT - A SAT solver written in C.
+               Read the license file for more info.]
+
+  Synopsis    [CNF DIMACS file format parser.]
+
+  Author      [Bruno Schmitt <boschmitt@inf.ufrgs.br>]
+
+  Affiliation [UC Berkeley / UFRGS]
+
+  Date        [Ver. 1.0. Started - November 10, 2016.]
+
+  Revision    []
+
+***********************************************************************/
+
+////////////////////////////////////////////////////////////////////////
+///                          INCLUDES                                ///
+////////////////////////////////////////////////////////////////////////
+#include <ctype.h>
+
+#include "misc/util/abc_global.h"
+#include "misc/vec/vecInt.h"
+
+#include "xsatSolver.h"
+
+ABC_NAMESPACE_IMPL_START
+
+////////////////////////////////////////////////////////////////////////
+///                     FUNCTION DEFINITIONS                         ///
+////////////////////////////////////////////////////////////////////////
+
+/**Function*************************************************************
+
+  Synopsis    [Read the file into the internal buffer.]
+
+  Description []
+
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+char * xSAT_FileRead( FILE * pFile )
+{
+    int nFileSize;
+    char * pBuffer;
+    int RetValue;
+    // get the file size, in bytes
+    fseek( pFile, 0, SEEK_END );
+    nFileSize = ftell( pFile );
+    // move the file current reading position to the beginning
+    rewind( pFile );
+    // load the contents of the file into memory
+    pBuffer = ABC_ALLOC( char, nFileSize + 3 );
+    RetValue = fread( pBuffer, nFileSize, 1, pFile );
+    // terminate the string with '\0'
+    pBuffer[ nFileSize + 0] = '\n';
+    pBuffer[ nFileSize + 1] = '\0';
+    return pBuffer;
+}
+
+/**Function*************************************************************
+
+  Synopsis    []
+
+  Description []
+
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+static void skipLine( char ** pIn )
+{
+    while ( 1 )
+    {
+        if (**pIn == 0)
+            return;
+        if (**pIn == '\n')
+        {
+            (*pIn)++;
+            return;
+        }
+        (*pIn)++;
+    }
+}
+
+/**Function*************************************************************
+
+  Synopsis    []
+
+  Description []
+
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+static int xSAT_ReadInt( char ** pIn )
+{
+    int val = 0;
+    int neg = 0;
+
+    for(; isspace(**pIn); (*pIn)++);
+    if ( **pIn == '-' )
+        neg = 1,
+        (*pIn)++;
+    else if ( **pIn == '+' )
+        (*pIn)++;
+    if ( !isdigit(**pIn) )
+        fprintf(stderr, "PARSE ERROR! Unexpected char: %c\n", **pIn),
+        exit(1);
+    while ( isdigit(**pIn) )
+        val = val*10 + (**pIn - '0'),
+        (*pIn)++;
+    return neg ? -val : val;
+}
+
+/**Function*************************************************************
+
+  Synopsis    []
+
+  Description []
+
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+static void xSAT_ReadClause( char ** pIn, xSAT_Solver_t * p, Vec_Int_t * vLits )
+{
+    int token, var, sign;
+
+    Vec_IntClear( vLits );
+    while ( 1 )
+    {
+        token = xSAT_ReadInt( pIn );
+        if ( token == 0 )
+            break;
+        var = abs(token) - 1;
+        sign = (token > 0);
+        Vec_IntPush( vLits, xSAT_Var2Lit( var, !sign ) );
+    }
+}
+
+/**Function*************************************************************
+
+  Synopsis    []
+
+  Description []
+
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+static int xSAT_ParseDimacs( char * pText, xSAT_Solver_t ** pS )
+{
+    xSAT_Solver_t * p = NULL;
+    Vec_Int_t * vLits = NULL;
+    char * pIn = pText;
+    int nVars, nClas;
+    while ( 1 )
+    {
+        for(; isspace(*pIn); pIn++);
+        if ( *pIn == 0 )
+            break;
+        else if ( *pIn == 'c' )
+            skipLine( &pIn );
+        else if ( *pIn == 'p' )
+        {
+            pIn++;
+            for(; isspace(*pIn); pIn++);
+            for(; !isspace(*pIn); pIn++);
+
+            nVars = xSAT_ReadInt( &pIn );
+            nClas = xSAT_ReadInt( &pIn );
+            skipLine( &pIn );
+
+            /* start the solver */
+            p = xSAT_SolverCreate();
+            /* allocate the vector */
+            vLits = Vec_IntAlloc( nVars );
+        }
+        else
+        {
+            if ( p == NULL )
+            {
+                printf( "There is no parameter line.\n" );
+                exit(1);
+            }
+            xSAT_ReadClause( &pIn, p, vLits );
+            if ( !xSAT_SolverAddClause( p, vLits ) )
+            {
+                Vec_IntPrint(vLits);
+                return 0;
+            }
+        }
+    }
+    Vec_IntFree( vLits );
+    *pS = p;
+    return xSAT_SolverSimplify( p );
+}
+
+/**Function*************************************************************
+
+  Synopsis    [Starts the solver and reads the DIMAC file.]
+
+  Description [Returns FALSE upon immediate conflict.]
+
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+int xSAT_SolverParseDimacs( FILE * pFile, xSAT_Solver_t ** p )
+{
+    char * pText;
+    int  Value;
+    pText = xSAT_FileRead( pFile );
+    Value = xSAT_ParseDimacs( pText, p );
+    ABC_FREE( pText );
+    return Value;
+}
+
+ABC_NAMESPACE_IMPL_END
+
+////////////////////////////////////////////////////////////////////////
+///                       END OF FILE                                ///
+////////////////////////////////////////////////////////////////////////
diff --git a/src/sat/xsat/xsatHeap.h b/src/sat/xsat/xsatHeap.h
new file mode 100644
index 00000000..2e873e59
--- /dev/null
+++ b/src/sat/xsat/xsatHeap.h
@@ -0,0 +1,330 @@
+/**CFile****************************************************************
+
+  FileName    [xsatHeap.h]
+
+  SystemName  [ABC: Logic synthesis and verification system.]
+
+  PackageName [xSAT - A SAT solver written in C.
+               Read the license file for more info.]
+
+  Synopsis    [Heap implementation.]
+
+  Author      [Bruno Schmitt <boschmitt@inf.ufrgs.br>]
+
+  Affiliation [UC Berkeley / UFRGS]
+
+  Date        [Ver. 1.0. Started - November 10, 2016.]
+
+  Revision    []
+
+***********************************************************************/
+#ifndef ABC__sat__xSAT__xsatHeap_h
+#define ABC__sat__xSAT__xsatHeap_h
+
+#include "misc/util/abc_global.h"
+#include "misc/vec/vecInt.h"
+
+ABC_NAMESPACE_HEADER_START
+
+////////////////////////////////////////////////////////////////////////
+///                    STRUCTURE DEFINITIONS                         ///
+////////////////////////////////////////////////////////////////////////
+typedef struct xSAT_Heap_t_ xSAT_Heap_t;
+struct xSAT_Heap_t_
+{
+    Vec_Int_t * vActivity;
+    Vec_Int_t * vIndices;
+    Vec_Int_t * vHeap;
+};
+
+/**Function*************************************************************
+
+  Synopsis    []
+
+  Description []
+
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+inline int xSAT_HeapSize( xSAT_Heap_t * h )
+{
+    return Vec_IntSize( h->vHeap );
+}
+
+/**Function*************************************************************
+
+  Synopsis    []
+
+  Description []
+
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+inline int xSAT_HeapInHeap( xSAT_Heap_t * h, int Var )
+{
+    return ( Var < Vec_IntSize( h->vIndices ) ) && ( Vec_IntEntry( h->vIndices, Var ) >= 0 );
+}
+
+static inline int Left  ( int i ) { return 2 * i + 1; }
+static inline int Right ( int i ) { return ( i + 1 ) * 2; }
+static inline int Parent( int i ) { return ( i - 1 ) >> 1; }
+static inline int Compare( xSAT_Heap_t * p, int x, int y )
+{
+    return ( unsigned )Vec_IntEntry( p->vActivity, x ) > ( unsigned )Vec_IntEntry( p->vActivity, y );
+}
+
+/**Function*************************************************************
+
+  Synopsis    []
+
+  Description []
+
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+static inline void xSAT_HeapPercolateUp( xSAT_Heap_t * h, int i )
+{
+    int x = Vec_IntEntry( h->vHeap, i );
+    int p = Parent( i );
+
+    while ( i != 0 && Compare( h, x, Vec_IntEntry( h->vHeap, p ) ) )
+    {
+        Vec_IntWriteEntry( h->vHeap, i, Vec_IntEntry( h->vHeap, p ) );
+        Vec_IntWriteEntry( h->vIndices, Vec_IntEntry( h->vHeap, p ), i );
+        i = p;
+        p = Parent(p);
+    }
+    Vec_IntWriteEntry( h->vHeap, i, x );
+    Vec_IntWriteEntry( h->vIndices, x, i );
+}
+
+/**Function*************************************************************
+
+  Synopsis    []
+
+  Description []
+
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+static inline void xSAT_HeapPercolateDown( xSAT_Heap_t * h, int i )
+{
+    int x = Vec_IntEntry( h->vHeap, i );
+
+    while ( Left( i ) < Vec_IntSize( h->vHeap ) )
+    {
+        int child = Right( i ) < Vec_IntSize( h->vHeap ) &&
+                    Compare( h, Vec_IntEntry( h->vHeap, Right( i ) ), Vec_IntEntry( h->vHeap, Left( i ) ) ) ?
+                    Right( i ) : Left( i );
+
+        if ( !Compare( h, Vec_IntEntry( h->vHeap, child ), x ) )
+            break;
+
+        Vec_IntWriteEntry( h->vHeap, i, Vec_IntEntry( h->vHeap, child ) );
+        Vec_IntWriteEntry( h->vIndices, Vec_IntEntry( h->vHeap, i ), i );
+        i = child;
+    }
+    Vec_IntWriteEntry( h->vHeap, i, x );
+    Vec_IntWriteEntry( h->vIndices, x, i );
+}
+
+////////////////////////////////////////////////////////////////////////
+///                     FUNCTION DEFINITIONS                         ///
+////////////////////////////////////////////////////////////////////////
+
+/**Function*************************************************************
+
+  Synopsis    []
+
+  Description []
+
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+static inline xSAT_Heap_t * xSAT_HeapAlloc( Vec_Int_t * vActivity )
+{
+    xSAT_Heap_t * p = ABC_ALLOC( xSAT_Heap_t, 1 );
+    p->vActivity = vActivity;
+    p->vIndices = Vec_IntAlloc( 0 );
+    p->vHeap = Vec_IntAlloc( 0 );
+
+    return p;
+}
+
+/**Function*************************************************************
+
+  Synopsis    []
+
+  Description []
+
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+static inline void xSAT_HeapFree( xSAT_Heap_t * p )
+{
+    Vec_IntFree( p->vIndices );
+    Vec_IntFree( p->vHeap );
+    ABC_FREE( p );
+}
+
+/**Function*************************************************************
+
+  Synopsis    []
+
+  Description []
+
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+static inline void xSAT_HeapIncrease( xSAT_Heap_t * h, int e )
+{
+    assert( xSAT_HeapInHeap( h, e ) );
+    xSAT_HeapPercolateDown( h, Vec_IntEntry( h->vIndices, e ) );
+}
+
+/**Function*************************************************************
+
+  Synopsis    []
+
+  Description []
+
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+static inline void xSAT_HeapDecrease( xSAT_Heap_t * p, int e )
+{
+    assert( xSAT_HeapInHeap( p, e ) );
+    xSAT_HeapPercolateUp( p , Vec_IntEntry( p->vIndices, e ) );
+}
+
+/**Function*************************************************************
+
+  Synopsis    []
+
+  Description []
+
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+static inline void xSAT_HeapInsert( xSAT_Heap_t * p, int n )
+{
+    Vec_IntFillExtra( p->vIndices, n + 1, -1);
+    assert( !xSAT_HeapInHeap( p, n ) );
+
+    Vec_IntWriteEntry( p->vIndices, n, Vec_IntSize( p->vHeap ) );
+    Vec_IntPush( p->vHeap, n );
+    xSAT_HeapPercolateUp( p, Vec_IntEntry( p->vIndices, n ) );
+}
+
+/**Function*************************************************************
+
+  Synopsis    []
+
+  Description []
+
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+static inline void xSAT_HeapUpdate( xSAT_Heap_t * p, int i )
+{
+    if ( !xSAT_HeapInHeap( p, i ) )
+        xSAT_HeapInsert( p, i );
+    else
+    {
+        xSAT_HeapPercolateUp( p, Vec_IntEntry( p->vIndices, i ) );
+        xSAT_HeapPercolateDown( p, Vec_IntEntry( p->vIndices, i ) );
+    }
+}
+
+/**Function*************************************************************
+
+  Synopsis    []
+
+  Description []
+
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+static inline void xSAT_HeapBuild( xSAT_Heap_t * p, Vec_Int_t * Vars )
+{
+    int i, Var;
+
+    Vec_IntForEachEntry( p->vHeap, Var, i )
+        Vec_IntWriteEntry( p->vIndices, Var, -1 );
+    Vec_IntClear( p->vHeap );
+
+    Vec_IntForEachEntry( Vars, Var, i )
+    {
+        Vec_IntWriteEntry( p->vIndices, Var, i );
+        Vec_IntPush( p->vHeap, Var );
+    }
+
+    for ( ( i = Vec_IntSize( p->vHeap ) / 2 - 1 ); i >= 0; i-- )
+        xSAT_HeapPercolateDown( p, i );
+}
+
+/**Function*************************************************************
+
+  Synopsis    []
+
+  Description []
+
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+static inline void xSAT_HeapClear( xSAT_Heap_t * p )
+{
+    Vec_IntFill( p->vIndices, Vec_IntSize( p->vIndices ), -1 );
+    Vec_IntClear( p->vHeap );
+}
+
+/**Function*************************************************************
+
+  Synopsis    []
+
+  Description []
+
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+static inline int xSAT_HeapRemoveMin( xSAT_Heap_t * p )
+{
+    int x = Vec_IntEntry( p->vHeap, 0 );
+    Vec_IntWriteEntry( p->vHeap, 0, Vec_IntEntryLast( p->vHeap ) );
+    Vec_IntWriteEntry( p->vIndices, Vec_IntEntry( p->vHeap, 0), 0 );
+    Vec_IntWriteEntry( p->vIndices, x, -1 );
+    Vec_IntPop( p->vHeap );
+    if ( Vec_IntSize( p->vHeap ) > 1 )
+        xSAT_HeapPercolateDown( p, 0 );
+    return x;
+}
+
+ABC_NAMESPACE_HEADER_END
+
+#endif
diff --git a/src/sat/xsat/xsatMemory.h b/src/sat/xsat/xsatMemory.h
new file mode 100644
index 00000000..3a961b97
--- /dev/null
+++ b/src/sat/xsat/xsatMemory.h
@@ -0,0 +1,225 @@
+/**CFile****************************************************************
+
+  FileName    [xsatMemory.h]
+
+  SystemName  [ABC: Logic synthesis and verification system.]
+
+  PackageName [xSAT - A SAT solver written in C.
+               Read the license file for more info.]
+
+  Synopsis    [Memory management implementation.]
+
+  Author      [Bruno Schmitt <boschmitt@inf.ufrgs.br>]
+
+  Affiliation [UC Berkeley / UFRGS]
+
+  Date        [Ver. 1.0. Started - November 10, 2016.]
+
+  Revision    []
+
+***********************************************************************/
+#ifndef ABC__sat__xSAT__xsatMemory_h
+#define ABC__sat__xSAT__xsatMemory_h
+
+////////////////////////////////////////////////////////////////////////
+///                          INCLUDES                                ///
+////////////////////////////////////////////////////////////////////////
+#include "misc/util/abc_global.h"
+
+#include "xsatClause.h"
+
+ABC_NAMESPACE_HEADER_START
+
+////////////////////////////////////////////////////////////////////////
+///                    STRUCTURE DEFINITIONS                         ///
+////////////////////////////////////////////////////////////////////////
+typedef struct xSAT_Mem_t_ xSAT_Mem_t;
+struct xSAT_Mem_t_
+{
+    uint32_t   nSize;
+    uint32_t   nCap;
+    uint32_t   nWasted;
+    uint32_t * pData;
+};
+
+////////////////////////////////////////////////////////////////////////
+///                     FUNCTION DECLARATIONS                        ///
+////////////////////////////////////////////////////////////////////////
+/**Function*************************************************************
+
+  Synopsis    []
+
+  Description []
+
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+static inline xSAT_Clause_t *  xSAT_MemClauseHand( xSAT_Mem_t * p, int h )
+{
+    return h != UINT32_MAX ? ( xSAT_Clause_t * )( p->pData + h ) : NULL;
+}
+
+/**Function*************************************************************
+
+  Synopsis    []
+
+  Description []
+
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+static inline void xSAT_MemGrow( xSAT_Mem_t * p, uint32_t nCap )
+{
+    if ( p->nCap >= nCap )
+        return;
+
+    uint32_t nPrevCap = p->nCap;
+    while (p->nCap < nCap)
+    {
+        uint32_t delta = ((p->nCap >> 1) + (p->nCap >> 3) + 2) & ~1;
+        p->nCap += delta;
+        assert(p->nCap >= nPrevCap);
+    }
+
+    assert(p->nCap > 0);
+    p->pData = ABC_REALLOC(uint32_t, p->pData, p->nCap);
+}
+
+/**Function*************************************************************
+
+  Synopsis    [Allocating vector.]
+
+  Description []
+
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+static inline xSAT_Mem_t * xSAT_MemAlloc( int nCap )
+{
+    xSAT_Mem_t * p;
+    p = ABC_CALLOC( xSAT_Mem_t, 1 );
+    if (nCap <= 0)
+        nCap = 1024*1024;
+
+    xSAT_MemGrow(p, nCap);
+    return p;
+}
+
+/**Function*************************************************************
+
+  Synopsis    [Resetting vector.]
+
+  Description []
+
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+static inline void xSAT_MemRestart( xSAT_Mem_t * p )
+{
+    p->nSize = 0;
+    p->nWasted = 0;
+}
+
+/**Function*************************************************************
+
+  Synopsis    [Freeing vector.]
+
+  Description []
+
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+static inline void xSAT_MemFree( xSAT_Mem_t * p )
+{
+    ABC_FREE( p->pData );
+    ABC_FREE( p );
+}
+
+/**Function*************************************************************
+
+  Synopsis    [Creates new clause.]
+
+  Description [The resulting clause is fully initialized.]
+
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+static inline uint32_t xSAT_MemAppend( xSAT_Mem_t * p, int nSize )
+{
+    assert(nSize > 0);
+    xSAT_MemGrow(p, p->nSize + nSize);
+
+    uint32_t nPrevSize = p->nSize;
+    p->nSize += nSize;
+    assert(p->nSize > nPrevSize);
+
+    return nPrevSize;
+}
+
+/**Function*************************************************************
+
+  Synopsis    []
+
+  Description []
+
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+static inline uint32_t xSAT_MemCRef( xSAT_Mem_t * p, uint32_t * pC )
+{
+    return ( uint32_t )( pC - &(p->pData[0]) );
+}
+
+/**Function*************************************************************
+
+  Synopsis    []
+
+  Description []
+
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+static inline uint32_t xSAT_MemCap( xSAT_Mem_t * p )
+{
+    return p->nCap;
+}
+
+/**Function*************************************************************
+
+  Synopsis    []
+
+  Description []
+
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+static inline uint32_t xSAT_MemWastedCap( xSAT_Mem_t * p )
+{
+    return p->nWasted;
+}
+
+ABC_NAMESPACE_HEADER_END
+
+#endif
+
+////////////////////////////////////////////////////////////////////////
+///                       END OF FILE                                ///
+////////////////////////////////////////////////////////////////////////
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
diff --git a/src/sat/xsat/xsatSolver.h b/src/sat/xsat/xsatSolver.h
new file mode 100644
index 00000000..a6d646c6
--- /dev/null
+++ b/src/sat/xsat/xsatSolver.h
@@ -0,0 +1,247 @@
+/**CFile****************************************************************
+
+  FileName    [xsatSolver.h]
+
+  SystemName  [ABC: Logic synthesis and verification system.]
+
+  PackageName [xSAT - A SAT solver written in C.
+               Read the license file for more info.]
+
+  Synopsis    [Internal definitions of the solver.]
+
+  Author      [Bruno Schmitt <boschmitt@inf.ufrgs.br>]
+
+  Affiliation [UC Berkeley / UFRGS]
+
+  Date        [Ver. 1.0. Started - November 10, 2016.]
+
+  Revision    []
+
+***********************************************************************/
+#ifndef ABC__sat__xSAT__xsatSolver_h
+#define ABC__sat__xSAT__xsatSolver_h
+
+////////////////////////////////////////////////////////////////////////
+///                          INCLUDES                                ///
+////////////////////////////////////////////////////////////////////////
+#include <stdio.h>
+#include <stdlib.h>
+#include <string.h>
+#include <assert.h>
+
+#include "misc/util/abc_global.h"
+#include "misc/vec/vecStr.h"
+
+#include "xsat.h"
+#include "xsatBQueue.h"
+#include "xsatClause.h"
+#include "xsatHeap.h"
+#include "xsatMemory.h"
+#include "xsatWatchList.h"
+
+ABC_NAMESPACE_HEADER_START
+
+#ifndef __cplusplus
+#ifndef false
+#  define false 0
+#endif
+#ifndef true
+#  define true 1
+#endif
+#endif
+
+enum
+{
+    Var0 = 1,
+    Var1 = 0,
+    VarX = 3
+};
+
+enum
+{
+    LBoolUndef =  0,
+    LBoolTrue  =  1,
+    LBoolFalse = -1
+};
+
+enum
+{
+    VarUndef = -1,
+    LitUndef = -2
+};
+
+#define CRefUndef UINT32_MAX
+
+////////////////////////////////////////////////////////////////////////
+///                    STRUCTURE DEFINITIONS                         ///
+////////////////////////////////////////////////////////////////////////
+typedef struct xSAT_SolverOptions_t_ xSAT_SolverOptions_t;
+struct xSAT_SolverOptions_t_
+{
+    char fVerbose;
+
+    // Limits
+    ABC_INT64_T nConfLimit;    // external limit on the number of conflicts
+    ABC_INT64_T nInsLimit;     // external limit on the number of implications
+    abctime     nRuntimeLimit; // external limit on runtime
+
+    // Constants used for restart heuristic
+    double K; // Forces a restart
+    double R; // Block a restart
+    int nFirstBlockRestart; // Lower bound number of conflicts for start blocking restarts
+    int nSizeLBDQueue;      // Size of the moving avarege queue for LBD (force restart)
+    int nSizeTrailQueue;    // Size of the moving avarege queue for Trail size (block restart)
+
+    // Constants used for clause database reduction heuristic
+    int nConfFirstReduce;  // Number of conflicts before first reduction
+    int nIncReduce;        // Increment to reduce
+    int nSpecialIncReduce; // Special increment to reduce
+    unsigned nLBDFrozenClause;
+};
+
+typedef struct xSAT_Stats_t_ xSAT_Stats_t;
+struct xSAT_Stats_t_
+{
+    unsigned nStarts;
+    unsigned nReduceDB;
+
+    ABC_INT64_T nDecisions;
+    ABC_INT64_T nPropagations;
+    ABC_INT64_T nInspects;
+    ABC_INT64_T nConflicts;
+
+    ABC_INT64_T nClauseLits;
+    ABC_INT64_T nLearntLits;
+};
+
+struct xSAT_Solver_t_
+{
+    /* Clauses Database */
+    xSAT_Mem_t * pMemory;
+    Vec_Int_t  * vLearnts;
+    Vec_Int_t  * vClauses;
+    xSAT_VecWatchList_t * vWatches;
+    xSAT_VecWatchList_t * vBinWatches;
+
+    /* Activity heuristic */
+    int nVarActInc;       /* Amount to bump next variable with. */
+    int nClaActInc;       /* Amount to bump next clause with. */
+
+    /* Variable Information */
+    Vec_Int_t * vActivity;      /* A heuristic measurement of the activity of a variable. */
+    xSAT_Heap_t * hOrder;
+    Vec_Int_t * vLevels;        /* Decision level of the current assignment */
+    Vec_Int_t * vReasons;       /* Reason (clause) of the current assignment */
+    Vec_Str_t * vAssigns;       /* Current assignment. */
+    Vec_Str_t * vPolarity;
+    Vec_Str_t * vTags;
+
+    /* Assignments */
+    Vec_Int_t * vTrail;
+    Vec_Int_t * vTrailLim; // Separator indices for different decision levels in 'trail'.
+    int iQhead;            // Head of propagation queue (as index into the trail).
+
+    int     nAssignSimplify; /* Number of top-level assignments since last
+                              * execution of 'simplify()'. */
+    int64_t nPropSimplify;   /* Remaining number of propagations that must be
+                              * made before next execution of 'simplify()'. */
+
+    /* Temporary data used by Search method */
+    xSAT_BQueue_t * bqTrail;
+    xSAT_BQueue_t * bqLBD;
+    float nSumLBD;
+    int  nConfBeforeReduce;
+    long nRC1;
+    int  nRC2;
+
+    /* Temporary data used by Analyze */
+    Vec_Int_t * vLearntClause;
+    Vec_Str_t * vSeen;
+    Vec_Int_t * vTagged;
+    Vec_Int_t * vStack;
+    Vec_Int_t * vLastDLevel;
+
+    /* Misc temporary */
+    unsigned nStamp;
+    Vec_Int_t * vStamp;        /* Multipurpose stamp used to calculate LBD and
+                                * clauses minimization with binary resolution */
+
+    xSAT_SolverOptions_t Config;
+    xSAT_Stats_t Stats;
+};
+
+static inline int xSAT_Var2Lit( int Var, int c )
+{
+    return Var + Var + ( c != 0 );
+}
+
+static inline int  xSAT_NegLit( int Lit )
+{
+    return Lit ^ 1;
+}
+
+static inline int  xSAT_Lit2Var( int Lit )
+{
+    return Lit >> 1;
+}
+
+static inline int  xSAT_LitSign( int Lit )
+{
+    return Lit & 1;
+}
+
+static inline int xSAT_SolverDecisionLevel( xSAT_Solver_t * s )
+{
+    return Vec_IntSize( s->vTrailLim );
+}
+
+static inline xSAT_Clause_t * xSAT_SolverReadClause( xSAT_Solver_t * s, uint32_t h )
+{
+    return xSAT_MemClauseHand( s->pMemory, h );
+}
+
+static inline int xSAT_SolverIsClauseSatisfied( xSAT_Solver_t * s, xSAT_Clause_t * pCla )
+{
+    int * lits = &( pCla->pData[0].Lit );
+
+    for ( int i = 0; i < pCla->nSize; i++ )
+        if ( Vec_StrEntry( s->vAssigns, xSAT_Lit2Var( lits[i] ) ) == xSAT_LitSign( ( lits[i] ) ) )
+            return true;
+
+    return false;
+}
+
+static inline void xSAT_SolverPrintClauses( xSAT_Solver_t * s )
+{
+    int i;
+    unsigned CRef;
+
+    Vec_IntForEachEntry( s->vClauses, CRef, i )
+        xSAT_ClausePrint( xSAT_SolverReadClause( s, CRef ) );
+}
+
+static inline void xSAT_SolverPrintState( xSAT_Solver_t * s )
+{
+    printf( "starts        : %10d\n", s->Stats.nStarts );
+    printf( "conflicts     : %10ld\n", s->Stats.nConflicts );
+    printf( "decisions     : %10ld\n", s->Stats.nDecisions );
+    printf( "propagations  : %10ld\n", s->Stats.nPropagations );
+}
+
+
+////////////////////////////////////////////////////////////////////////
+///                     FUNCTION DECLARATIONS                        ///
+////////////////////////////////////////////////////////////////////////
+extern uint32_t xSAT_SolverClaNew( xSAT_Solver_t* s, Vec_Int_t * vLits, int fLearnt );
+extern char    xSAT_SolverSearch( xSAT_Solver_t * s );
+
+extern void xSAT_SolverGarbageCollect( xSAT_Solver_t * s );
+
+extern int xSAT_SolverEnqueue( xSAT_Solver_t* s, int Lit, uint32_t From );
+extern void xSAT_SolverCancelUntil( xSAT_Solver_t* s, int Level);
+extern uint32_t xSAT_SolverPropagate( xSAT_Solver_t* s );
+extern void xSAT_SolverRebuildOrderHeap( xSAT_Solver_t* s );
+
+ABC_NAMESPACE_HEADER_END
+
+#endif
diff --git a/src/sat/xsat/xsatSolverAPI.c b/src/sat/xsat/xsatSolverAPI.c
new file mode 100644
index 00000000..7ee817ee
--- /dev/null
+++ b/src/sat/xsat/xsatSolverAPI.c
@@ -0,0 +1,345 @@
+/**CFile****************************************************************
+
+  FileName    [xsatSolverAPI.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 external API 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 "xsatSolver.h"
+
+ABC_NAMESPACE_IMPL_START
+
+xSAT_SolverOptions_t DefaultConfig =
+{
+    .fVerbose = 1,
+
+    .nConfLimit = 0,
+    .nInsLimit = 0,
+    .nRuntimeLimit = 0,
+
+    .K = 0.8,
+    .R = 1.4,
+    .nFirstBlockRestart = 10000,
+    .nSizeLBDQueue = 50,
+    .nSizeTrailQueue = 5000,
+
+    .nConfFirstReduce = 2000,
+    .nIncReduce = 300,
+    .nSpecialIncReduce = 1000,
+
+    .nLBDFrozenClause = 30
+};
+
+/**Function*************************************************************
+
+  Synopsis    []
+
+  Description []
+
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+xSAT_Solver_t* xSAT_SolverCreate()
+{
+    xSAT_Solver_t * s = (xSAT_Solver_t *) ABC_CALLOC( char, sizeof( xSAT_Solver_t ) );
+    s->Config = DefaultConfig;
+
+    s->pMemory = xSAT_MemAlloc(0);
+    s->vClauses = Vec_IntAlloc(0);
+    s->vLearnts = Vec_IntAlloc(0);
+    s->vWatches = xSAT_VecWatchListAlloc( 0 );
+    s->vBinWatches = xSAT_VecWatchListAlloc( 0 );
+
+    s->vTrailLim = Vec_IntAlloc(0);
+    s->vTrail = Vec_IntAlloc( 0 );
+
+    s->vActivity = Vec_IntAlloc( 0 );
+    s->hOrder = xSAT_HeapAlloc( s->vActivity );
+
+    s->vPolarity = Vec_StrAlloc( 0 );
+    s->vTags = Vec_StrAlloc( 0 );
+    s->vAssigns = Vec_StrAlloc( 0 );
+    s->vLevels = Vec_IntAlloc( 0 );
+    s->vReasons = Vec_IntAlloc( 0 );
+    s->vStamp = Vec_IntAlloc( 0 );
+
+    s->vTagged = Vec_IntAlloc(0);
+    s->vStack  = Vec_IntAlloc(0);
+
+    s->vSeen = Vec_StrAlloc( 0 );
+    s->vLearntClause = Vec_IntAlloc(0);
+    s->vLastDLevel = Vec_IntAlloc(0);
+
+
+    s->bqTrail = xSAT_BQueueNew( s->Config.nSizeTrailQueue );
+    s->bqLBD = xSAT_BQueueNew( s->Config.nSizeLBDQueue );
+
+    s->nVarActInc = (1 <<  5);
+    s->nClaActInc = (1 << 11);
+
+    s->nConfBeforeReduce = s->Config.nConfFirstReduce;
+    s->nRC1 = 1;
+    s->nRC2 = s->Config.nConfFirstReduce;
+    return s;
+}
+
+/**Function*************************************************************
+
+  Synopsis    []
+
+  Description []
+
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+void xSAT_SolverDestroy( xSAT_Solver_t * s )
+{
+    xSAT_MemFree( s->pMemory );
+    Vec_IntFree( s->vClauses );
+    Vec_IntFree( s->vLearnts );
+    xSAT_VecWatchListFree( s->vWatches );
+    xSAT_VecWatchListFree( s->vBinWatches );
+
+    // delete vectors
+    xSAT_HeapFree(s->hOrder);
+    Vec_IntFree( s->vTrailLim );
+    Vec_IntFree( s->vTrail );
+    Vec_IntFree( s->vTagged );
+    Vec_IntFree( s->vStack );
+
+    Vec_StrFree( s->vSeen );
+    Vec_IntFree( s->vLearntClause );
+    Vec_IntFree( s->vLastDLevel );
+
+    Vec_IntFree( s->vActivity );
+    Vec_StrFree( s->vPolarity );
+    Vec_StrFree( s->vTags );
+    Vec_StrFree( s->vAssigns );
+    Vec_IntFree( s->vLevels );
+    Vec_IntFree( s->vReasons );
+
+    xSAT_BQueueFree(s->bqLBD);
+    xSAT_BQueueFree(s->bqTrail);
+
+    ABC_FREE(s);
+}
+
+/**Function*************************************************************
+
+  Synopsis    []
+
+  Description []
+
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+int xSAT_SolverSimplify( xSAT_Solver_t * s )
+{
+    int i, j;
+    uint32_t CRef;
+    assert( xSAT_SolverDecisionLevel(s) == 0 );
+
+    if ( xSAT_SolverPropagate(s) != CRefUndef )
+        return false;
+
+    if ( s->nAssignSimplify == Vec_IntSize( s->vTrail ) || s->nPropSimplify > 0 )
+        return true;
+
+    j = 0;
+    Vec_IntForEachEntry( s->vClauses, CRef, i )
+    {
+        xSAT_Clause_t * pCla = xSAT_SolverReadClause( s, CRef );
+        if ( xSAT_SolverIsClauseSatisfied( s, pCla ) )
+        {
+            pCla->fMark = 1;
+            s->Stats.nClauseLits -= pCla->nSize;
+
+            if ( pCla->nSize == 2 )
+            {
+                xSAT_WatchListRemove( xSAT_VecWatchListEntry( s->vBinWatches, xSAT_NegLit(pCla->pData[0].Lit) ), CRef );
+                xSAT_WatchListRemove( xSAT_VecWatchListEntry( s->vBinWatches, xSAT_NegLit(pCla->pData[1].Lit) ), CRef );
+            }
+            else
+            {
+                xSAT_WatchListRemove( xSAT_VecWatchListEntry( s->vWatches, xSAT_NegLit(pCla->pData[0].Lit) ), CRef );
+                xSAT_WatchListRemove( xSAT_VecWatchListEntry( s->vWatches, xSAT_NegLit(pCla->pData[1].Lit) ), CRef );
+            }
+        }
+        else
+            Vec_IntWriteEntry( s->vClauses, j++, CRef );
+    }
+    Vec_IntShrink( s->vClauses, j );
+    xSAT_SolverRebuildOrderHeap( s );
+
+    s->nAssignSimplify = Vec_IntSize( s->vTrail );
+    s->nPropSimplify = s->Stats.nClauseLits + s->Stats.nLearntLits;
+
+    return true;
+}
+
+/**Function*************************************************************
+
+  Synopsis    []
+
+  Description []
+
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+void xSAT_SolverAddVariable( xSAT_Solver_t* s, int Sign )
+{
+    int Var = Vec_IntSize( s->vActivity );
+
+    xSAT_VecWatchListPush( s->vWatches );
+    xSAT_VecWatchListPush( s->vWatches );
+    xSAT_VecWatchListPush( s->vBinWatches );
+    xSAT_VecWatchListPush( s->vBinWatches );
+
+    Vec_IntPush( s->vActivity, 0 );
+    Vec_IntPush( s->vLevels, 0 );
+    Vec_StrPush( s->vAssigns, VarX );
+    Vec_StrPush( s->vPolarity, 1 );
+    Vec_StrPush( s->vTags, 0 );
+    Vec_IntPush( s->vReasons, ( int ) CRefUndef );
+    Vec_IntPush( s->vStamp, 0 );
+    Vec_StrPush( s->vSeen, 0 );
+
+    xSAT_HeapInsert( s->hOrder, Var );
+}
+
+/**Function*************************************************************
+
+  Synopsis    []
+
+  Description []
+
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+int xSAT_SolverAddClause( xSAT_Solver_t * s, Vec_Int_t * vLits )
+{
+    int i, j;
+    int Lit, PrevLit;
+    int MaxVar;
+
+    Vec_IntSort( vLits, 0 );
+    MaxVar = xSAT_Lit2Var( Vec_IntEntryLast( vLits ) );
+    while ( MaxVar >= Vec_IntSize( s->vActivity ) )
+        xSAT_SolverAddVariable( s, 1 );
+
+    j = 0;
+    PrevLit = LitUndef;
+    Vec_IntForEachEntry( vLits, Lit, i )
+    {
+        if ( Lit == xSAT_NegLit( PrevLit ) || Vec_StrEntry( s->vAssigns, xSAT_Lit2Var( Lit ) ) == xSAT_LitSign( Lit ) )
+            return true;
+        else if ( Lit != PrevLit && Vec_StrEntry( s->vAssigns, xSAT_Lit2Var( Lit ) ) == VarX )
+        {
+            PrevLit = Lit;
+            Vec_IntWriteEntry( vLits, j++, Lit );
+        }
+    }
+    Vec_IntShrink( vLits, j );
+
+    if ( Vec_IntSize( vLits ) == 0 )
+        return false;
+    if ( Vec_IntSize( vLits ) == 1 )
+    {
+        xSAT_SolverEnqueue( s, Vec_IntEntry( vLits, 0 ), CRefUndef );
+        return ( xSAT_SolverPropagate( s ) == CRefUndef );
+    }
+
+    xSAT_SolverClaNew( s, vLits, 0 );
+    return true;
+}
+
+/**Function*************************************************************
+
+  Synopsis    []
+
+  Description []
+
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+int xSAT_SolverSolve( xSAT_Solver_t* s )
+{
+    char status = LBoolUndef;
+
+    assert(s);
+    if ( s->Config.fVerbose )
+    {
+        printf( "==========================================[ BLACK MAGIC ]================================================\n" );
+        printf( "|                                |                                |                                     |\n" );
+        printf( "| - Restarts:                    | - Reduce Clause DB:            | - Minimize Asserting:               |\n" );
+        printf( "|   * LBD Queue    : %6d      |   * First     : %6d         |    * size < %3d                     |\n",       s->Config.nSizeLBDQueue, s->Config.nConfFirstReduce, 0 );
+        printf( "|   * Trail Queue  : %6d      |   * Inc       : %6d         |    * lbd  < %3d                     |\n",       s->Config.nSizeTrailQueue, s->Config.nIncReduce, 0 );
+        printf( "|   * K            : %6.2f      |   * Special   : %6d         |                                     |\n",     s->Config.K, s->Config.nSpecialIncReduce );
+        printf( "|   * R            : %6.2f      |   * Protected :  (lbd)< %2d     |                                     |\n", s->Config.R, s->Config.nLBDFrozenClause );
+        printf( "|                                |                                |                                     |\n" );
+        printf( "=========================================================================================================\n" );
+    }
+
+    while ( status == LBoolUndef )
+        status = xSAT_SolverSearch( s );
+
+    if ( s->Config.fVerbose )
+        printf( "=========================================================================================================\n" );
+
+    xSAT_SolverCancelUntil( s, 0 );
+    return status;
+}
+
+/**Function*************************************************************
+
+  Synopsis    []
+
+  Description []
+
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+void xSAT_SolverPrintStats( xSAT_Solver_t * s )
+{
+    printf( "starts        : %10d\n", s->Stats.nStarts );
+    printf( "conflicts     : %10ld\n", s->Stats.nConflicts );
+    printf( "decisions     : %10ld\n", s->Stats.nDecisions );
+    printf( "propagations  : %10ld\n", s->Stats.nPropagations );
+}
+
+ABC_NAMESPACE_IMPL_END
diff --git a/src/sat/xsat/xsatUtils.h b/src/sat/xsat/xsatUtils.h
new file mode 100644
index 00000000..7f774d85
--- /dev/null
+++ b/src/sat/xsat/xsatUtils.h
@@ -0,0 +1,106 @@
+/**CFile****************************************************************
+
+  FileName    [xsatUtils.h]
+
+  SystemName  [ABC: Logic synthesis and verification system.]
+
+  PackageName [xSAT - A SAT solver written in C.
+               Read the license file for more info.]
+
+  Synopsis    [Utility functions used in xSAT]
+
+  Author      [Bruno Schmitt <boschmitt@inf.ufrgs.br>]
+
+  Affiliation [UC Berkeley / UFRGS]
+
+  Date        [Ver. 1.0. Started - November 10, 2016.]
+
+  Revision    []
+
+***********************************************************************/
+#ifndef ABC__sat__xSAT__xsatUtils_h
+#define ABC__sat__xSAT__xsatUtils_h
+
+////////////////////////////////////////////////////////////////////////
+///                          INCLUDES                                ///
+////////////////////////////////////////////////////////////////////////
+#include "misc/util/abc_global.h"
+
+ABC_NAMESPACE_HEADER_START
+
+/**Function*************************************************************
+
+  Synopsis    []
+
+  Description []
+
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+static inline void xSAT_UtilSelectSort( void** pArray, int nSize, int(* CompFnct )( const void *, const void * ) )
+{
+    int i, j, iBest;
+    void* pTmp;
+
+    for ( i = 0; i < ( nSize - 1 ); i++ )
+    {
+        iBest = i;
+        for ( j = i + 1; j < nSize; j++ )
+        {
+            if ( CompFnct( pArray[j], pArray[iBest] ) )
+                iBest = j;
+        }
+        pTmp = pArray[i];
+        pArray[i] = pArray[iBest];
+        pArray[iBest] = pTmp;
+    }
+}
+
+/**Function*************************************************************
+
+  Synopsis    []
+
+  Description []
+
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+static void xSAT_UtilSort( void** pArray, int nSize, int(* CompFnct )( const void *, const void *) )
+{
+    if ( nSize <= 15 )
+        xSAT_UtilSelectSort( pArray, nSize, CompFnct );
+    else
+    {
+        void* pPivot = pArray[nSize / 2];
+        void* pTmp;
+        int i = -1;
+        int j = nSize;
+
+        for(;;)
+        {
+            do i++; while( CompFnct( pArray[i], pPivot ) );
+            do j--; while( CompFnct( pPivot, pArray[j] ) );
+
+            if ( i >= j )
+                break;
+
+            pTmp = pArray[i];
+            pArray[i] = pArray[j];
+            pArray[j] = pTmp;
+        }
+
+        xSAT_UtilSort( pArray, i, CompFnct );
+        xSAT_UtilSort( pArray + i, ( nSize - i ), CompFnct );
+    }
+}
+
+ABC_NAMESPACE_HEADER_END
+
+#endif
+////////////////////////////////////////////////////////////////////////
+///                       END OF FILE                                ///
+////////////////////////////////////////////////////////////////////////
diff --git a/src/sat/xsat/xsatWatchList.h b/src/sat/xsat/xsatWatchList.h
new file mode 100644
index 00000000..454cfe44
--- /dev/null
+++ b/src/sat/xsat/xsatWatchList.h
@@ -0,0 +1,268 @@
+/**CFile****************************************************************
+
+  FileName    [xsatWatchList.h]
+
+  SystemName  [ABC: Logic synthesis and verification system.]
+
+  PackageName [xSAT - A SAT solver written in C.
+               Read the license file for more info.]
+
+  Synopsis    [Watch list and its related structures implementation]
+
+  Author      [Bruno Schmitt <boschmitt@inf.ufrgs.br>]
+
+  Affiliation [UC Berkeley / UFRGS]
+
+  Date        [Ver. 1.0. Started - November 10, 2016.]
+
+  Revision    []
+
+***********************************************************************/
+#ifndef ABC__sat__xSAT__xsatWatchList_h
+#define ABC__sat__xSAT__xsatWatchList_h
+
+////////////////////////////////////////////////////////////////////////
+///                          INCLUDES                                ///
+////////////////////////////////////////////////////////////////////////
+#include "misc/util/abc_global.h"
+
+ABC_NAMESPACE_HEADER_START
+
+////////////////////////////////////////////////////////////////////////
+///                    STRUCTURE DEFINITIONS                         ///
+////////////////////////////////////////////////////////////////////////
+typedef struct xSAT_Watcher_t_ xSAT_Watcher_t;
+struct xSAT_Watcher_t_
+{
+    uint32_t CRef;
+    int Blocker;
+};
+
+typedef struct xSAT_WatchList_t_ xSAT_WatchList_t;
+struct xSAT_WatchList_t_
+{
+    int nCap;
+    int nSize;
+    xSAT_Watcher_t * pArray;
+};
+
+typedef struct xSAT_VecWatchList_t_ xSAT_VecWatchList_t;
+struct xSAT_VecWatchList_t_
+{
+    int nCap;
+    int nSize;
+    xSAT_WatchList_t * pArray;
+};
+
+/**Function*************************************************************
+
+  Synopsis    []
+
+  Description []
+
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+static inline void xSAT_WatchListFree( xSAT_WatchList_t * v )
+{
+    if ( v->pArray )
+        ABC_FREE( v->pArray );
+}
+
+/**Function*************************************************************
+
+  Synopsis    []
+
+  Description []
+
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+static inline int  xSAT_WatchListSize( xSAT_WatchList_t * v )
+{
+    return v->nSize;
+}
+
+/**Function*************************************************************
+
+  Synopsis    []
+
+  Description []
+
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+static inline void xSAT_WatchListShrink( xSAT_WatchList_t * v, int k )
+{
+    assert(k <= v->nSize);
+    v->nSize = k;
+}
+
+/**Function*************************************************************
+
+  Synopsis    []
+
+  Description []
+
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+static inline void xSAT_WatchListPush( xSAT_WatchList_t * v, xSAT_Watcher_t e )
+{
+    assert( v );
+    if (v->nSize == v->nCap)
+    {
+        int newsize = (v->nCap < 4) ? 4 : (v->nCap / 2) * 3;
+
+        v->pArray = ABC_REALLOC( xSAT_Watcher_t, v->pArray, newsize );
+        if ( v->pArray == NULL )
+        {
+            printf( "Failed to realloc memory from %.1f MB to %.1f MB.\n",
+                1.0 * v->nCap / (1<<20), 1.0 * newsize / (1<<20) );
+            fflush( stdout );
+        }
+        v->nCap = newsize;
+    }
+
+    v->pArray[v->nSize++] = e;
+}
+
+/**Function*************************************************************
+
+  Synopsis    []
+
+  Description []
+
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+static inline xSAT_Watcher_t* xSAT_WatchListArray( xSAT_WatchList_t * v )
+{
+    return v->pArray;
+}
+
+/**Function*************************************************************
+
+  Synopsis    []
+
+  Description []
+
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+static inline void xSAT_WatchListRemove( xSAT_WatchList_t * v, uint32_t CRef )
+{
+    xSAT_Watcher_t* ws = xSAT_WatchListArray(v);
+    int j = 0;
+
+    for (; ws[j].CRef != CRef; j++);
+    assert(j < xSAT_WatchListSize(v));
+    memmove(v->pArray + j, v->pArray + j + 1, (v->nSize - j - 1) * sizeof(xSAT_Watcher_t));
+    v->nSize -= 1;
+}
+
+/**Function*************************************************************
+
+  Synopsis    []
+
+  Description []
+
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+static inline xSAT_VecWatchList_t * xSAT_VecWatchListAlloc( int nCap )
+{
+    xSAT_VecWatchList_t * v = ABC_ALLOC( xSAT_VecWatchList_t, 1 );
+
+    v->nCap   = 4;
+    v->nSize  = 0;
+    v->pArray = (xSAT_WatchList_t *) ABC_CALLOC(xSAT_WatchList_t, sizeof( xSAT_WatchList_t ) * v->nCap);
+    return v;
+}
+
+/**Function*************************************************************
+
+  Synopsis    []
+
+  Description []
+
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+static inline void xSAT_VecWatchListFree( xSAT_VecWatchList_t* v )
+{
+    for( int i = 0; i < v->nSize; i++ )
+        xSAT_WatchListFree( v->pArray + i );
+
+    ABC_FREE( v->pArray );
+    ABC_FREE( v );
+}
+
+/**Function*************************************************************
+
+  Synopsis    []
+
+  Description []
+
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+static inline void xSAT_VecWatchListPush( xSAT_VecWatchList_t* v )
+{
+    if ( v->nSize == v->nCap )
+    {
+        int newsize = (v->nCap < 4) ? v->nCap * 2 : (v->nCap / 2) * 3;
+
+        v->pArray = ABC_REALLOC( xSAT_WatchList_t, v->pArray, newsize );
+        memset( v->pArray + v->nCap, 0, sizeof(xSAT_WatchList_t) * (newsize - v->nCap) );
+        if ( v->pArray == NULL )
+        {
+            printf( "Failed to realloc memory from %.1f MB to %.1f MB.\n",
+                1.0 * v->nCap / (1<<20), 1.0 * newsize / (1<<20) );
+            fflush( stdout );
+        }
+        v->nCap = newsize;
+    }
+
+    v->nSize++;
+}
+
+/**Function*************************************************************
+
+  Synopsis    []
+
+  Description []
+
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+static inline xSAT_WatchList_t * xSAT_VecWatchListEntry( xSAT_VecWatchList_t* v, int iEntry )
+{
+    assert( iEntry < v->nCap );
+    assert( iEntry < v->nSize );
+    return v->pArray + iEntry;
+}
+
+ABC_NAMESPACE_HEADER_END
+
+#endif