1 |
| |
2 |
| |
3 |
| |
4 |
| |
5 |
| |
6 |
| |
7 |
| |
8 |
| |
9 |
| |
10 |
| |
11 |
| |
12 |
| |
13 |
| |
14 |
| |
15 |
| |
16 |
| |
17 |
| |
18 |
| |
19 |
| |
20 |
| |
21 |
| |
22 |
| |
23 |
| |
24 |
| |
25 |
| |
26 |
| package org.sat4j.minisat.orders; |
27 |
| |
28 |
| import java.io.PrintWriter; |
29 |
| import java.io.Serializable; |
30 |
| |
31 |
| import org.sat4j.minisat.core.Heap; |
32 |
| import org.sat4j.minisat.core.ILits; |
33 |
| import org.sat4j.minisat.core.IOrder; |
34 |
| |
35 |
| |
36 |
| |
37 |
| |
38 |
| |
39 |
| |
40 |
| |
41 |
| |
42 |
| |
43 |
| public class VarOrderHeap implements IOrder, Serializable { |
44 |
| |
45 |
| private static final long serialVersionUID = 1L; |
46 |
| |
47 |
| private static final double VAR_RESCALE_FACTOR = 1e-100; |
48 |
| |
49 |
| private static final double VAR_RESCALE_BOUND = 1 / VAR_RESCALE_FACTOR; |
50 |
| |
51 |
| |
52 |
| |
53 |
| |
54 |
| protected double[] activity = new double[1]; |
55 |
| |
56 |
| private double varDecay = 1.0; |
57 |
| |
58 |
| |
59 |
| |
60 |
| |
61 |
| private double varInc = 1.0; |
62 |
| |
63 |
| protected ILits lits; |
64 |
| |
65 |
| private long nullchoice = 0; |
66 |
| |
67 |
| protected Heap heap; |
68 |
| |
69 |
| protected int[] phase; |
70 |
| |
71 |
1383
| public void setLits(ILits lits) {
|
72 |
1383
| this.lits = lits;
|
73 |
| } |
74 |
| |
75 |
| |
76 |
| |
77 |
| |
78 |
659841
| public void newVar() {
|
79 |
659841
| newVar(1);
|
80 |
| } |
81 |
| |
82 |
| |
83 |
| |
84 |
| |
85 |
| |
86 |
| |
87 |
660484
| public void newVar(int howmany) {
|
88 |
| } |
89 |
| |
90 |
| |
91 |
| |
92 |
| |
93 |
| |
94 |
| |
95 |
| |
96 |
53435489
| public int select() {
|
97 |
96752822
| while (!heap.empty()) {
|
98 |
96752822
| int var = heap.getmin();
|
99 |
96752822
| int next = phase[var];
|
100 |
96752822
| if (lits.isUnassigned(next)) {
|
101 |
53435489
| if (activity[var] < 0.0001) {
|
102 |
329005
| nullchoice++;
|
103 |
| } |
104 |
53435489
| return next;
|
105 |
| } |
106 |
| } |
107 |
0
| return ILits.UNDEFINED;
|
108 |
| } |
109 |
| |
110 |
| |
111 |
| |
112 |
| |
113 |
| |
114 |
| |
115 |
2695
| public void setVarDecay(double d) {
|
116 |
2695
| varDecay = d;
|
117 |
| } |
118 |
| |
119 |
| |
120 |
| |
121 |
| |
122 |
| |
123 |
| |
124 |
880632813
| public void undo(int x) {
|
125 |
880632813
| if (!heap.inHeap(x))
|
126 |
96744762
| heap.insert(x);
|
127 |
| } |
128 |
| |
129 |
| |
130 |
| |
131 |
| |
132 |
| |
133 |
| |
134 |
411588354
| public void updateVar(int p) {
|
135 |
411588354
| int var = p >> 1;
|
136 |
411588354
| updateActivity(var);
|
137 |
411588354
| phase[var] = p;
|
138 |
411588354
| if (heap.inHeap(var))
|
139 |
741890987
| heap.increase(var);
|
140 |
| } |
141 |
| |
142 |
411588354
| protected void updateActivity(final int var) {
|
143 |
411588354
| if ((activity[var] += varInc) > VAR_RESCALE_BOUND) {
|
144 |
8422
| varRescaleActivity();
|
145 |
| } |
146 |
| } |
147 |
| |
148 |
| |
149 |
| |
150 |
| |
151 |
38114704
| public void varDecayActivity() {
|
152 |
38114704
| varInc *= varDecay;
|
153 |
| } |
154 |
| |
155 |
| |
156 |
| |
157 |
| |
158 |
8422
| private void varRescaleActivity() {
|
159 |
8422
| for (int i = 1; i < activity.length; i++) {
|
160 |
1278780
| activity[i] *= VAR_RESCALE_FACTOR;
|
161 |
| } |
162 |
8422
| varInc *= VAR_RESCALE_FACTOR;
|
163 |
| } |
164 |
| |
165 |
0
| public double varActivity(int p) {
|
166 |
0
| return activity[p >> 1];
|
167 |
| } |
168 |
| |
169 |
| |
170 |
| |
171 |
| |
172 |
0
| public int numberOfInterestingVariables() {
|
173 |
0
| int cpt = 0;
|
174 |
0
| for (int i = 1; i < activity.length; i++) {
|
175 |
0
| if (activity[i] > 1.0) {
|
176 |
0
| cpt++;
|
177 |
| } |
178 |
| } |
179 |
0
| return cpt;
|
180 |
| } |
181 |
| |
182 |
| |
183 |
| |
184 |
| |
185 |
| |
186 |
1245
| public void init() {
|
187 |
1245
| int nlength = lits.nVars() + 1;
|
188 |
1245
| activity = new double[nlength];
|
189 |
1245
| phase = new int[nlength];
|
190 |
1245
| activity[0] = -1;
|
191 |
1245
| heap = new Heap(activity);
|
192 |
1245
| heap.setBounds(nlength);
|
193 |
1245
| for (int i = 1; i < nlength; i++) {
|
194 |
| assert i > 0; |
195 |
| assert i <= lits.nVars() : "" + lits.nVars() + "/" + i; |
196 |
806866
| activity[i] = 0.0;
|
197 |
806866
| if (lits.belongsToPool(i)) {
|
198 |
806866
| heap.insert(i);
|
199 |
806866
| phase[i] = (i << 1) ^ 1;
|
200 |
| } else { |
201 |
0
| phase[i] = ILits.UNDEFINED;
|
202 |
| } |
203 |
| } |
204 |
| } |
205 |
| |
206 |
0
| @Override
|
207 |
| public String toString() { |
208 |
0
| return "VSIDS like heuristics from MiniSAT using a heap";
|
209 |
| } |
210 |
| |
211 |
0
| public ILits getVocabulary() {
|
212 |
0
| return lits;
|
213 |
| } |
214 |
| |
215 |
0
| public void printStat(PrintWriter out, String prefix) {
|
216 |
0
| out.println(prefix + "non guided choices\t" + nullchoice);
|
217 |
| } |
218 |
| } |