View Javadoc

1   /*******************************************************************************
2   * SAT4J: a SATisfiability library for Java Copyright (C) 2004-2008 Daniel Le Berre
3   *
4   * All rights reserved. This program and the accompanying materials
5   * are made available under the terms of the Eclipse Public License v1.0
6   * which accompanies this distribution, and is available at
7   * http://www.eclipse.org/legal/epl-v10.html
8   *
9   * Alternatively, the contents of this file may be used under the terms of
10  * either the GNU Lesser General Public License Version 2.1 or later (the
11  * "LGPL"), in which case the provisions of the LGPL are applicable instead
12  * of those above. If you wish to allow use of your version of this file only
13  * under the terms of the LGPL, and not to allow others to use your version of
14  * this file under the terms of the EPL, indicate your decision by deleting
15  * the provisions above and replace them with the notice and other provisions
16  * required by the LGPL. If you do not delete the provisions above, a recipient
17  * may use your version of this file under the terms of the EPL or the LGPL.
18  * 
19  * Based on the original MiniSat specification from:
20  * 
21  * An extensible SAT solver. Niklas Een and Niklas Sorensson. Proceedings of the
22  * Sixth International Conference on Theory and Applications of Satisfiability
23  * Testing, LNCS 2919, pp 502-518, 2003.
24  *
25  * See www.minisat.se for the original solver in C++.
26  * 
27  *******************************************************************************/
28  package org.sat4j.minisat.orders;
29  
30  import static org.sat4j.core.LiteralsUtils.var;
31  
32  import java.io.PrintWriter;
33  import java.io.Serializable;
34  
35  import org.sat4j.minisat.core.Heap;
36  import org.sat4j.minisat.core.ILits;
37  import org.sat4j.minisat.core.IOrder;
38  import org.sat4j.minisat.core.IPhaseSelectionStrategy;
39  
40  /*
41   * Created on 16 oct. 2003
42   */
43  
44  /**
45   * @author leberre Heuristique du prouveur. Changement par rapport au MiniSAT
46   *         original : la gestion activity est faite ici et non plus dans Solver.
47   */
48  public class VarOrderHeap implements IOrder, Serializable {
49  
50      private static final long serialVersionUID = 1L;
51  
52      private static final double VAR_RESCALE_FACTOR = 1e-100;
53  
54      private static final double VAR_RESCALE_BOUND = 1 / VAR_RESCALE_FACTOR;
55  
56      /**
57       * mesure heuristique de l'activite d'une variable.
58       */
59      protected double[] activity = new double[1];
60  
61      private double varDecay = 1.0;
62  
63      /**
64       * increment pour l'activite des variables.
65       */
66      private double varInc = 1.0;
67  
68      protected ILits lits;
69  
70      private long nullchoice = 0;
71  
72      protected Heap heap;
73  
74      protected IPhaseSelectionStrategy phaseStrategy;
75      
76      public VarOrderHeap() {
77          this(new PhaseInLastLearnedClauseSelectionStrategy());
78      }
79      
80      public VarOrderHeap(IPhaseSelectionStrategy strategy) {
81          this.phaseStrategy = strategy;
82      }
83      
84      /**
85       * Change the selection strategy.
86       * 
87       * @param strategy
88       */
89      public void setPhaseSelectionStrategy(IPhaseSelectionStrategy strategy) {
90          phaseStrategy = strategy;
91      }
92      
93      public IPhaseSelectionStrategy getPhaseSelectionStrategy() {
94          return phaseStrategy;
95      }
96      
97      public void setLits(ILits lits) {
98          this.lits = lits;
99      }
100 
101     /**
102      * Selectionne une nouvelle variable, non affectee, ayant l'activite
103      * la plus elevee.
104      * 
105      * @return Lit.UNDEFINED si aucune variable n'est trouvee
106      */
107     public int select() {
108         while (!heap.empty()) {
109             int var = heap.getmin();
110             int next = phaseStrategy.select(var);
111             if (lits.isUnassigned(next)) {
112                 if (activity[var] < 0.0001) {
113                     nullchoice++;
114                 }
115                 return next;
116             }
117         }
118         return ILits.UNDEFINED;
119     }
120 
121     /**
122      * Change la valeur de varDecay.
123      * 
124      * @param d
125      *            la nouvelle valeur de varDecay
126      */
127     public void setVarDecay(double d) {
128         varDecay = d;
129     }
130 
131     /**
132      * Methode appelee quand la variable x est desaffectee.
133      * 
134      * @param x
135      */
136     public void undo(int x) {
137         if (!heap.inHeap(x))
138             heap.insert(x);
139     }
140 
141     /**
142      * Appelee lorsque l'activite de la variable x a change.
143      * 
144      * @param p
145      *            a literal
146      */
147     public void updateVar(int p) {
148         int var = var(p);
149         updateActivity(var);
150         phaseStrategy.updateVar(p);
151         if (heap.inHeap(var))
152             heap.increase(var);
153     }
154 
155     protected void updateActivity(final int var) {
156         if ((activity[var] += varInc) > VAR_RESCALE_BOUND) {
157             varRescaleActivity();
158         }
159     }
160 
161     /**
162      * 
163      */
164     public void varDecayActivity() {
165         varInc *= varDecay;
166     }
167 
168     /**
169      * 
170      */
171     private void varRescaleActivity() {
172         for (int i = 1; i < activity.length; i++) {
173             activity[i] *= VAR_RESCALE_FACTOR;
174         }
175         varInc *= VAR_RESCALE_FACTOR;
176     }
177 
178     public double varActivity(int p) {
179         return activity[var(p)];
180     }
181 
182     /**
183      * 
184      */
185     public int numberOfInterestingVariables() {
186         int cpt = 0;
187         for (int i = 1; i < activity.length; i++) {
188             if (activity[i] > 1.0) {
189                 cpt++;
190             }
191         }
192         return cpt;
193     }
194 
195     /**
196      * that method has the responsability to initialize all arrays in the
197      * heuristics. PLEASE CALL super.init() IF YOU OVERRIDE THAT METHOD.
198      */
199     public void init() {
200         int nlength = lits.nVars() + 1;
201         activity = new double[nlength];
202         phaseStrategy.init(nlength);
203         activity[0] = -1;
204         heap = new Heap(activity);
205         heap.setBounds(nlength);
206         for (int i = 1; i < nlength; i++) {
207             assert i > 0;
208             assert i <= lits.nVars() : "" + lits.nVars() + "/" + i; //$NON-NLS-1$ //$NON-NLS-2$
209             activity[i] = 0.0;
210             if (lits.belongsToPool(i)) {
211                 heap.insert(i);
212             }
213         }
214     }
215 
216     @Override
217     public String toString() {
218         return "VSIDS like heuristics from MiniSAT using a heap "+phaseStrategy; //$NON-NLS-1$
219     }
220 
221     public ILits getVocabulary() {
222         return lits;
223     }
224 
225     public void printStat(PrintWriter out, String prefix) {
226         out.println(prefix + "non guided choices\t" + nullchoice); //$NON-NLS-1$
227     }
228 
229     public void assignLiteral(int p) {
230         // do nothing       
231     }
232 }