1 /**CFile****************************************************************
2
3 FileName [xsatSolver.h]
4
5 SystemName [ABC: Logic synthesis and verification system.]
6
7 PackageName [xSAT - A SAT solver written in C.
8 Read the license file for more info.]
9
10 Synopsis [Internal definitions of the solver.]
11
12 Author [Bruno Schmitt <boschmitt@inf.ufrgs.br>]
13
14 Affiliation [UC Berkeley / UFRGS]
15
16 Date [Ver. 1.0. Started - November 10, 2016.]
17
18 Revision []
19
20 ***********************************************************************/
21 #ifndef ABC__sat__xSAT__xsatSolver_h
22 #define ABC__sat__xSAT__xsatSolver_h
23
24 ////////////////////////////////////////////////////////////////////////
25 /// INCLUDES ///
26 ////////////////////////////////////////////////////////////////////////
27 #include <stdio.h>
28 #include <stdlib.h>
29 #include <string.h>
30 #include <assert.h>
31
32 #include "misc/util/abc_global.h"
33 #include "misc/vec/vecStr.h"
34
35 #include "xsat.h"
36 #include "xsatBQueue.h"
37 #include "xsatClause.h"
38 #include "xsatHeap.h"
39 #include "xsatMemory.h"
40 #include "xsatWatchList.h"
41
42 ABC_NAMESPACE_HEADER_START
43
44 #ifndef __cplusplus
45 #ifndef false
46 # define false 0
47 #endif
48 #ifndef true
49 # define true 1
50 #endif
51 #endif
52
53 enum
54 {
55 Var0 = 1,
56 Var1 = 0,
57 VarX = 3
58 };
59
60 enum
61 {
62 LBoolUndef = 0,
63 LBoolTrue = 1,
64 LBoolFalse = -1
65 };
66
67 enum
68 {
69 VarUndef = -1,
70 LitUndef = -2
71 };
72
73 #define CRefUndef 0xFFFFFFFF
74
75 ////////////////////////////////////////////////////////////////////////
76 /// STRUCTURE DEFINITIONS ///
77 ////////////////////////////////////////////////////////////////////////
78 typedef struct xSAT_SolverOptions_t_ xSAT_SolverOptions_t;
79 struct xSAT_SolverOptions_t_
80 {
81 char fVerbose;
82
83 // Limits
84 iword nConfLimit; // external limit on the number of conflicts
85 iword nInsLimit; // external limit on the number of implications
86 abctime nRuntimeLimit; // external limit on runtime
87
88 // Constants used for restart heuristic
89 double K; // Forces a restart
90 double R; // Block a restart
91 int nFirstBlockRestart; // Lower bound number of conflicts for start blocking restarts
92 int nSizeLBDQueue; // Size of the moving avarege queue for LBD (force restart)
93 int nSizeTrailQueue; // Size of the moving avarege queue for Trail size (block restart)
94
95 // Constants used for clause database reduction heuristic
96 int nConfFirstReduce; // Number of conflicts before first reduction
97 int nIncReduce; // Increment to reduce
98 int nSpecialIncReduce; // Special increment to reduce
99 unsigned nLBDFrozenClause;
100 };
101
102 typedef struct xSAT_Stats_t_ xSAT_Stats_t;
103 struct xSAT_Stats_t_
104 {
105 unsigned nStarts;
106 unsigned nReduceDB;
107
108 iword nDecisions;
109 iword nPropagations;
110 iword nInspects;
111 iword nConflicts;
112
113 iword nClauseLits;
114 iword nLearntLits;
115 };
116
117 struct xSAT_Solver_t_
118 {
119 /* Clauses Database */
120 xSAT_Mem_t * pMemory;
121 Vec_Int_t * vLearnts;
122 Vec_Int_t * vClauses;
123 xSAT_VecWatchList_t * vWatches;
124 xSAT_VecWatchList_t * vBinWatches;
125
126 /* Activity heuristic */
127 int nVarActInc; /* Amount to bump next variable with. */
128 int nClaActInc; /* Amount to bump next clause with. */
129
130 /* Variable Information */
131 Vec_Int_t * vActivity; /* A heuristic measurement of the activity of a variable. */
132 xSAT_Heap_t * hOrder;
133 Vec_Int_t * vLevels; /* Decision level of the current assignment */
134 Vec_Int_t * vReasons; /* Reason (clause) of the current assignment */
135 Vec_Str_t * vAssigns; /* Current assignment. */
136 Vec_Str_t * vPolarity;
137 Vec_Str_t * vTags;
138
139 /* Assignments */
140 Vec_Int_t * vTrail;
141 Vec_Int_t * vTrailLim; // Separator indices for different decision levels in 'trail'.
142 int iQhead; // Head of propagation queue (as index into the trail).
143
144 int nAssignSimplify; /* Number of top-level assignments since last
145 * execution of 'simplify()'. */
146 iword nPropSimplify; /* Remaining number of propagations that must be
147 * made before next execution of 'simplify()'. */
148
149 /* Temporary data used by Search method */
150 xSAT_BQueue_t * bqTrail;
151 xSAT_BQueue_t * bqLBD;
152 float nSumLBD;
153 int nConfBeforeReduce;
154 long nRC1;
155 int nRC2;
156
157 /* Temporary data used by Analyze */
158 Vec_Int_t * vLearntClause;
159 Vec_Str_t * vSeen;
160 Vec_Int_t * vTagged;
161 Vec_Int_t * vStack;
162 Vec_Int_t * vLastDLevel;
163
164 /* Misc temporary */
165 unsigned nStamp;
166 Vec_Int_t * vStamp; /* Multipurpose stamp used to calculate LBD and
167 * clauses minimization with binary resolution */
168
169 xSAT_SolverOptions_t Config;
170 xSAT_Stats_t Stats;
171 };
172
xSAT_Var2Lit(int Var,int c)173 static inline int xSAT_Var2Lit( int Var, int c )
174 {
175 return Var + Var + ( c != 0 );
176 }
177
xSAT_NegLit(int Lit)178 static inline int xSAT_NegLit( int Lit )
179 {
180 return Lit ^ 1;
181 }
182
xSAT_Lit2Var(int Lit)183 static inline int xSAT_Lit2Var( int Lit )
184 {
185 return Lit >> 1;
186 }
187
xSAT_LitSign(int Lit)188 static inline int xSAT_LitSign( int Lit )
189 {
190 return Lit & 1;
191 }
192
xSAT_SolverDecisionLevel(xSAT_Solver_t * s)193 static inline int xSAT_SolverDecisionLevel( xSAT_Solver_t * s )
194 {
195 return Vec_IntSize( s->vTrailLim );
196 }
197
xSAT_SolverReadClause(xSAT_Solver_t * s,unsigned h)198 static inline xSAT_Clause_t * xSAT_SolverReadClause( xSAT_Solver_t * s, unsigned h )
199 {
200 return xSAT_MemClauseHand( s->pMemory, h );
201 }
202
xSAT_SolverIsClauseSatisfied(xSAT_Solver_t * s,xSAT_Clause_t * pCla)203 static inline int xSAT_SolverIsClauseSatisfied( xSAT_Solver_t * s, xSAT_Clause_t * pCla )
204 {
205 int i;
206 int * Lits = &( pCla->pData[0].Lit );
207
208 for ( i = 0; i < pCla->nSize; i++ )
209 if ( Vec_StrEntry( s->vAssigns, xSAT_Lit2Var( Lits[i] ) ) == xSAT_LitSign( ( Lits[i] ) ) )
210 return true;
211
212 return false;
213 }
214
xSAT_SolverPrintClauses(xSAT_Solver_t * s)215 static inline void xSAT_SolverPrintClauses( xSAT_Solver_t * s )
216 {
217 int i;
218 unsigned CRef;
219
220 Vec_IntForEachEntry( s->vClauses, CRef, i )
221 xSAT_ClausePrint( xSAT_SolverReadClause( s, CRef ) );
222 }
223
xSAT_SolverPrintState(xSAT_Solver_t * s)224 static inline void xSAT_SolverPrintState( xSAT_Solver_t * s )
225 {
226 printf( "starts : %10d\n", s->Stats.nStarts );
227 printf( "conflicts : %10ld\n", s->Stats.nConflicts );
228 printf( "decisions : %10ld\n", s->Stats.nDecisions );
229 printf( "propagations : %10ld\n", s->Stats.nPropagations );
230 }
231
232
233 ////////////////////////////////////////////////////////////////////////
234 /// FUNCTION DECLARATIONS ///
235 ////////////////////////////////////////////////////////////////////////
236 extern unsigned xSAT_SolverClaNew( xSAT_Solver_t* s, Vec_Int_t * vLits, int fLearnt );
237 extern char xSAT_SolverSearch( xSAT_Solver_t * s );
238
239 extern void xSAT_SolverGarbageCollect( xSAT_Solver_t * s );
240
241 extern int xSAT_SolverEnqueue( xSAT_Solver_t* s, int Lit, unsigned From );
242 extern void xSAT_SolverCancelUntil( xSAT_Solver_t* s, int Level);
243 extern unsigned xSAT_SolverPropagate( xSAT_Solver_t* s );
244 extern void xSAT_SolverRebuildOrderHeap( xSAT_Solver_t* s );
245
246 ABC_NAMESPACE_HEADER_END
247
248 #endif
249