1 /**CFile**************************************************************** 2 3 FileName [msatInt.c] 4 5 PackageName [A C version of SAT solver MINISAT, originally developed 6 in C++ by Niklas Een and Niklas Sorensson, Chalmers University of 7 Technology, Sweden: http://www.cs.chalmers.se/~een/Satzoo.] 8 9 Synopsis [Internal definitions of the solver.] 10 11 Author [Alan Mishchenko <alanmi@eecs.berkeley.edu>] 12 13 Affiliation [UC Berkeley] 14 15 Date [Ver. 1.0. Started - January 1, 2004.] 16 17 Revision [$Id: msatInt.c,v 1.0 2004/01/01 1:00:00 alanmi Exp $] 18 19 ***********************************************************************/ 20 21 #ifndef ABC__sat__msat__msatInt_h 22 #define ABC__sat__msat__msatInt_h 23 24 25 //////////////////////////////////////////////////////////////////////// 26 /// INCLUDES /// 27 //////////////////////////////////////////////////////////////////////// 28 29 #include <stdio.h> 30 #include <stdlib.h> 31 #include <string.h> 32 #include <assert.h> 33 #include <math.h> 34 35 #include "misc/util/abc_global.h" 36 #include "msat.h" 37 38 ABC_NAMESPACE_HEADER_START 39 40 41 //////////////////////////////////////////////////////////////////////// 42 /// PARAMETERS /// 43 //////////////////////////////////////////////////////////////////////// 44 45 //////////////////////////////////////////////////////////////////////// 46 /// STRUCTURE DEFINITIONS /// 47 //////////////////////////////////////////////////////////////////////// 48 49 // By default, custom memory management is used 50 // which guarantees constant time allocation/deallocation 51 // for SAT clauses and other frequently modified objects. 52 // For debugging, it is possible use system memory management 53 // directly. In which case, uncomment the macro below. 54 //#define USE_SYSTEM_MEMORY_MANAGEMENT 55 56 // internal data structures 57 typedef struct Msat_Clause_t_ Msat_Clause_t; 58 typedef struct Msat_Queue_t_ Msat_Queue_t; 59 typedef struct Msat_Order_t_ Msat_Order_t; 60 // memory managers (duplicated from Extra for stand-aloneness) 61 typedef struct Msat_MmFixed_t_ Msat_MmFixed_t; 62 typedef struct Msat_MmFlex_t_ Msat_MmFlex_t; 63 typedef struct Msat_MmStep_t_ Msat_MmStep_t; 64 // variables and literals 65 typedef int Msat_Lit_t; 66 typedef int Msat_Var_t; 67 // the type of return value 68 #define MSAT_VAR_UNASSIGNED (-1) 69 #define MSAT_LIT_UNASSIGNED (-2) 70 #define MSAT_ORDER_UNKNOWN (-3) 71 72 // printing the search tree 73 #define L_IND "%-*d" 74 #define L_ind Msat_SolverReadDecisionLevel(p)*3+3,Msat_SolverReadDecisionLevel(p) 75 #define L_LIT "%s%d" 76 #define L_lit(Lit) MSAT_LITSIGN(Lit)?"-":"", MSAT_LIT2VAR(Lit)+1 77 78 typedef struct Msat_SolverStats_t_ Msat_SolverStats_t; 79 struct Msat_SolverStats_t_ 80 { 81 ABC_INT64_T nStarts; // the number of restarts 82 ABC_INT64_T nDecisions; // the number of decisions 83 ABC_INT64_T nPropagations; // the number of implications 84 ABC_INT64_T nInspects; // the number of times clauses are vising while watching them 85 ABC_INT64_T nConflicts; // the number of conflicts 86 ABC_INT64_T nSuccesses; // the number of sat assignments found 87 }; 88 89 typedef struct Msat_SearchParams_t_ Msat_SearchParams_t; 90 struct Msat_SearchParams_t_ 91 { 92 double dVarDecay; 93 double dClaDecay; 94 }; 95 96 // sat solver data structure visible through all the internal files 97 struct Msat_Solver_t_ 98 { 99 int nClauses; // the total number of clauses 100 int nClausesStart; // the number of clauses before adding 101 Msat_ClauseVec_t * vClauses; // problem clauses 102 Msat_ClauseVec_t * vLearned; // learned clauses 103 double dClaInc; // Amount to bump next clause with. 104 double dClaDecay; // INVERSE decay factor for clause activity: stores 1/decay. 105 106 double * pdActivity; // A heuristic measurement of the activity of a variable. 107 float * pFactors; // the multiplicative factors of variable activity 108 double dVarInc; // Amount to bump next variable with. 109 double dVarDecay; // INVERSE decay factor for variable activity: stores 1/decay. Use negative value for static variable order. 110 Msat_Order_t * pOrder; // Keeps track of the decision variable order. 111 112 Msat_ClauseVec_t ** pvWatched; // 'pvWatched[lit]' is a list of constraints watching 'lit' (will go there if literal becomes true). 113 Msat_Queue_t * pQueue; // Propagation queue. 114 115 int nVars; // the current number of variables 116 int nVarsAlloc; // the maximum allowed number of variables 117 int * pAssigns; // The current assignments (literals or MSAT_VAR_UNKOWN) 118 int * pModel; // The satisfying assignment 119 Msat_IntVec_t * vTrail; // List of assignments made. 120 Msat_IntVec_t * vTrailLim; // Separator indices for different decision levels in 'trail'. 121 Msat_Clause_t ** pReasons; // 'reason[var]' is the clause that implied the variables current value, or 'NULL' if none. 122 int * pLevel; // 'level[var]' is the decision level at which assignment was made. 123 int nLevelRoot; // Level of first proper decision. 124 125 double dRandSeed; // For the internal random number generator (makes solver deterministic over different platforms). 126 127 int fVerbose; // the verbosity flag 128 double dProgress; // Set by 'search()'. 129 130 // the variable cone and variable connectivity 131 Msat_IntVec_t * vConeVars; 132 Msat_IntVec_t * vVarsUsed; 133 Msat_ClauseVec_t * vAdjacents; 134 135 // internal data used during conflict analysis 136 int * pSeen; // time when a lit was seen for the last time 137 int nSeenId; // the id of current seeing 138 Msat_IntVec_t * vReason; // the temporary array of literals 139 Msat_IntVec_t * vTemp; // the temporary array of literals 140 int * pFreq; // the number of times each var participated in conflicts 141 142 // the memory manager 143 Msat_MmStep_t * pMem; 144 145 // statistics 146 Msat_SolverStats_t Stats; 147 int nTwoLits; 148 int nTwoLitsL; 149 int nClausesInit; 150 int nClausesAlloc; 151 int nClausesAllocL; 152 int nBackTracks; 153 }; 154 155 struct Msat_ClauseVec_t_ 156 { 157 Msat_Clause_t ** pArray; 158 int nSize; 159 int nCap; 160 }; 161 162 struct Msat_IntVec_t_ 163 { 164 int * pArray; 165 int nSize; 166 int nCap; 167 }; 168 169 //////////////////////////////////////////////////////////////////////// 170 /// GLOBAL VARIABLES /// 171 //////////////////////////////////////////////////////////////////////// 172 173 //////////////////////////////////////////////////////////////////////// 174 /// MACRO DEFINITIONS /// 175 //////////////////////////////////////////////////////////////////////// 176 177 //////////////////////////////////////////////////////////////////////// 178 /// FUNCTION DECLARATIONS /// 179 //////////////////////////////////////////////////////////////////////// 180 181 /*=== satActivity.c ===========================================================*/ 182 extern void Msat_SolverVarDecayActivity( Msat_Solver_t * p ); 183 extern void Msat_SolverVarRescaleActivity( Msat_Solver_t * p ); 184 extern void Msat_SolverClaDecayActivity( Msat_Solver_t * p ); 185 extern void Msat_SolverClaRescaleActivity( Msat_Solver_t * p ); 186 /*=== satSolverApi.c ===========================================================*/ 187 extern Msat_Clause_t * Msat_SolverReadClause( Msat_Solver_t * p, int Num ); 188 /*=== satSolver.c ===========================================================*/ 189 extern int Msat_SolverReadDecisionLevel( Msat_Solver_t * p ); 190 extern int * Msat_SolverReadDecisionLevelArray( Msat_Solver_t * p ); 191 extern Msat_Clause_t ** Msat_SolverReadReasonArray( Msat_Solver_t * p ); 192 extern Msat_Type_t Msat_SolverReadVarValue( Msat_Solver_t * p, Msat_Var_t Var ); 193 extern Msat_ClauseVec_t * Msat_SolverReadLearned( Msat_Solver_t * p ); 194 extern Msat_ClauseVec_t ** Msat_SolverReadWatchedArray( Msat_Solver_t * p ); 195 extern int * Msat_SolverReadSeenArray( Msat_Solver_t * p ); 196 extern int Msat_SolverIncrementSeenId( Msat_Solver_t * p ); 197 extern Msat_MmStep_t * Msat_SolverReadMem( Msat_Solver_t * p ); 198 extern void Msat_SolverClausesIncrement( Msat_Solver_t * p ); 199 extern void Msat_SolverClausesDecrement( Msat_Solver_t * p ); 200 extern void Msat_SolverClausesIncrementL( Msat_Solver_t * p ); 201 extern void Msat_SolverClausesDecrementL( Msat_Solver_t * p ); 202 extern void Msat_SolverVarBumpActivity( Msat_Solver_t * p, Msat_Lit_t Lit ); 203 extern void Msat_SolverClaBumpActivity( Msat_Solver_t * p, Msat_Clause_t * pC ); 204 extern int Msat_SolverEnqueue( Msat_Solver_t * p, Msat_Lit_t Lit, Msat_Clause_t * pC ); 205 extern double Msat_SolverProgressEstimate( Msat_Solver_t * p ); 206 /*=== satSolverSearch.c ===========================================================*/ 207 extern int Msat_SolverAssume( Msat_Solver_t * p, Msat_Lit_t Lit ); 208 extern Msat_Clause_t * Msat_SolverPropagate( Msat_Solver_t * p ); 209 extern void Msat_SolverCancelUntil( Msat_Solver_t * p, int Level ); 210 extern Msat_Type_t Msat_SolverSearch( Msat_Solver_t * p, int nConfLimit, int nLearnedLimit, int nBackTrackLimit, Msat_SearchParams_t * pPars ); 211 /*=== satQueue.c ===========================================================*/ 212 extern Msat_Queue_t * Msat_QueueAlloc( int nVars ); 213 extern void Msat_QueueFree( Msat_Queue_t * p ); 214 extern int Msat_QueueReadSize( Msat_Queue_t * p ); 215 extern void Msat_QueueInsert( Msat_Queue_t * p, int Lit ); 216 extern int Msat_QueueExtract( Msat_Queue_t * p ); 217 extern void Msat_QueueClear( Msat_Queue_t * p ); 218 /*=== satOrder.c ===========================================================*/ 219 extern Msat_Order_t * Msat_OrderAlloc( Msat_Solver_t * pSat ); 220 extern void Msat_OrderSetBounds( Msat_Order_t * p, int nVarsMax ); 221 extern void Msat_OrderClean( Msat_Order_t * p, Msat_IntVec_t * vCone ); 222 extern int Msat_OrderCheck( Msat_Order_t * p ); 223 extern void Msat_OrderFree( Msat_Order_t * p ); 224 extern int Msat_OrderVarSelect( Msat_Order_t * p ); 225 extern void Msat_OrderVarAssigned( Msat_Order_t * p, int Var ); 226 extern void Msat_OrderVarUnassigned( Msat_Order_t * p, int Var ); 227 extern void Msat_OrderUpdate( Msat_Order_t * p, int Var ); 228 /*=== satClause.c ===========================================================*/ 229 extern int Msat_ClauseCreate( Msat_Solver_t * p, Msat_IntVec_t * vLits, int fLearnt, Msat_Clause_t ** pClause_out ); 230 extern Msat_Clause_t * Msat_ClauseCreateFake( Msat_Solver_t * p, Msat_IntVec_t * vLits ); 231 extern Msat_Clause_t * Msat_ClauseCreateFakeLit( Msat_Solver_t * p, Msat_Lit_t Lit ); 232 extern int Msat_ClauseReadLearned( Msat_Clause_t * pC ); 233 extern int Msat_ClauseReadSize( Msat_Clause_t * pC ); 234 extern int * Msat_ClauseReadLits( Msat_Clause_t * pC ); 235 extern int Msat_ClauseReadMark( Msat_Clause_t * pC ); 236 extern void Msat_ClauseSetMark( Msat_Clause_t * pC, int fMark ); 237 extern int Msat_ClauseReadNum( Msat_Clause_t * pC ); 238 extern void Msat_ClauseSetNum( Msat_Clause_t * pC, int Num ); 239 extern int Msat_ClauseReadTypeA( Msat_Clause_t * pC ); 240 extern void Msat_ClauseSetTypeA( Msat_Clause_t * pC, int fTypeA ); 241 extern int Msat_ClauseIsLocked( Msat_Solver_t * p, Msat_Clause_t * pC ); 242 extern float Msat_ClauseReadActivity( Msat_Clause_t * pC ); 243 extern void Msat_ClauseWriteActivity( Msat_Clause_t * pC, float Num ); 244 extern void Msat_ClauseFree( Msat_Solver_t * p, Msat_Clause_t * pC, int fRemoveWatched ); 245 extern int Msat_ClausePropagate( Msat_Clause_t * pC, Msat_Lit_t Lit, int * pAssigns, Msat_Lit_t * pLit_out ); 246 extern int Msat_ClauseSimplify( Msat_Clause_t * pC, int * pAssigns ); 247 extern void Msat_ClauseCalcReason( Msat_Solver_t * p, Msat_Clause_t * pC, Msat_Lit_t Lit, Msat_IntVec_t * vLits_out ); 248 extern void Msat_ClauseRemoveWatch( Msat_ClauseVec_t * vClauses, Msat_Clause_t * pC ); 249 extern void Msat_ClausePrint( Msat_Clause_t * pC ); 250 extern void Msat_ClausePrintSymbols( Msat_Clause_t * pC ); 251 extern void Msat_ClauseWriteDimacs( FILE * pFile, Msat_Clause_t * pC, int fIncrement ); 252 extern unsigned Msat_ClauseComputeTruth( Msat_Solver_t * p, Msat_Clause_t * pC ); 253 /*=== satSort.c ===========================================================*/ 254 extern void Msat_SolverSortDB( Msat_Solver_t * p ); 255 /*=== satClauseVec.c ===========================================================*/ 256 extern Msat_ClauseVec_t * Msat_ClauseVecAlloc( int nCap ); 257 extern void Msat_ClauseVecFree( Msat_ClauseVec_t * p ); 258 extern Msat_Clause_t ** Msat_ClauseVecReadArray( Msat_ClauseVec_t * p ); 259 extern int Msat_ClauseVecReadSize( Msat_ClauseVec_t * p ); 260 extern void Msat_ClauseVecGrow( Msat_ClauseVec_t * p, int nCapMin ); 261 extern void Msat_ClauseVecShrink( Msat_ClauseVec_t * p, int nSizeNew ); 262 extern void Msat_ClauseVecClear( Msat_ClauseVec_t * p ); 263 extern void Msat_ClauseVecPush( Msat_ClauseVec_t * p, Msat_Clause_t * Entry ); 264 extern Msat_Clause_t * Msat_ClauseVecPop( Msat_ClauseVec_t * p ); 265 extern void Msat_ClauseVecWriteEntry( Msat_ClauseVec_t * p, int i, Msat_Clause_t * Entry ); 266 extern Msat_Clause_t * Msat_ClauseVecReadEntry( Msat_ClauseVec_t * p, int i ); 267 268 /*=== satMem.c ===========================================================*/ 269 // fixed-size-block memory manager 270 extern Msat_MmFixed_t * Msat_MmFixedStart( int nEntrySize ); 271 extern void Msat_MmFixedStop( Msat_MmFixed_t * p, int fVerbose ); 272 extern char * Msat_MmFixedEntryFetch( Msat_MmFixed_t * p ); 273 extern void Msat_MmFixedEntryRecycle( Msat_MmFixed_t * p, char * pEntry ); 274 extern void Msat_MmFixedRestart( Msat_MmFixed_t * p ); 275 extern int Msat_MmFixedReadMemUsage( Msat_MmFixed_t * p ); 276 // flexible-size-block memory manager 277 extern Msat_MmFlex_t * Msat_MmFlexStart(); 278 extern void Msat_MmFlexStop( Msat_MmFlex_t * p, int fVerbose ); 279 extern char * Msat_MmFlexEntryFetch( Msat_MmFlex_t * p, int nBytes ); 280 extern int Msat_MmFlexReadMemUsage( Msat_MmFlex_t * p ); 281 // hierarchical memory manager 282 extern Msat_MmStep_t * Msat_MmStepStart( int nSteps ); 283 extern void Msat_MmStepStop( Msat_MmStep_t * p, int fVerbose ); 284 extern char * Msat_MmStepEntryFetch( Msat_MmStep_t * p, int nBytes ); 285 extern void Msat_MmStepEntryRecycle( Msat_MmStep_t * p, char * pEntry, int nBytes ); 286 extern int Msat_MmStepReadMemUsage( Msat_MmStep_t * p ); 287 288 //////////////////////////////////////////////////////////////////////// 289 /// END OF FILE /// 290 //////////////////////////////////////////////////////////////////////// 291 292 293 ABC_NAMESPACE_HEADER_END 294 295 #endif 296