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