1 /**CFile****************************************************************
2
3 FileName [msatClause.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 [Procedures working with SAT clauses.]
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: msatClause.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 struct Msat_Clause_t_
31 {
32 int Num; // unique number of the clause
33 unsigned fLearned : 1; // 1 if the clause is learned
34 unsigned fMark : 1; // used to mark visited clauses during proof recording
35 unsigned fTypeA : 1; // used to mark clauses belonging to A for interpolant computation
36 unsigned nSize : 14; // the number of literals in the clause
37 unsigned nSizeAlloc : 15; // the number of bytes allocated for the clause
38 Msat_Lit_t pData[0];
39 };
40
41 ////////////////////////////////////////////////////////////////////////
42 /// FUNCTION DEFINITIONS ///
43 ////////////////////////////////////////////////////////////////////////
44
45 /**Function*************************************************************
46
47 Synopsis [Creates a new clause.]
48
49 Description [Returns FALSE if top-level conflict detected (must be handled);
50 TRUE otherwise. 'pClause_out' may be set to NULL if clause is already
51 satisfied by the top-level assignment.]
52
53 SideEffects []
54
55 SeeAlso []
56
57 ***********************************************************************/
Msat_ClauseCreate(Msat_Solver_t * p,Msat_IntVec_t * vLits,int fLearned,Msat_Clause_t ** pClause_out)58 int Msat_ClauseCreate( Msat_Solver_t * p, Msat_IntVec_t * vLits, int fLearned, Msat_Clause_t ** pClause_out )
59 {
60 int * pAssigns = Msat_SolverReadAssignsArray(p);
61 Msat_ClauseVec_t ** pvWatched;
62 Msat_Clause_t * pC;
63 int * pLits;
64 int nLits, i, j;
65 int nBytes;
66 Msat_Var_t Var;
67 int Sign;
68
69 *pClause_out = NULL;
70
71 nLits = Msat_IntVecReadSize(vLits);
72 pLits = Msat_IntVecReadArray(vLits);
73
74 if ( !fLearned )
75 {
76 int * pSeen = Msat_SolverReadSeenArray( p );
77 int nSeenId;
78 assert( Msat_SolverReadDecisionLevel(p) == 0 );
79 // sorting literals makes the code trace-equivalent
80 // with to the original C++ solver
81 Msat_IntVecSort( vLits, 0 );
82 // increment the counter of seen twice
83 nSeenId = Msat_SolverIncrementSeenId( p );
84 nSeenId = Msat_SolverIncrementSeenId( p );
85 // nSeenId - 1 stands for negative
86 // nSeenId stands for positive
87 // Remove false literals
88
89 // there is a bug here!!!!
90 // when the same var in opposite polarities is given, it drops one polarity!!!
91
92 for ( i = j = 0; i < nLits; i++ ) {
93 // get the corresponding variable
94 Var = MSAT_LIT2VAR(pLits[i]);
95 Sign = MSAT_LITSIGN(pLits[i]); // Sign=0 for positive
96 // check if we already saw this variable in the this clause
97 if ( pSeen[Var] >= nSeenId - 1 )
98 {
99 if ( (pSeen[Var] != nSeenId) == Sign ) // the same lit
100 continue;
101 return 1; // two opposite polarity lits -- don't add the clause
102 }
103 // mark the variable as seen
104 pSeen[Var] = nSeenId - !Sign;
105
106 // analize the value of this literal
107 if ( pAssigns[Var] != MSAT_VAR_UNASSIGNED )
108 {
109 if ( pAssigns[Var] == pLits[i] )
110 return 1; // the clause is always true -- don't add anything
111 // the literal has no impact - skip it
112 continue;
113 }
114 // otherwise, add this literal to the clause
115 pLits[j++] = pLits[i];
116 }
117 Msat_IntVecShrink( vLits, j );
118 nLits = j;
119 /*
120 // the problem with this code is that performance is very
121 // sensitive to the ordering of adjacency lits
122 // the best ordering requires fanins first, next fanouts
123 // this ordering is more convenient to make from FRAIG
124
125 // create the adjacency information
126 if ( nLits > 2 )
127 {
128 Msat_Var_t VarI, VarJ;
129 Msat_IntVec_t * pAdjI, * pAdjJ;
130
131 for ( i = 0; i < nLits; i++ )
132 {
133 VarI = MSAT_LIT2VAR(pLits[i]);
134 pAdjI = (Msat_IntVec_t *)p->vAdjacents->pArray[VarI];
135
136 for ( j = i+1; j < nLits; j++ )
137 {
138 VarJ = MSAT_LIT2VAR(pLits[j]);
139 pAdjJ = (Msat_IntVec_t *)p->vAdjacents->pArray[VarJ];
140
141 Msat_IntVecPushUniqueOrder( pAdjI, VarJ, 1 );
142 Msat_IntVecPushUniqueOrder( pAdjJ, VarI, 1 );
143 }
144 }
145 }
146 */
147 }
148 // 'vLits' is now the (possibly) reduced vector of literals.
149 if ( nLits == 0 )
150 return 0;
151 if ( nLits == 1 )
152 return Msat_SolverEnqueue( p, pLits[0], NULL );
153
154 // Allocate clause:
155 // nBytes = sizeof(unsigned)*(nLits + 1 + (int)fLearned);
156 nBytes = sizeof(unsigned)*(nLits + 2 + (int)fLearned);
157 #ifdef USE_SYSTEM_MEMORY_MANAGEMENT
158 pC = (Msat_Clause_t *)ABC_ALLOC( char, nBytes );
159 #else
160 pC = (Msat_Clause_t *)Msat_MmStepEntryFetch( Msat_SolverReadMem(p), nBytes );
161 #endif
162 pC->Num = p->nClauses++;
163 pC->fTypeA = 0;
164 pC->fMark = 0;
165 pC->fLearned = fLearned;
166 pC->nSize = nLits;
167 pC->nSizeAlloc = nBytes;
168 memcpy( pC->pData, pLits, sizeof(int)*nLits );
169
170 // For learnt clauses only:
171 if ( fLearned )
172 {
173 int * pLevel = Msat_SolverReadDecisionLevelArray( p );
174 int iLevelMax, iLevelCur, iLitMax;
175
176 // Put the second watch on the literal with highest decision level:
177 iLitMax = 1;
178 iLevelMax = pLevel[ MSAT_LIT2VAR(pLits[1]) ];
179 for ( i = 2; i < nLits; i++ )
180 {
181 iLevelCur = pLevel[ MSAT_LIT2VAR(pLits[i]) ];
182 assert( iLevelCur != -1 );
183 if ( iLevelMax < iLevelCur )
184 // this is very strange - shouldn't it be???
185 // if ( iLevelMax > iLevelCur )
186 iLevelMax = iLevelCur, iLitMax = i;
187 }
188 pC->pData[1] = pLits[iLitMax];
189 pC->pData[iLitMax] = pLits[1];
190
191 // Bumping:
192 // (newly learnt clauses should be considered active)
193 Msat_ClauseWriteActivity( pC, 0.0 );
194 Msat_SolverClaBumpActivity( p, pC );
195 // if ( nLits < 20 )
196 for ( i = 0; i < nLits; i++ )
197 {
198 Msat_SolverVarBumpActivity( p, pLits[i] );
199 // Msat_SolverVarBumpActivity( p, pLits[i] );
200 // p->pFreq[ MSAT_LIT2VAR(pLits[i]) ]++;
201 }
202 }
203
204 // Store clause:
205 pvWatched = Msat_SolverReadWatchedArray( p );
206 Msat_ClauseVecPush( pvWatched[ MSAT_LITNOT(pC->pData[0]) ], pC );
207 Msat_ClauseVecPush( pvWatched[ MSAT_LITNOT(pC->pData[1]) ], pC );
208 *pClause_out = pC;
209 return 1;
210 }
211
212 /**Function*************************************************************
213
214 Synopsis [Deallocates the clause.]
215
216 Description []
217
218 SideEffects []
219
220 SeeAlso []
221
222 ***********************************************************************/
Msat_ClauseFree(Msat_Solver_t * p,Msat_Clause_t * pC,int fRemoveWatched)223 void Msat_ClauseFree( Msat_Solver_t * p, Msat_Clause_t * pC, int fRemoveWatched )
224 {
225 if ( fRemoveWatched )
226 {
227 Msat_Lit_t Lit;
228 Msat_ClauseVec_t ** pvWatched;
229 pvWatched = Msat_SolverReadWatchedArray( p );
230 Lit = MSAT_LITNOT( pC->pData[0] );
231 Msat_ClauseRemoveWatch( pvWatched[Lit], pC );
232 Lit = MSAT_LITNOT( pC->pData[1] );
233 Msat_ClauseRemoveWatch( pvWatched[Lit], pC );
234 }
235
236 #ifdef USE_SYSTEM_MEMORY_MANAGEMENT
237 ABC_FREE( pC );
238 #else
239 Msat_MmStepEntryRecycle( Msat_SolverReadMem(p), (char *)pC, pC->nSizeAlloc );
240 #endif
241
242 }
243
244 /**Function*************************************************************
245
246 Synopsis [Access the data field of the clause.]
247
248 Description []
249
250 SideEffects []
251
252 SeeAlso []
253
254 ***********************************************************************/
Msat_ClauseReadLearned(Msat_Clause_t * pC)255 int Msat_ClauseReadLearned( Msat_Clause_t * pC ) { return pC->fLearned; }
Msat_ClauseReadSize(Msat_Clause_t * pC)256 int Msat_ClauseReadSize( Msat_Clause_t * pC ) { return pC->nSize; }
Msat_ClauseReadLits(Msat_Clause_t * pC)257 int * Msat_ClauseReadLits( Msat_Clause_t * pC ) { return pC->pData; }
Msat_ClauseReadMark(Msat_Clause_t * pC)258 int Msat_ClauseReadMark( Msat_Clause_t * pC ) { return pC->fMark; }
Msat_ClauseReadNum(Msat_Clause_t * pC)259 int Msat_ClauseReadNum( Msat_Clause_t * pC ) { return pC->Num; }
Msat_ClauseReadTypeA(Msat_Clause_t * pC)260 int Msat_ClauseReadTypeA( Msat_Clause_t * pC ) { return pC->fTypeA; }
261
Msat_ClauseSetMark(Msat_Clause_t * pC,int fMark)262 void Msat_ClauseSetMark( Msat_Clause_t * pC, int fMark ) { pC->fMark = fMark; }
Msat_ClauseSetNum(Msat_Clause_t * pC,int Num)263 void Msat_ClauseSetNum( Msat_Clause_t * pC, int Num ) { pC->Num = Num; }
Msat_ClauseSetTypeA(Msat_Clause_t * pC,int fTypeA)264 void Msat_ClauseSetTypeA( Msat_Clause_t * pC, int fTypeA ) { pC->fTypeA = fTypeA; }
265
266 /**Function*************************************************************
267
268 Synopsis [Checks whether the learned clause is locked.]
269
270 Description [The clause may be locked if it is the reason of a
271 recent conflict. Such clause cannot be removed from the database.]
272
273 SideEffects []
274
275 SeeAlso []
276
277 ***********************************************************************/
Msat_ClauseIsLocked(Msat_Solver_t * p,Msat_Clause_t * pC)278 int Msat_ClauseIsLocked( Msat_Solver_t * p, Msat_Clause_t * pC )
279 {
280 Msat_Clause_t ** pReasons = Msat_SolverReadReasonArray( p );
281 return (int )(pReasons[MSAT_LIT2VAR(pC->pData[0])] == pC);
282 }
283
284 /**Function*************************************************************
285
286 Synopsis [Reads the activity of the given clause.]
287
288 Description []
289
290 SideEffects []
291
292 SeeAlso []
293
294 ***********************************************************************/
Msat_ClauseReadActivity(Msat_Clause_t * pC)295 float Msat_ClauseReadActivity( Msat_Clause_t * pC )
296 {
297 float f;
298
299 memcpy( &f, pC->pData + pC->nSize, sizeof (f));
300 return f;
301 }
302
303 /**Function*************************************************************
304
305 Synopsis [Sets the activity of the clause.]
306
307 Description []
308
309 SideEffects []
310
311 SeeAlso []
312
313 ***********************************************************************/
Msat_ClauseWriteActivity(Msat_Clause_t * pC,float Num)314 void Msat_ClauseWriteActivity( Msat_Clause_t * pC, float Num )
315 {
316 memcpy( pC->pData + pC->nSize, &Num, sizeof (Num) );
317 }
318
319 /**Function*************************************************************
320
321 Synopsis [Propages the assignment.]
322
323 Description [The literal that has become true (Lit) is given to this
324 procedure. The array of current variable assignments is given for
325 efficiency. The output literal (pLit_out) can be the second watched
326 literal (if TRUE is returned) or the conflict literal (if FALSE is
327 returned). This messy interface is used to improve performance.
328 This procedure accounts for ~50% of the runtime of the solver.]
329
330 SideEffects []
331
332 SeeAlso []
333
334 ***********************************************************************/
Msat_ClausePropagate(Msat_Clause_t * pC,Msat_Lit_t Lit,int * pAssigns,Msat_Lit_t * pLit_out)335 int Msat_ClausePropagate( Msat_Clause_t * pC, Msat_Lit_t Lit, int * pAssigns, Msat_Lit_t * pLit_out )
336 {
337 // make sure the false literal is pC->pData[1]
338 Msat_Lit_t LitF = MSAT_LITNOT(Lit);
339 if ( pC->pData[0] == LitF )
340 pC->pData[0] = pC->pData[1], pC->pData[1] = LitF;
341 assert( pC->pData[1] == LitF );
342 // if the 0-th watch is true, clause is already satisfied
343 if ( pAssigns[MSAT_LIT2VAR(pC->pData[0])] == pC->pData[0] )
344 return 1;
345 // look for a new watch
346 if ( pC->nSize > 2 )
347 {
348 int i;
349 for ( i = 2; i < (int)pC->nSize; i++ )
350 if ( pAssigns[MSAT_LIT2VAR(pC->pData[i])] != MSAT_LITNOT(pC->pData[i]) )
351 {
352 pC->pData[1] = pC->pData[i], pC->pData[i] = LitF;
353 *pLit_out = MSAT_LITNOT(pC->pData[1]);
354 return 1;
355 }
356 }
357 // clause is unit under assignment
358 *pLit_out = pC->pData[0];
359 return 0;
360 }
361
362 /**Function*************************************************************
363
364 Synopsis [Simplifies the clause.]
365
366 Description [Assumes everything has been propagated! (esp. watches
367 in clauses are NOT unsatisfied)]
368
369 SideEffects []
370
371 SeeAlso []
372
373 ***********************************************************************/
Msat_ClauseSimplify(Msat_Clause_t * pC,int * pAssigns)374 int Msat_ClauseSimplify( Msat_Clause_t * pC, int * pAssigns )
375 {
376 Msat_Var_t Var;
377 int i, j;
378 for ( i = j = 0; i < (int)pC->nSize; i++ )
379 {
380 Var = MSAT_LIT2VAR(pC->pData[i]);
381 if ( pAssigns[Var] == MSAT_VAR_UNASSIGNED )
382 {
383 pC->pData[j++] = pC->pData[i];
384 continue;
385 }
386 if ( pAssigns[Var] == pC->pData[i] )
387 return 1;
388 // otherwise, the value of the literal is false
389 // make sure, this literal is not watched
390 assert( i >= 2 );
391 }
392 // if the size has changed, update it and move activity
393 if ( j < (int)pC->nSize )
394 {
395 float Activ = Msat_ClauseReadActivity(pC);
396 pC->nSize = j;
397 Msat_ClauseWriteActivity(pC, Activ);
398 }
399 return 0;
400 }
401
402 /**Function*************************************************************
403
404 Synopsis [Computes reason of conflict in the given clause.]
405
406 Description [If the literal is unassigned, finds the reason by
407 complementing literals in the given cluase (pC). If the literal is
408 assigned, makes sure that this literal is the first one in the clause
409 and computes the complement of all other literals in the clause.
410 Returns the reason in the given array (vLits_out). If the clause is
411 learned, bumps its activity.]
412
413 SideEffects []
414
415 SeeAlso []
416
417 ***********************************************************************/
Msat_ClauseCalcReason(Msat_Solver_t * p,Msat_Clause_t * pC,Msat_Lit_t Lit,Msat_IntVec_t * vLits_out)418 void Msat_ClauseCalcReason( Msat_Solver_t * p, Msat_Clause_t * pC, Msat_Lit_t Lit, Msat_IntVec_t * vLits_out )
419 {
420 int i;
421 // clear the reason
422 Msat_IntVecClear( vLits_out );
423 assert( Lit == MSAT_LIT_UNASSIGNED || Lit == pC->pData[0] );
424 for ( i = (Lit != MSAT_LIT_UNASSIGNED); i < (int)pC->nSize; i++ )
425 {
426 assert( Msat_SolverReadAssignsArray(p)[MSAT_LIT2VAR(pC->pData[i])] == MSAT_LITNOT(pC->pData[i]) );
427 Msat_IntVecPush( vLits_out, MSAT_LITNOT(pC->pData[i]) );
428 }
429 if ( pC->fLearned )
430 Msat_SolverClaBumpActivity( p, pC );
431 }
432
433 /**Function*************************************************************
434
435 Synopsis [Removes the given clause from the watched list.]
436
437 Description []
438
439 SideEffects []
440
441 SeeAlso []
442
443 ***********************************************************************/
Msat_ClauseRemoveWatch(Msat_ClauseVec_t * vClauses,Msat_Clause_t * pC)444 void Msat_ClauseRemoveWatch( Msat_ClauseVec_t * vClauses, Msat_Clause_t * pC )
445 {
446 Msat_Clause_t ** pClauses;
447 int nClauses, i;
448 nClauses = Msat_ClauseVecReadSize( vClauses );
449 pClauses = Msat_ClauseVecReadArray( vClauses );
450 for ( i = 0; pClauses[i] != pC; i++ )
451 assert( i < nClauses );
452 for ( ; i < nClauses - 1; i++ )
453 pClauses[i] = pClauses[i+1];
454 Msat_ClauseVecPop( vClauses );
455 }
456
457 /**Function*************************************************************
458
459 Synopsis [Prints the given clause.]
460
461 Description []
462
463 SideEffects []
464
465 SeeAlso []
466
467 ***********************************************************************/
Msat_ClausePrint(Msat_Clause_t * pC)468 void Msat_ClausePrint( Msat_Clause_t * pC )
469 {
470 int i;
471 if ( pC == NULL )
472 printf( "NULL pointer" );
473 else
474 {
475 if ( pC->fLearned )
476 printf( "Act = %.4f ", Msat_ClauseReadActivity(pC) );
477 for ( i = 0; i < (int)pC->nSize; i++ )
478 printf( " %s%d", ((pC->pData[i]&1)? "-": ""), pC->pData[i]/2 + 1 );
479 }
480 printf( "\n" );
481 }
482
483 /**Function*************************************************************
484
485 Synopsis [Writes the given clause in a file in DIMACS format.]
486
487 Description []
488
489 SideEffects []
490
491 SeeAlso []
492
493 ***********************************************************************/
Msat_ClauseWriteDimacs(FILE * pFile,Msat_Clause_t * pC,int fIncrement)494 void Msat_ClauseWriteDimacs( FILE * pFile, Msat_Clause_t * pC, int fIncrement )
495 {
496 int i;
497 for ( i = 0; i < (int)pC->nSize; i++ )
498 fprintf( pFile, "%s%d ", ((pC->pData[i]&1)? "-": ""), pC->pData[i]/2 + (int)(fIncrement>0) );
499 if ( fIncrement )
500 fprintf( pFile, "0" );
501 fprintf( pFile, "\n" );
502 }
503
504 /**Function*************************************************************
505
506 Synopsis [Prints the given clause.]
507
508 Description []
509
510 SideEffects []
511
512 SeeAlso []
513
514 ***********************************************************************/
Msat_ClausePrintSymbols(Msat_Clause_t * pC)515 void Msat_ClausePrintSymbols( Msat_Clause_t * pC )
516 {
517 int i;
518 if ( pC == NULL )
519 printf( "NULL pointer" );
520 else
521 {
522 // if ( pC->fLearned )
523 // printf( "Act = %.4f ", Msat_ClauseReadActivity(pC) );
524 for ( i = 0; i < (int)pC->nSize; i++ )
525 printf(" "L_LIT, L_lit(pC->pData[i]));
526 }
527 printf( "\n" );
528 }
529
530
531 ////////////////////////////////////////////////////////////////////////
532 /// END OF FILE ///
533 ////////////////////////////////////////////////////////////////////////
534
535
536 ABC_NAMESPACE_IMPL_END
537
538