abc-master
 All Data Structures Namespaces Files Functions Variables Typedefs Enumerations Enumerator Friends Macros
msatActivity.c
Go to the documentation of this file.
1 /**CFile****************************************************************
2 
3  FileName [msatActivity.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 controlling activity of variables and 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: msatActivity.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 ////////////////////////////////////////////////////////////////////////
31 /// FUNCTION DEFINITIONS ///
32 ////////////////////////////////////////////////////////////////////////
33 
34 /**Function*************************************************************
35 
36  Synopsis []
37 
38  Description []
39 
40  SideEffects []
41 
42  SeeAlso []
43 
44 ***********************************************************************/
45 void Msat_SolverVarBumpActivity( Msat_Solver_t * p, Msat_Lit_t Lit )
46 {
47  Msat_Var_t Var;
48  if ( p->dVarDecay < 0 ) // (negative decay means static variable order -- don't bump)
49  return;
50  Var = MSAT_LIT2VAR(Lit);
51  p->pdActivity[Var] += p->dVarInc;
52 // p->pdActivity[Var] += p->dVarInc * p->pFactors[Var];
53  if ( p->pdActivity[Var] > 1e100 )
54  Msat_SolverVarRescaleActivity( p );
55  Msat_OrderUpdate( p->pOrder, Var );
56 }
57 
58 /**Function*************************************************************
59 
60  Synopsis []
61 
62  Description []
63 
64  SideEffects []
65 
66  SeeAlso []
67 
68 ***********************************************************************/
69 void Msat_SolverVarDecayActivity( Msat_Solver_t * p )
70 {
71  if ( p->dVarDecay >= 0 )
72  p->dVarInc *= p->dVarDecay;
73 }
74 
75 /**Function*************************************************************
76 
77  Synopsis [Divide all variable activities by 1e100.]
78 
79  Description []
80 
81  SideEffects []
82 
83  SeeAlso []
84 
85 ***********************************************************************/
86 void Msat_SolverVarRescaleActivity( Msat_Solver_t * p )
87 {
88  int i;
89  for ( i = 0; i < p->nVars; i++ )
90  p->pdActivity[i] *= 1e-100;
91  p->dVarInc *= 1e-100;
92 }
93 
94 /**Function*************************************************************
95 
96  Synopsis []
97 
98  Description []
99 
100  SideEffects []
101 
102  SeeAlso []
103 
104 ***********************************************************************/
105 void Msat_SolverClaBumpActivity( Msat_Solver_t * p, Msat_Clause_t * pC )
106 {
107  float Activ;
108  Activ = Msat_ClauseReadActivity(pC);
109  if ( Activ + p->dClaInc > 1e20 )
110  {
111  Msat_SolverClaRescaleActivity( p );
112  Activ = Msat_ClauseReadActivity( pC );
113  }
114  Msat_ClauseWriteActivity( pC, Activ + (float)p->dClaInc );
115 }
116 
117 /**Function*************************************************************
118 
119  Synopsis []
120 
121  Description []
122 
123  SideEffects []
124 
125  SeeAlso []
126 
127 ***********************************************************************/
128 void Msat_SolverClaDecayActivity( Msat_Solver_t * p )
129 {
130  p->dClaInc *= p->dClaDecay;
131 }
132 
133 /**Function*************************************************************
134 
135  Synopsis [Divide all constraint activities by 1e20.]
136 
137  Description []
138 
139  SideEffects []
140 
141  SeeAlso []
142 
143 ***********************************************************************/
144 void Msat_SolverClaRescaleActivity( Msat_Solver_t * p )
145 {
146  Msat_Clause_t ** pLearned;
147  int nLearned, i;
148  float Activ;
149  nLearned = Msat_ClauseVecReadSize( p->vLearned );
150  pLearned = Msat_ClauseVecReadArray( p->vLearned );
151  for ( i = 0; i < nLearned; i++ )
152  {
153  Activ = Msat_ClauseReadActivity( pLearned[i] );
154  Msat_ClauseWriteActivity( pLearned[i], Activ * (float)1e-20 );
155  }
156  p->dClaInc *= 1e-20;
157 }
158 
159 ////////////////////////////////////////////////////////////////////////
160 /// END OF FILE ///
161 ////////////////////////////////////////////////////////////////////////
162 
163 
164 ABC_NAMESPACE_IMPL_END
165 
Msat_Var_t
int Msat_Var_t
Definition: msatInt.h:66
Msat_SolverClaDecayActivity
void Msat_SolverClaDecayActivity(Msat_Solver_t *p)
Definition: msatActivity.c:128
p
static Llb_Mgr_t * p
Definition: llb3Image.c:950
MSAT_LIT2VAR
#define MSAT_LIT2VAR(l)
Definition: msat.h:59
Msat_Clause_t
typedefABC_NAMESPACE_HEADER_START struct Msat_Clause_t_ Msat_Clause_t
INCLUDES ///.
Definition: msatInt.h:57
Msat_Lit_t
int Msat_Lit_t
Definition: msatInt.h:65
Msat_ClauseVecReadSize
int Msat_ClauseVecReadSize(Msat_ClauseVec_t *p)
Definition: msatClauseVec.c:101
Msat_SolverVarBumpActivity
ABC_NAMESPACE_IMPL_START void Msat_SolverVarBumpActivity(Msat_Solver_t *p, Msat_Lit_t Lit)
DECLARATIONS ///.
Definition: msatActivity.c:45
Msat_ClauseWriteActivity
void Msat_ClauseWriteActivity(Msat_Clause_t *pC, float Num)
Definition: msatClause.c:314
Msat_SolverVarDecayActivity
void Msat_SolverVarDecayActivity(Msat_Solver_t *p)
GLOBAL VARIABLES ///.
Definition: msatActivity.c:69
Msat_SolverClaRescaleActivity
void Msat_SolverClaRescaleActivity(Msat_Solver_t *p)
Definition: msatActivity.c:144
Msat_ClauseVecReadArray
Msat_Clause_t ** Msat_ClauseVecReadArray(Msat_ClauseVec_t *p)
Definition: msatClauseVec.c:85
ABC_NAMESPACE_IMPL_END
#define ABC_NAMESPACE_IMPL_END
Definition: abc_global.h:108
ABC_NAMESPACE_IMPL_START
#define ABC_NAMESPACE_IMPL_START
Definition: abc_global.h:107
Minisat::Var
int Var
Definition: SolverTypes.h:42
Msat_OrderUpdate
void Msat_OrderUpdate(Msat_Order_t *p, int Var)
Definition: msatOrderH.c:257
Msat_SolverVarRescaleActivity
void Msat_SolverVarRescaleActivity(Msat_Solver_t *p)
Definition: msatActivity.c:86
Msat_Solver_t
typedefABC_NAMESPACE_HEADER_START struct Msat_Solver_t_ Msat_Solver_t
INCLUDES ///.
Definition: msat.h:42
Msat_ClauseReadActivity
float Msat_ClauseReadActivity(Msat_Clause_t *pC)
Definition: msatClause.c:295
Msat_SolverClaBumpActivity
void Msat_SolverClaBumpActivity(Msat_Solver_t *p, Msat_Clause_t *pC)
Definition: msatActivity.c:105