1 /**CFile****************************************************************
2
3 FileName [msatSolverApi.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 [APIs of the SAT 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: msatSolverApi.c,v 1.0 2004/01/01 1:00:00 alanmi Exp $]
18
19 ***********************************************************************/
20
21 #include "msatInt.h"
22
23 ABC_NAMESPACE_IMPL_START
24
25
26 ////////////////////////////////////////////////////////////////////////
27 /// DECLARATIONS ///
28 ////////////////////////////////////////////////////////////////////////
29
30 static void Msat_SolverSetupTruthTables( unsigned uTruths[][2] );
31
32 ////////////////////////////////////////////////////////////////////////
33 /// FUNCTION DEFINITIONS ///
34 ////////////////////////////////////////////////////////////////////////
35
36 /**Function*************************************************************
37
38 Synopsis [Simple SAT solver APIs.]
39
40 Description []
41
42 SideEffects []
43
44 SeeAlso []
45
46 ***********************************************************************/
Msat_SolverReadVarNum(Msat_Solver_t * p)47 int Msat_SolverReadVarNum( Msat_Solver_t * p ) { return p->nVars; }
Msat_SolverReadClauseNum(Msat_Solver_t * p)48 int Msat_SolverReadClauseNum( Msat_Solver_t * p ) { return p->nClauses; }
Msat_SolverReadVarAllocNum(Msat_Solver_t * p)49 int Msat_SolverReadVarAllocNum( Msat_Solver_t * p ) { return p->nVarsAlloc; }
Msat_SolverReadDecisionLevel(Msat_Solver_t * p)50 int Msat_SolverReadDecisionLevel( Msat_Solver_t * p ) { return Msat_IntVecReadSize(p->vTrailLim); }
Msat_SolverReadDecisionLevelArray(Msat_Solver_t * p)51 int * Msat_SolverReadDecisionLevelArray( Msat_Solver_t * p ) { return p->pLevel; }
Msat_SolverReadReasonArray(Msat_Solver_t * p)52 Msat_Clause_t ** Msat_SolverReadReasonArray( Msat_Solver_t * p ) { return p->pReasons; }
Msat_SolverReadVarValue(Msat_Solver_t * p,Msat_Var_t Var)53 Msat_Type_t Msat_SolverReadVarValue( Msat_Solver_t * p, Msat_Var_t Var ) { return (Msat_Type_t)p->pAssigns[Var]; }
Msat_SolverReadLearned(Msat_Solver_t * p)54 Msat_ClauseVec_t * Msat_SolverReadLearned( Msat_Solver_t * p ) { return p->vLearned; }
Msat_SolverReadWatchedArray(Msat_Solver_t * p)55 Msat_ClauseVec_t ** Msat_SolverReadWatchedArray( Msat_Solver_t * p ) { return p->pvWatched; }
Msat_SolverReadAssignsArray(Msat_Solver_t * p)56 int * Msat_SolverReadAssignsArray( Msat_Solver_t * p ) { return p->pAssigns; }
Msat_SolverReadModelArray(Msat_Solver_t * p)57 int * Msat_SolverReadModelArray( Msat_Solver_t * p ) { return p->pModel; }
Msat_SolverReadBackTracks(Msat_Solver_t * p)58 int Msat_SolverReadBackTracks( Msat_Solver_t * p ) { return (int)p->Stats.nConflicts; }
Msat_SolverReadInspects(Msat_Solver_t * p)59 int Msat_SolverReadInspects( Msat_Solver_t * p ) { return (int)p->Stats.nInspects; }
Msat_SolverReadMem(Msat_Solver_t * p)60 Msat_MmStep_t * Msat_SolverReadMem( Msat_Solver_t * p ) { return p->pMem; }
Msat_SolverReadSeenArray(Msat_Solver_t * p)61 int * Msat_SolverReadSeenArray( Msat_Solver_t * p ) { return p->pSeen; }
Msat_SolverIncrementSeenId(Msat_Solver_t * p)62 int Msat_SolverIncrementSeenId( Msat_Solver_t * p ) { return ++p->nSeenId; }
Msat_SolverSetVerbosity(Msat_Solver_t * p,int fVerbose)63 void Msat_SolverSetVerbosity( Msat_Solver_t * p, int fVerbose ) { p->fVerbose = fVerbose; }
Msat_SolverClausesIncrement(Msat_Solver_t * p)64 void Msat_SolverClausesIncrement( Msat_Solver_t * p ) { p->nClausesAlloc++; }
Msat_SolverClausesDecrement(Msat_Solver_t * p)65 void Msat_SolverClausesDecrement( Msat_Solver_t * p ) { p->nClausesAlloc--; }
Msat_SolverClausesIncrementL(Msat_Solver_t * p)66 void Msat_SolverClausesIncrementL( Msat_Solver_t * p ) { p->nClausesAllocL++; }
Msat_SolverClausesDecrementL(Msat_Solver_t * p)67 void Msat_SolverClausesDecrementL( Msat_Solver_t * p ) { p->nClausesAllocL--; }
Msat_SolverMarkLastClauseTypeA(Msat_Solver_t * p)68 void Msat_SolverMarkLastClauseTypeA( Msat_Solver_t * p ) { Msat_ClauseSetTypeA( Msat_ClauseVecReadEntry( p->vClauses, Msat_ClauseVecReadSize(p->vClauses)-1 ), 1 ); }
Msat_SolverMarkClausesStart(Msat_Solver_t * p)69 void Msat_SolverMarkClausesStart( Msat_Solver_t * p ) { p->nClausesStart = Msat_ClauseVecReadSize(p->vClauses); }
Msat_SolverReadFactors(Msat_Solver_t * p)70 float * Msat_SolverReadFactors( Msat_Solver_t * p ) { return p->pFactors; }
71
72 /**Function*************************************************************
73
74 Synopsis [Reads the clause with the given number.]
75
76 Description []
77
78 SideEffects []
79
80 SeeAlso []
81
82 ***********************************************************************/
Msat_SolverReadClause(Msat_Solver_t * p,int Num)83 Msat_Clause_t * Msat_SolverReadClause( Msat_Solver_t * p, int Num )
84 {
85 int nClausesP;
86 assert( Num < p->nClauses );
87 nClausesP = Msat_ClauseVecReadSize( p->vClauses );
88 if ( Num < nClausesP )
89 return Msat_ClauseVecReadEntry( p->vClauses, Num );
90 return Msat_ClauseVecReadEntry( p->vLearned, Num - nClausesP );
91 }
92
93 /**Function*************************************************************
94
95 Synopsis [Reads the clause with the given number.]
96
97 Description []
98
99 SideEffects []
100
101 SeeAlso []
102
103 ***********************************************************************/
Msat_SolverReadAdjacents(Msat_Solver_t * p)104 Msat_ClauseVec_t * Msat_SolverReadAdjacents( Msat_Solver_t * p )
105 {
106 return p->vAdjacents;
107 }
108
109 /**Function*************************************************************
110
111 Synopsis [Reads the clause with the given number.]
112
113 Description []
114
115 SideEffects []
116
117 SeeAlso []
118
119 ***********************************************************************/
Msat_SolverReadConeVars(Msat_Solver_t * p)120 Msat_IntVec_t * Msat_SolverReadConeVars( Msat_Solver_t * p )
121 {
122 return p->vConeVars;
123 }
124
125 /**Function*************************************************************
126
127 Synopsis [Reads the clause with the given number.]
128
129 Description []
130
131 SideEffects []
132
133 SeeAlso []
134
135 ***********************************************************************/
Msat_SolverReadVarsUsed(Msat_Solver_t * p)136 Msat_IntVec_t * Msat_SolverReadVarsUsed( Msat_Solver_t * p )
137 {
138 return p->vVarsUsed;
139 }
140
141
142 /**Function*************************************************************
143
144 Synopsis [Allocates the solver.]
145
146 Description [After the solver is allocated, the procedure
147 Msat_SolverClean() should be called to set the number of variables.]
148
149 SideEffects []
150
151 SeeAlso []
152
153 ***********************************************************************/
Msat_SolverAlloc(int nVarsAlloc,double dClaInc,double dClaDecay,double dVarInc,double dVarDecay,int fVerbose)154 Msat_Solver_t * Msat_SolverAlloc( int nVarsAlloc,
155 double dClaInc, double dClaDecay,
156 double dVarInc, double dVarDecay,
157 int fVerbose )
158 {
159 Msat_Solver_t * p;
160 int i;
161
162 assert(sizeof(Msat_Lit_t) == sizeof(unsigned));
163 assert(sizeof(float) == sizeof(unsigned));
164
165 p = ABC_ALLOC( Msat_Solver_t, 1 );
166 memset( p, 0, sizeof(Msat_Solver_t) );
167
168 p->nVarsAlloc = nVarsAlloc;
169 p->nVars = 0;
170
171 p->nClauses = 0;
172 p->vClauses = Msat_ClauseVecAlloc( 512 );
173 p->vLearned = Msat_ClauseVecAlloc( 512 );
174
175 p->dClaInc = dClaInc;
176 p->dClaDecay = dClaDecay;
177 p->dVarInc = dVarInc;
178 p->dVarDecay = dVarDecay;
179
180 p->pdActivity = ABC_ALLOC( double, p->nVarsAlloc );
181 p->pFactors = ABC_ALLOC( float, p->nVarsAlloc );
182 for ( i = 0; i < p->nVarsAlloc; i++ )
183 {
184 p->pdActivity[i] = 0.0;
185 p->pFactors[i] = 1.0;
186 }
187
188 p->pAssigns = ABC_ALLOC( int, p->nVarsAlloc );
189 p->pModel = ABC_ALLOC( int, p->nVarsAlloc );
190 for ( i = 0; i < p->nVarsAlloc; i++ )
191 p->pAssigns[i] = MSAT_VAR_UNASSIGNED;
192 // p->pOrder = Msat_OrderAlloc( p->pAssigns, p->pdActivity, p->nVarsAlloc );
193 p->pOrder = Msat_OrderAlloc( p );
194
195 p->pvWatched = ABC_ALLOC( Msat_ClauseVec_t *, 2 * p->nVarsAlloc );
196 for ( i = 0; i < 2 * p->nVarsAlloc; i++ )
197 p->pvWatched[i] = Msat_ClauseVecAlloc( 16 );
198 p->pQueue = Msat_QueueAlloc( p->nVarsAlloc );
199
200 p->vTrail = Msat_IntVecAlloc( p->nVarsAlloc );
201 p->vTrailLim = Msat_IntVecAlloc( p->nVarsAlloc );
202 p->pReasons = ABC_ALLOC( Msat_Clause_t *, p->nVarsAlloc );
203 memset( p->pReasons, 0, sizeof(Msat_Clause_t *) * p->nVarsAlloc );
204 p->pLevel = ABC_ALLOC( int, p->nVarsAlloc );
205 for ( i = 0; i < p->nVarsAlloc; i++ )
206 p->pLevel[i] = -1;
207 p->dRandSeed = 91648253;
208 p->fVerbose = fVerbose;
209 p->dProgress = 0.0;
210 // p->pModel = Msat_IntVecAlloc( p->nVarsAlloc );
211 p->pMem = Msat_MmStepStart( 10 );
212
213 p->vConeVars = Msat_IntVecAlloc( p->nVarsAlloc );
214 p->vAdjacents = Msat_ClauseVecAlloc( p->nVarsAlloc );
215 for ( i = 0; i < p->nVarsAlloc; i++ )
216 Msat_ClauseVecPush( p->vAdjacents, (Msat_Clause_t *)Msat_IntVecAlloc(5) );
217 p->vVarsUsed = Msat_IntVecAlloc( p->nVarsAlloc );
218 Msat_IntVecFill( p->vVarsUsed, p->nVarsAlloc, 1 );
219
220
221 p->pSeen = ABC_ALLOC( int, p->nVarsAlloc );
222 memset( p->pSeen, 0, sizeof(int) * p->nVarsAlloc );
223 p->nSeenId = 1;
224 p->vReason = Msat_IntVecAlloc( p->nVarsAlloc );
225 p->vTemp = Msat_IntVecAlloc( p->nVarsAlloc );
226 return p;
227 }
228
229 /**Function*************************************************************
230
231 Synopsis [Resizes the solver.]
232
233 Description [Assumes that the solver contains some clauses, and that
234 it is currently between the calls. Resizes the solver to accomodate
235 more variables.]
236
237 SideEffects []
238
239 SeeAlso []
240
241 ***********************************************************************/
Msat_SolverResize(Msat_Solver_t * p,int nVarsAlloc)242 void Msat_SolverResize( Msat_Solver_t * p, int nVarsAlloc )
243 {
244 int nVarsAllocOld, i;
245
246 nVarsAllocOld = p->nVarsAlloc;
247 p->nVarsAlloc = nVarsAlloc;
248
249 p->pdActivity = ABC_REALLOC( double, p->pdActivity, p->nVarsAlloc );
250 p->pFactors = ABC_REALLOC( float, p->pFactors, p->nVarsAlloc );
251 for ( i = nVarsAllocOld; i < p->nVarsAlloc; i++ )
252 {
253 p->pdActivity[i] = 0.0;
254 p->pFactors[i] = 1.0;
255 }
256
257 p->pAssigns = ABC_REALLOC( int, p->pAssigns, p->nVarsAlloc );
258 p->pModel = ABC_REALLOC( int, p->pModel, p->nVarsAlloc );
259 for ( i = nVarsAllocOld; i < p->nVarsAlloc; i++ )
260 p->pAssigns[i] = MSAT_VAR_UNASSIGNED;
261
262 // Msat_OrderRealloc( p->pOrder, p->pAssigns, p->pdActivity, p->nVarsAlloc );
263 Msat_OrderSetBounds( p->pOrder, p->nVarsAlloc );
264
265 p->pvWatched = ABC_REALLOC( Msat_ClauseVec_t *, p->pvWatched, 2 * p->nVarsAlloc );
266 for ( i = 2 * nVarsAllocOld; i < 2 * p->nVarsAlloc; i++ )
267 p->pvWatched[i] = Msat_ClauseVecAlloc( 16 );
268
269 Msat_QueueFree( p->pQueue );
270 p->pQueue = Msat_QueueAlloc( p->nVarsAlloc );
271
272 p->pReasons = ABC_REALLOC( Msat_Clause_t *, p->pReasons, p->nVarsAlloc );
273 p->pLevel = ABC_REALLOC( int, p->pLevel, p->nVarsAlloc );
274 for ( i = nVarsAllocOld; i < p->nVarsAlloc; i++ )
275 {
276 p->pReasons[i] = NULL;
277 p->pLevel[i] = -1;
278 }
279
280 p->pSeen = ABC_REALLOC( int, p->pSeen, p->nVarsAlloc );
281 for ( i = nVarsAllocOld; i < p->nVarsAlloc; i++ )
282 p->pSeen[i] = 0;
283
284 Msat_IntVecGrow( p->vTrail, p->nVarsAlloc );
285 Msat_IntVecGrow( p->vTrailLim, p->nVarsAlloc );
286
287 // make sure the array of adjucents has room to store the variable numbers
288 for ( i = Msat_ClauseVecReadSize(p->vAdjacents); i < p->nVarsAlloc; i++ )
289 Msat_ClauseVecPush( p->vAdjacents, (Msat_Clause_t *)Msat_IntVecAlloc(5) );
290 Msat_IntVecFill( p->vVarsUsed, p->nVarsAlloc, 1 );
291 }
292
293 /**Function*************************************************************
294
295 Synopsis [Prepares the solver.]
296
297 Description [Cleans the solver assuming that the problem will involve
298 the given number of variables (nVars). This procedure is useful
299 for many small (incremental) SAT problems, to prevent the solver
300 from being reallocated each time.]
301
302 SideEffects []
303
304 SeeAlso []
305
306 ***********************************************************************/
Msat_SolverClean(Msat_Solver_t * p,int nVars)307 void Msat_SolverClean( Msat_Solver_t * p, int nVars )
308 {
309 int i;
310 // free the clauses
311 int nClauses;
312 Msat_Clause_t ** pClauses;
313
314 assert( p->nVarsAlloc >= nVars );
315 p->nVars = nVars;
316 p->nClauses = 0;
317
318 nClauses = Msat_ClauseVecReadSize( p->vClauses );
319 pClauses = Msat_ClauseVecReadArray( p->vClauses );
320 for ( i = 0; i < nClauses; i++ )
321 Msat_ClauseFree( p, pClauses[i], 0 );
322 // Msat_ClauseVecFree( p->vClauses );
323 Msat_ClauseVecClear( p->vClauses );
324
325 nClauses = Msat_ClauseVecReadSize( p->vLearned );
326 pClauses = Msat_ClauseVecReadArray( p->vLearned );
327 for ( i = 0; i < nClauses; i++ )
328 Msat_ClauseFree( p, pClauses[i], 0 );
329 // Msat_ClauseVecFree( p->vLearned );
330 Msat_ClauseVecClear( p->vLearned );
331
332 // ABC_FREE( p->pdActivity );
333 for ( i = 0; i < p->nVars; i++ )
334 p->pdActivity[i] = 0;
335
336 // Msat_OrderFree( p->pOrder );
337 // Msat_OrderClean( p->pOrder, p->nVars, NULL );
338 Msat_OrderSetBounds( p->pOrder, p->nVars );
339
340 for ( i = 0; i < 2 * p->nVars; i++ )
341 // Msat_ClauseVecFree( p->pvWatched[i] );
342 Msat_ClauseVecClear( p->pvWatched[i] );
343 // ABC_FREE( p->pvWatched );
344 // Msat_QueueFree( p->pQueue );
345 Msat_QueueClear( p->pQueue );
346
347 // ABC_FREE( p->pAssigns );
348 for ( i = 0; i < p->nVars; i++ )
349 p->pAssigns[i] = MSAT_VAR_UNASSIGNED;
350 // Msat_IntVecFree( p->vTrail );
351 Msat_IntVecClear( p->vTrail );
352 // Msat_IntVecFree( p->vTrailLim );
353 Msat_IntVecClear( p->vTrailLim );
354 // ABC_FREE( p->pReasons );
355 memset( p->pReasons, 0, sizeof(Msat_Clause_t *) * p->nVars );
356 // ABC_FREE( p->pLevel );
357 for ( i = 0; i < p->nVars; i++ )
358 p->pLevel[i] = -1;
359 // Msat_IntVecFree( p->pModel );
360 // Msat_MmStepStop( p->pMem, 0 );
361 p->dRandSeed = 91648253;
362 p->dProgress = 0.0;
363
364 // ABC_FREE( p->pSeen );
365 memset( p->pSeen, 0, sizeof(int) * p->nVars );
366 p->nSeenId = 1;
367 // Msat_IntVecFree( p->vReason );
368 Msat_IntVecClear( p->vReason );
369 // Msat_IntVecFree( p->vTemp );
370 Msat_IntVecClear( p->vTemp );
371 // printf(" The number of clauses remaining = %d (%d).\n", p->nClausesAlloc, p->nClausesAllocL );
372 // ABC_FREE( p );
373 }
374
375 /**Function*************************************************************
376
377 Synopsis [Frees the solver.]
378
379 Description []
380
381 SideEffects []
382
383 SeeAlso []
384
385 ***********************************************************************/
Msat_SolverFree(Msat_Solver_t * p)386 void Msat_SolverFree( Msat_Solver_t * p )
387 {
388 int i;
389
390 // free the clauses
391 int nClauses;
392 Msat_Clause_t ** pClauses;
393 //printf( "clauses = %d. learned = %d.\n", Msat_ClauseVecReadSize( p->vClauses ),
394 // Msat_ClauseVecReadSize( p->vLearned ) );
395
396 nClauses = Msat_ClauseVecReadSize( p->vClauses );
397 pClauses = Msat_ClauseVecReadArray( p->vClauses );
398 for ( i = 0; i < nClauses; i++ )
399 Msat_ClauseFree( p, pClauses[i], 0 );
400 Msat_ClauseVecFree( p->vClauses );
401
402 nClauses = Msat_ClauseVecReadSize( p->vLearned );
403 pClauses = Msat_ClauseVecReadArray( p->vLearned );
404 for ( i = 0; i < nClauses; i++ )
405 Msat_ClauseFree( p, pClauses[i], 0 );
406 Msat_ClauseVecFree( p->vLearned );
407
408 ABC_FREE( p->pdActivity );
409 ABC_FREE( p->pFactors );
410 Msat_OrderFree( p->pOrder );
411
412 for ( i = 0; i < 2 * p->nVarsAlloc; i++ )
413 Msat_ClauseVecFree( p->pvWatched[i] );
414 ABC_FREE( p->pvWatched );
415 Msat_QueueFree( p->pQueue );
416
417 ABC_FREE( p->pAssigns );
418 ABC_FREE( p->pModel );
419 Msat_IntVecFree( p->vTrail );
420 Msat_IntVecFree( p->vTrailLim );
421 ABC_FREE( p->pReasons );
422 ABC_FREE( p->pLevel );
423
424 Msat_MmStepStop( p->pMem, 0 );
425
426 nClauses = Msat_ClauseVecReadSize( p->vAdjacents );
427 pClauses = Msat_ClauseVecReadArray( p->vAdjacents );
428 for ( i = 0; i < nClauses; i++ )
429 Msat_IntVecFree( (Msat_IntVec_t *)pClauses[i] );
430 Msat_ClauseVecFree( p->vAdjacents );
431 Msat_IntVecFree( p->vConeVars );
432 Msat_IntVecFree( p->vVarsUsed );
433
434 ABC_FREE( p->pSeen );
435 Msat_IntVecFree( p->vReason );
436 Msat_IntVecFree( p->vTemp );
437 ABC_FREE( p );
438 }
439
440 /**Function*************************************************************
441
442 Synopsis [Prepares the solver to run on a subset of variables.]
443
444 Description []
445
446 SideEffects []
447
448 SeeAlso []
449
450 ***********************************************************************/
Msat_SolverPrepare(Msat_Solver_t * p,Msat_IntVec_t * vVars)451 void Msat_SolverPrepare( Msat_Solver_t * p, Msat_IntVec_t * vVars )
452 {
453
454 int i;
455 // undo the previous data
456 for ( i = 0; i < p->nVarsAlloc; i++ )
457 {
458 p->pAssigns[i] = MSAT_VAR_UNASSIGNED;
459 p->pReasons[i] = NULL;
460 p->pLevel[i] = -1;
461 p->pdActivity[i] = 0.0;
462 }
463
464 // set the new variable order
465 Msat_OrderClean( p->pOrder, vVars );
466
467 Msat_QueueClear( p->pQueue );
468 Msat_IntVecClear( p->vTrail );
469 Msat_IntVecClear( p->vTrailLim );
470 p->dProgress = 0.0;
471 }
472
473 /**Function*************************************************************
474
475 Synopsis [Sets up the truth tables.]
476
477 Description []
478
479 SideEffects []
480
481 SeeAlso []
482
483 ***********************************************************************/
Msat_SolverSetupTruthTables(unsigned uTruths[][2])484 void Msat_SolverSetupTruthTables( unsigned uTruths[][2] )
485 {
486 int m, v;
487 // set up the truth tables
488 for ( m = 0; m < 32; m++ )
489 for ( v = 0; v < 5; v++ )
490 if ( m & (1 << v) )
491 uTruths[v][0] |= (1 << m);
492 // make adjustments for the case of 6 variables
493 for ( v = 0; v < 5; v++ )
494 uTruths[v][1] = uTruths[v][0];
495 uTruths[5][0] = 0;
496 uTruths[5][1] = ~((unsigned)0);
497 }
498
499 ////////////////////////////////////////////////////////////////////////
500 /// END OF FILE ///
501 ////////////////////////////////////////////////////////////////////////
502
503
504 ABC_NAMESPACE_IMPL_END
505
506