From 5351ab4b13aa46db5710ca3ffe659e8e691ba126 Mon Sep 17 00:00:00 2001 From: Bruno Schmitt Date: Mon, 12 Dec 2016 16:20:38 -0200 Subject: =?UTF-8?q?xSAT=20is=20an=20experimental=20SAT=20Solver=20based=20?= =?UTF-8?q?on=20Glucose=20v3(see=20Glucose=20copyrights=20below)=20and=20A?= =?UTF-8?q?BC=20C=20version=20of=20MiniSat=20(bsat)=20developed=20by=20Nik?= =?UTF-8?q?las=20Sorensson=20and=20modified=20by=20Alan=20Mishchenko.=20It?= =?UTF-8?q?=E2=80=99s=20development=20has=20reached=20sufficient=20maturit?= =?UTF-8?q?y=20to=20be=20committed=20in=20ABC,=20but=20still=20in=20a=20be?= =?UTF-8?q?ta=20state.?= MIME-Version: 1.0 Content-Type: text/plain; charset=UTF-8 Content-Transfer-Encoding: 8bit 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. --- src/sat/xsat/xsatSolver.h | 247 ++++++++++++++++++++++++++++++++++++++++++++++ 1 file changed, 247 insertions(+) create mode 100644 src/sat/xsat/xsatSolver.h (limited to 'src/sat/xsat/xsatSolver.h') 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 ] + + 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 +#include +#include +#include + +#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 -- cgit v1.2.3