1 /*
2 * SAT4J: a SATisfiability library for Java Copyright (C) 2004-2006 Daniel Le Berre
3 *
4 * Based on the original minisat specification from:
5 *
6 * An extensible SAT solver. Niklas E?n and Niklas S?rensson. Proceedings of the
7 * Sixth International Conference on Theory and Applications of Satisfiability
8 * Testing, LNCS 2919, pp 502-518, 2003.
9 *
10 * This library is free software; you can redistribute it and/or modify it under
11 * the terms of the GNU Lesser General Public License as published by the Free
12 * Software Foundation; either version 2.1 of the License, or (at your option)
13 * any later version.
14 *
15 * This library is distributed in the hope that it will be useful, but WITHOUT
16 * ANY WARRANTY; without even the implied warranty of MERCHANTABILITY or FITNESS
17 * FOR A PARTICULAR PURPOSE. See the GNU Lesser General Public License for more
18 * details.
19 *
20 * You should have received a copy of the GNU Lesser General Public License
21 * along with this library; if not, write to the Free Software Foundation, Inc.,
22 * 59 Temple Place, Suite 330, Boston, MA 02111-1307 USA
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.ILits;
32 import org.sat4j.minisat.core.IOrder;
33
34 /*
35 * Created on 16 oct. 2003
36 */
37
38 /**
39 * @author leberre Heuristique du prouveur. Changement par rapport au MiniSAT
40 * original : la gestion activity est faite ici et non plus dans Solver.
41 */
42 public class VarOrder<L extends ILits> implements Serializable, IOrder<L> {
43
44 private static final long serialVersionUID = 1L;
45
46 /**
47 * Comparateur permettant de trier les variables
48 */
49 private static final double VAR_RESCALE_FACTOR = 1e-100;
50
51 private static final double VAR_RESCALE_BOUND = 1 / VAR_RESCALE_FACTOR;
52
53 /**
54 * mesure heuristique de l'activite d'une variable.
55 */
56 protected double[] activity = new double[1];
57
58 /**
59 * Derniere variable choisie
60 */
61 protected int lastVar = 1;
62
63 /**
64 * Ordre des variables
65 */
66 protected int[] order = new int[1];
67
68 private double varDecay = 1.0;
69
70 /**
71 * increment pour l'activite des variables.
72 */
73 private double varInc = 1.0;
74
75 /**
76 * position des variables
77 */
78 protected int[] varpos = new int[1];
79
80 protected L lits;
81
82 private long nullchoice = 0;
83
84 // private long randchoice = 0;
85
86 // private Random rand = new Random(12345);
87
88 // private final static double RANDOM_WALK = 0.05;
89
90 /*
91 * (non-Javadoc)
92 *
93 * @see org.sat4j.minisat.core.IOrder#setLits(org.sat4j.minisat.core.ILits)
94 */
95 public void setLits(L lits) {
96 this.lits = lits;
97 }
98
99 /*
100 * (non-Javadoc)
101 *
102 * @see org.sat4j.minisat.core.IOrder#newVar()
103 */
104 public void newVar() {
105 newVar(1);
106 }
107
108 /*
109 * (non-Javadoc)
110 *
111 * @see org.sat4j.minisat.core.IOrder#newVar(int)
112 */
113 public void newVar(int howmany) {
114 }
115
116 /*
117 * (non-Javadoc)
118 *
119 * @see org.sat4j.minisat.core.IOrder#select()
120 */
121 public int select() {
122 assert lastVar > 0;
123 for (int i = lastVar; i < order.length; i++) {
124 assert i > 0;
125 if (lits.isUnassigned(order[i])) {
126 lastVar = i;
127 if (activity[i] < 0.0001) {
128 // if (rand.nextDouble() <= RANDOM_WALK) {
129 // int randomchoice = rand.nextInt(order.length - i) + i;
130 // assert randomchoice >= i;
131 // if ((randomchoice > i)
132 // && lits.isUnassigned(order[randomchoice])) {
133 // randchoice++;
134 // return order[randomchoice];
135 // }
136 // }
137 nullchoice++;
138 }
139 return order[i];
140 }
141 }
142 return ILits.UNDEFINED;
143 }
144
145 /**
146 * Change la valeur de varDecay.
147 *
148 * @param d
149 * la nouvelle valeur de varDecay
150 */
151 public void setVarDecay(double d) {
152 varDecay = d;
153 }
154
155 /*
156 * (non-Javadoc)
157 *
158 * @see org.sat4j.minisat.core.IOrder#undo(int)
159 */
160 public void undo(int x) {
161 assert x > 0;
162 assert x < order.length;
163 int pos = varpos[x];
164 if (pos < lastVar) {
165 lastVar = pos;
166 }
167 assert lastVar > 0;
168 }
169
170 /*
171 * (non-Javadoc)
172 *
173 * @see org.sat4j.minisat.core.IOrder#updateVar(int)
174 */
175 public void updateVar(int p) {
176 assert p > 1;
177 final int var = p >> 1;
178
179 updateActivity(var);
180 int i = varpos[var];
181 for (; i > 1 // because there is nothing at i=0
182 && (activity[order[i - 1] >> 1] < activity[var]); i--) {
183 assert i > 1;
184 // echange p avec son predecesseur
185 final int orderpm1 = order[i - 1];
186 assert varpos[orderpm1 >> 1] == i - 1;
187 varpos[orderpm1 >> 1] = i;
188 order[i] = orderpm1;
189 }
190 assert i >= 1;
191 varpos[var] = i;
192 order[i] = p;
193
194 if (i < lastVar) {
195 lastVar = i;
196 }
197 }
198
199 protected void updateActivity(final int var) {
200 if ((activity[var] += varInc) > VAR_RESCALE_BOUND) {
201 varRescaleActivity();
202 }
203 }
204
205 /**
206 *
207 */
208 public void varDecayActivity() {
209 varInc *= varDecay;
210 }
211
212 /**
213 *
214 */
215 private void varRescaleActivity() {
216 for (int i = 1; i < activity.length; i++) {
217 activity[i] *= VAR_RESCALE_FACTOR;
218 }
219 varInc *= VAR_RESCALE_FACTOR;
220 }
221
222 public double varActivity(int p) {
223 return activity[p >> 1];
224 }
225
226 /**
227 *
228 */
229 public int numberOfInterestingVariables() {
230 int cpt = 0;
231 for (int i = 1; i < activity.length; i++) {
232 if (activity[i] > 1.0) {
233 cpt++;
234 }
235 }
236 return cpt;
237 }
238
239 /*
240 * (non-Javadoc)
241 *
242 * @see org.sat4j.minisat.core.IOrder#init()
243 */
244 public void init() {
245 int nlength = lits.nVars() + 1;
246 int reallength = lits.realnVars() + 1;
247 int[] nvarpos = new int[nlength];
248 double[] nactivity = new double[nlength];
249 int[] norder = new int[reallength];
250 nvarpos[0] = -1;
251 nactivity[0] = -1;
252 norder[0] = ILits.UNDEFINED;
253 for (int i = 1, j = 1; i < nlength; i++) {
254 assert i > 0;
255 assert i <= lits.nVars() : "" + lits.nVars() + "/" + i; //$NON-NLS-1$ //$NON-NLS-2$
256 if (lits.belongsToPool(i)) {
257 norder[j] = lits.getFromPool(i) ^ 1; // Looks a
258 // promising
259 // approach
260 nvarpos[i] = j++;
261 }
262 nactivity[i] = 0.0;
263 }
264 varpos = nvarpos;
265 activity = nactivity;
266 order = norder;
267 lastVar = 1;
268 }
269
270 /**
271 * Affiche les litteraux dans l'ordre de l'heuristique, la valeur de
272 * l'activite entre ().
273 *
274 * @return les litteraux dans l'ordre courant.
275 */
276 @Override
277 public String toString() {
278 return "VSIDS like heuristics from MiniSAT using a sorted array"; //$NON-NLS-1$
279 }
280
281 public ILits getVocabulary() {
282 return lits;
283 }
284
285 /*
286 * (non-Javadoc)
287 *
288 * @see org.sat4j.minisat.core.IOrder#printStat(java.io.PrintStream,
289 * java.lang.String)
290 */
291 public void printStat(PrintWriter out, String prefix) {
292 out.println(prefix + "non guided choices\t" + nullchoice); //$NON-NLS-1$
293 // out.println(prefix + "random choices\t" + randchoice);
294 }
295
296 public void assignLiteral(int p) {
297 // do nothing
298 }
299
300 }