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.Heap;
32 import org.sat4j.minisat.core.ILits;
33 import org.sat4j.minisat.core.IOrder;
34
35 /*
36 * Created on 16 oct. 2003
37 */
38
39 /**
40 * @author leberre Heuristique du prouveur. Changement par rapport au MiniSAT
41 * original : la gestion activity est faite ici et non plus dans Solver.
42 */
43 public class VarOrderHeap<L extends ILits> implements IOrder<L>, 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 * mesure heuristique de l'activite d'une variable.
53 */
54 protected double[] activity = new double[1];
55
56 private double varDecay = 1.0;
57
58 /**
59 * increment pour l'activite des variables.
60 */
61 private double varInc = 1.0;
62
63 protected L lits;
64
65 private long nullchoice = 0;
66
67 protected Heap heap;
68
69 protected int[] phase;
70
71 public void setLits(L lits) {
72 this.lits = lits;
73 }
74
75 /**
76 * Appelee quand une nouvelle variable est creee.
77 */
78 public void newVar() {
79 newVar(1);
80 }
81
82 /**
83 * Appelee lorsque plusieurs variables sont creees
84 *
85 * @param howmany
86 * le nombre de variables creees
87 */
88 public void newVar(int howmany) {
89 }
90
91 /**
92 * Selectionne une nouvelle variable, non affectee, ayant l'activite
93 * la plus elevee.
94 *
95 * @return Lit.UNDEFINED si aucune variable n'est trouvee
96 */
97 public int select() {
98 while (!heap.empty()) {
99 int var = heap.getmin();
100 int next = phase[var];
101 if (lits.isUnassigned(next)) {
102 if (activity[var] < 0.0001) {
103 nullchoice++;
104 }
105 return next;
106 }
107 }
108 return ILits.UNDEFINED;
109 }
110
111 /**
112 * Change la valeur de varDecay.
113 *
114 * @param d
115 * la nouvelle valeur de varDecay
116 */
117 public void setVarDecay(double d) {
118 varDecay = d;
119 }
120
121 /**
122 * Methode appelee quand la variable x est desaffectee.
123 *
124 * @param x
125 */
126 public void undo(int x) {
127 if (!heap.inHeap(x))
128 heap.insert(x);
129 }
130
131 /**
132 * Appelee lorsque l'activite de la variable x a change.
133 *
134 * @param p
135 * a literal
136 */
137 public void updateVar(int p) {
138 int var = p >> 1;
139 updateActivity(var);
140 phase[var] = p;
141 if (heap.inHeap(var))
142 heap.increase(var);
143 }
144
145 protected void updateActivity(final int var) {
146 if ((activity[var] += varInc) > VAR_RESCALE_BOUND) {
147 varRescaleActivity();
148 }
149 }
150
151 /**
152 *
153 */
154 public void varDecayActivity() {
155 varInc *= varDecay;
156 }
157
158 /**
159 *
160 */
161 private void varRescaleActivity() {
162 for (int i = 1; i < activity.length; i++) {
163 activity[i] *= VAR_RESCALE_FACTOR;
164 }
165 varInc *= VAR_RESCALE_FACTOR;
166 }
167
168 public double varActivity(int p) {
169 return activity[p >> 1];
170 }
171
172 /**
173 *
174 */
175 public int numberOfInterestingVariables() {
176 int cpt = 0;
177 for (int i = 1; i < activity.length; i++) {
178 if (activity[i] > 1.0) {
179 cpt++;
180 }
181 }
182 return cpt;
183 }
184
185 /**
186 * that method has the responsability to initialize all arrays in the
187 * heuristics. PLEASE CALL super.init() IF YOU OVERRIDE THAT METHOD.
188 */
189 public void init() {
190 int nlength = lits.nVars() + 1;
191 activity = new double[nlength];
192 phase = new int[nlength];
193 activity[0] = -1;
194 heap = new Heap(activity);
195 heap.setBounds(nlength);
196 for (int i = 1; i < nlength; i++) {
197 assert i > 0;
198 assert i <= lits.nVars() : "" + lits.nVars() + "/" + i; //$NON-NLS-1$ //$NON-NLS-2$
199 activity[i] = 0.0;
200 if (lits.belongsToPool(i)) {
201 heap.insert(i);
202 phase[i] = (i << 1) ^ 1;
203 } else {
204 phase[i] = ILits.UNDEFINED;
205 }
206 }
207 }
208
209 @Override
210 public String toString() {
211 return "VSIDS like heuristics from MiniSAT using a heap"; //$NON-NLS-1$
212 }
213
214 public ILits getVocabulary() {
215 return lits;
216 }
217
218 public void printStat(PrintWriter out, String prefix) {
219 out.println(prefix + "non guided choices\t" + nullchoice); //$NON-NLS-1$
220 }
221
222 public void assignLiteral(int p) {
223 // do nothing
224 }
225 }