View Javadoc

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  package org.sat4j.minisat.core;
26  
27  import java.io.Serializable;
28  
29  import org.sat4j.core.VecInt;
30  import org.sat4j.specs.IVecInt;
31  
32  /**
33   * Heap implementation used to maintain the variables order in some heuristics.
34   * 
35   * @author daniel
36   * 
37   */
38  public class Heap implements Serializable {
39  
40      /*
41       * default serial version id
42       */
43      private static final long serialVersionUID = 1L;
44  
45      private final static int left(int i) {
46          return i << 1;
47      }
48  
49      private final static int right(int i) {
50          return (i << 1) ^ 1;
51      }
52  
53      private final static int parent(int i) {
54          return i >> 1;
55      }
56  
57      private final boolean comp(int a, int b) {
58          return activity[a] > activity[b];
59      }
60  
61      private final IVecInt heap = new VecInt(); // heap of ints
62  
63      private final IVecInt indices = new VecInt(); // int -> index in heap
64  
65      private final double[] activity;
66  
67      @SuppressWarnings("PMD")
68      final void percolateUp(int i) {
69          int x = heap.get(i);
70          while (parent(i) != 0 && comp(x, heap.get(parent(i)))) {
71              heap.set(i, heap.get(parent(i)));
72              indices.set(heap.get(i), i);
73              i = parent(i);
74          }
75          heap.set(i, x);
76          indices.set(x, i);
77      }
78  
79      final void percolateDown(int i) {
80          int x = heap.get(i);
81          while (left(i) < heap.size()) {
82              int child = right(i) < heap.size()
83                      && comp(heap.get(right(i)), heap.get(left(i))) ? right(i)
84                      : left(i);
85              if (!comp(heap.get(child), x))
86                  break;
87              heap.set(i, heap.get(child));
88              indices.set(heap.get(i), i);
89              i = child;
90          }
91          heap.set(i, x);
92          indices.set(x, i);
93      }
94  
95      boolean ok(int n) {
96          return n >= 0 && n < indices.size();
97      }
98  
99      public Heap(double[] activity) {
100         // DLB findbugs ok
101         this.activity = activity;
102         heap.push(-1);
103     }
104 
105     public void setBounds(int size) {
106         assert (size >= 0);
107         indices.growTo(size, 0);
108     }
109 
110     public boolean inHeap(int n) {
111         assert (ok(n));
112         return indices.get(n) != 0;
113     }
114 
115     public void increase(int n) {
116         assert (ok(n));
117         assert (inHeap(n));
118         percolateUp(indices.get(n));
119     }
120 
121     public boolean empty() {
122         return heap.size() == 1;
123     }
124 
125     public void insert(int n) {
126         assert (ok(n));
127         indices.set(n, heap.size());
128         heap.push(n);
129         percolateUp(indices.get(n));
130     }
131 
132     public int getmin() {
133         int r = heap.get(1);
134         heap.set(1, heap.last());
135         indices.set(heap.get(1), 1);
136         indices.set(r, 0);
137         heap.pop();
138         if (heap.size() > 1)
139             percolateDown(1);
140         return r;
141     }
142 
143     public boolean heapProperty() {
144         return heapProperty(1);
145     }
146 
147     public boolean heapProperty(int i) {
148         return i >= heap.size()
149                 || ((parent(i) == 0 || !comp(heap.get(i), heap.get(parent(i))))
150                         && heapProperty(left(i)) && heapProperty(right(i)));
151     }
152 
153 }