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

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

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

1 files changed, 247 insertions, 0 deletions

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