1 /**CFile****************************************************************
2
3 FileName [msatSolverCore.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 [The SAT solver core procedures.]
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: msatSolverCore.c,v 1.2 2004/05/12 03:37:40 satrajit Exp $]
18
19 ***********************************************************************/
20
21 #include "msatInt.h"
22
23 ABC_NAMESPACE_IMPL_START
24
25
26 ////////////////////////////////////////////////////////////////////////
27 /// DECLARATIONS ///
28 ////////////////////////////////////////////////////////////////////////
29
30 ////////////////////////////////////////////////////////////////////////
31 /// FUNCTION DEFINITIONS ///
32 ////////////////////////////////////////////////////////////////////////
33
34 /**Function*************************************************************
35
36 Synopsis [Adds one variable to the solver.]
37
38 Description []
39
40 SideEffects []
41
42 SeeAlso []
43
44 ***********************************************************************/
Msat_SolverAddVar(Msat_Solver_t * p,int Level)45 int Msat_SolverAddVar( Msat_Solver_t * p, int Level )
46 {
47 if ( p->nVars == p->nVarsAlloc )
48 Msat_SolverResize( p, 2 * p->nVarsAlloc );
49 p->pLevel[p->nVars] = Level;
50 p->nVars++;
51 return 1;
52 }
53
54 /**Function*************************************************************
55
56 Synopsis [Adds one clause to the solver's clause database.]
57
58 Description []
59
60 SideEffects []
61
62 SeeAlso []
63
64 ***********************************************************************/
Msat_SolverAddClause(Msat_Solver_t * p,Msat_IntVec_t * vLits)65 int Msat_SolverAddClause( Msat_Solver_t * p, Msat_IntVec_t * vLits )
66 {
67 Msat_Clause_t * pC;
68 int Value;
69 Value = Msat_ClauseCreate( p, vLits, 0, &pC );
70 if ( pC != NULL )
71 Msat_ClauseVecPush( p->vClauses, pC );
72 // else if ( p->fProof )
73 // Msat_ClauseCreateFake( p, vLits );
74 return Value;
75 }
76
77 /**Function*************************************************************
78
79 Synopsis [Returns search-space coverage. Not extremely reliable.]
80
81 Description []
82
83 SideEffects []
84
85 SeeAlso []
86
87 ***********************************************************************/
Msat_SolverProgressEstimate(Msat_Solver_t * p)88 double Msat_SolverProgressEstimate( Msat_Solver_t * p )
89 {
90 double dProgress = 0.0;
91 double dF = 1.0 / p->nVars;
92 int i;
93 for ( i = 0; i < p->nVars; i++ )
94 if ( p->pAssigns[i] != MSAT_VAR_UNASSIGNED )
95 dProgress += pow( dF, p->pLevel[i] );
96 return dProgress / p->nVars;
97 }
98
99 /**Function*************************************************************
100
101 Synopsis [Prints statistics about the solver.]
102
103 Description []
104
105 SideEffects []
106
107 SeeAlso []
108
109 ***********************************************************************/
Msat_SolverPrintStats(Msat_Solver_t * p)110 void Msat_SolverPrintStats( Msat_Solver_t * p )
111 {
112 printf("C solver (%d vars; %d clauses; %d learned):\n",
113 p->nVars, Msat_ClauseVecReadSize(p->vClauses), Msat_ClauseVecReadSize(p->vLearned) );
114 printf("starts : %d\n", (int)p->Stats.nStarts);
115 printf("conflicts : %d\n", (int)p->Stats.nConflicts);
116 printf("decisions : %d\n", (int)p->Stats.nDecisions);
117 printf("propagations : %d\n", (int)p->Stats.nPropagations);
118 printf("inspects : %d\n", (int)p->Stats.nInspects);
119 }
120
121 /**Function*************************************************************
122
123 Synopsis [Top-level solve.]
124
125 Description [If using assumptions (non-empty 'assumps' vector), you must
126 call 'simplifyDB()' first to see that no top-level conflict is present
127 (which would put the solver in an undefined state. If the last argument
128 is given (vProj), the solver enumerates through the satisfying solutions,
129 which are projected on the variables listed in this array. Note that the
130 variables in the array may be complemented, in which case the derived
131 assignment for the variable is complemented.]
132
133 SideEffects []
134
135 SeeAlso []
136
137 ***********************************************************************/
Msat_SolverSolve(Msat_Solver_t * p,Msat_IntVec_t * vAssumps,int nBackTrackLimit,int nTimeLimit)138 int Msat_SolverSolve( Msat_Solver_t * p, Msat_IntVec_t * vAssumps, int nBackTrackLimit, int nTimeLimit )
139 {
140 Msat_SearchParams_t Params = { 0.95, 0.999 };
141 double nConflictsLimit, nLearnedLimit;
142 Msat_Type_t Status;
143 abctime timeStart = Abc_Clock();
144
145 // p->pFreq = ABC_ALLOC( int, p->nVarsAlloc );
146 // memset( p->pFreq, 0, sizeof(int) * p->nVarsAlloc );
147
148 if ( vAssumps )
149 {
150 int * pAssumps, nAssumps, i;
151
152 assert( Msat_IntVecReadSize(p->vTrailLim) == 0 );
153
154 nAssumps = Msat_IntVecReadSize( vAssumps );
155 pAssumps = Msat_IntVecReadArray( vAssumps );
156 for ( i = 0; i < nAssumps; i++ )
157 {
158 if ( !Msat_SolverAssume(p, pAssumps[i]) || Msat_SolverPropagate(p) )
159 {
160 Msat_QueueClear( p->pQueue );
161 Msat_SolverCancelUntil( p, 0 );
162 return MSAT_FALSE;
163 }
164 }
165 }
166 p->nLevelRoot = Msat_SolverReadDecisionLevel(p);
167 p->nClausesInit = Msat_ClauseVecReadSize( p->vClauses );
168 nConflictsLimit = 100;
169 nLearnedLimit = Msat_ClauseVecReadSize(p->vClauses) / 3;
170 Status = MSAT_UNKNOWN;
171 p->nBackTracks = (int)p->Stats.nConflicts;
172 while ( Status == MSAT_UNKNOWN )
173 {
174 if ( p->fVerbose )
175 printf("Solving -- conflicts=%d learnts=%d progress=%.4f %%\n",
176 (int)nConflictsLimit, (int)nLearnedLimit, p->dProgress*100);
177 Status = Msat_SolverSearch( p, (int)nConflictsLimit, (int)nLearnedLimit, nBackTrackLimit, &Params );
178 nConflictsLimit *= 1.5;
179 nLearnedLimit *= 1.1;
180 // if the limit on the number of backtracks is given, quit the restart loop
181 if ( nBackTrackLimit > 0 && (int)p->Stats.nConflicts - p->nBackTracks > nBackTrackLimit )
182 break;
183 // if the runtime limit is exceeded, quit the restart loop
184 if ( nTimeLimit > 0 && Abc_Clock() - timeStart >= nTimeLimit * CLOCKS_PER_SEC )
185 break;
186 }
187 Msat_SolverCancelUntil( p, 0 );
188 p->nBackTracks = (int)p->Stats.nConflicts - p->nBackTracks;
189 /*
190 ABC_PRT( "True solver runtime", Abc_Clock() - timeStart );
191 // print the statistics
192 {
193 int i, Counter = 0;
194 for ( i = 0; i < p->nVars; i++ )
195 if ( p->pFreq[i] > 0 )
196 {
197 printf( "%d ", p->pFreq[i] );
198 Counter++;
199 }
200 if ( Counter )
201 printf( "\n" );
202 printf( "Total = %d. Used = %d. Decisions = %d. Imps = %d. Conflicts = %d. ", p->nVars, Counter, (int)p->Stats.nDecisions, (int)p->Stats.nPropagations, (int)p->Stats.nConflicts );
203 ABC_PRT( "Time", Abc_Clock() - timeStart );
204 }
205 */
206 return Status;
207 }
208
209 ////////////////////////////////////////////////////////////////////////
210 /// END OF FILE ///
211 ////////////////////////////////////////////////////////////////////////
212
213
214 ABC_NAMESPACE_IMPL_END
215
216