View Javadoc

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