1 /**CFile****************************************************************
2
3 FileName [msatSort.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 [Sorting 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: msatSort.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 int Msat_SolverSortCompare( Msat_Clause_t ** ppC1, Msat_Clause_t ** ppC2 );
31
32 // Returns a random float 0 <= x < 1. Seed must never be 0.
drand(double seed)33 static double drand(double seed) {
34 int q;
35 seed *= 1389796;
36 q = (int)(seed / 2147483647);
37 seed -= (double)q * 2147483647;
38 return seed / 2147483647; }
39
40 // Returns a random integer 0 <= x < size. Seed must never be 0.
irand(double seed,int size)41 static int irand(double seed, int size) {
42 return (int)(drand(seed) * size); }
43
44 static void Msat_SolverSort( Msat_Clause_t ** array, int size, double seed );
45
46 ////////////////////////////////////////////////////////////////////////
47 /// FUNCTION DEFINITIONS ///
48 ////////////////////////////////////////////////////////////////////////
49
50 /**Function*************************************************************
51
52 Synopsis [Msat_SolverSort the learned clauses in the increasing order of activity.]
53
54 Description []
55
56 SideEffects []
57
58 SeeAlso []
59
60 ***********************************************************************/
Msat_SolverSortDB(Msat_Solver_t * p)61 void Msat_SolverSortDB( Msat_Solver_t * p )
62 {
63 Msat_ClauseVec_t * pVecClauses;
64 Msat_Clause_t ** pLearned;
65 int nLearned;
66 // read the parameters
67 pVecClauses = Msat_SolverReadLearned( p );
68 nLearned = Msat_ClauseVecReadSize( pVecClauses );
69 pLearned = Msat_ClauseVecReadArray( pVecClauses );
70 // Msat_SolverSort the array
71 // qMsat_SolverSort( (void *)pLearned, nLearned, sizeof(Msat_Clause_t *),
72 // (int (*)(const void *, const void *)) Msat_SolverSortCompare );
73 // printf( "Msat_SolverSorting.\n" );
74 Msat_SolverSort( pLearned, nLearned, 91648253 );
75 /*
76 if ( nLearned > 2 )
77 {
78 printf( "Clause 1: %0.20f\n", Msat_ClauseReadActivity(pLearned[0]) );
79 printf( "Clause 2: %0.20f\n", Msat_ClauseReadActivity(pLearned[1]) );
80 printf( "Clause 3: %0.20f\n", Msat_ClauseReadActivity(pLearned[2]) );
81 }
82 */
83 }
84
85 /**Function*************************************************************
86
87 Synopsis [Comparison procedure for two clauses.]
88
89 Description []
90
91 SideEffects []
92
93 SeeAlso []
94
95 ***********************************************************************/
Msat_SolverSortCompare(Msat_Clause_t ** ppC1,Msat_Clause_t ** ppC2)96 int Msat_SolverSortCompare( Msat_Clause_t ** ppC1, Msat_Clause_t ** ppC2 )
97 {
98 float Value1 = Msat_ClauseReadActivity( *ppC1 );
99 float Value2 = Msat_ClauseReadActivity( *ppC2 );
100 if ( Value1 < Value2 )
101 return -1;
102 if ( Value1 > Value2 )
103 return 1;
104 return 0;
105 }
106
107
108 /**Function*************************************************************
109
110 Synopsis [Selection sort for small array size.]
111
112 Description []
113
114 SideEffects []
115
116 SeeAlso []
117
118 ***********************************************************************/
Msat_SolverSortSelection(Msat_Clause_t ** array,int size)119 void Msat_SolverSortSelection( Msat_Clause_t ** array, int size )
120 {
121 Msat_Clause_t * tmp;
122 int i, j, best_i;
123 for ( i = 0; i < size-1; i++ )
124 {
125 best_i = i;
126 for (j = i+1; j < size; j++)
127 {
128 if ( Msat_ClauseReadActivity(array[j]) < Msat_ClauseReadActivity(array[best_i]) )
129 best_i = j;
130 }
131 tmp = array[i]; array[i] = array[best_i]; array[best_i] = tmp;
132 }
133 }
134
135 /**Function*************************************************************
136
137 Synopsis [The original MiniSat sorting procedure.]
138
139 Description [This procedure is used to preserve trace-equivalence
140 with the orignal C++ implemenation of the solver.]
141
142 SideEffects []
143
144 SeeAlso []
145
146 ***********************************************************************/
Msat_SolverSort(Msat_Clause_t ** array,int size,double seed)147 void Msat_SolverSort( Msat_Clause_t ** array, int size, double seed )
148 {
149 if (size <= 15)
150 Msat_SolverSortSelection( array, size );
151 else
152 {
153 Msat_Clause_t * pivot = array[irand(seed, size)];
154 Msat_Clause_t * tmp;
155 int i = -1;
156 int j = size;
157
158 for(;;)
159 {
160 do i++; while( Msat_ClauseReadActivity(array[i]) < Msat_ClauseReadActivity(pivot) );
161 do j--; while( Msat_ClauseReadActivity(pivot) < Msat_ClauseReadActivity(array[j]) );
162
163 if ( i >= j ) break;
164
165 tmp = array[i]; array[i] = array[j]; array[j] = tmp;
166 }
167 Msat_SolverSort(array , i , seed);
168 Msat_SolverSort(&array[i], size-i, seed);
169 }
170 }
171
172 ////////////////////////////////////////////////////////////////////////
173 /// END OF FILE ///
174 ////////////////////////////////////////////////////////////////////////
175
176
177 ABC_NAMESPACE_IMPL_END
178
179