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 final class Heap implements Serializable {
42  
43  	/*
44  	 * default serial version id
45  	 */
46  	private static final long serialVersionUID = 1L;
47  
48  	private static final int left(int i) {
49  		return i << 1;
50  	}
51  
52  	private static final int right(int i) {
53  		return (i << 1) ^ 1;
54  	}
55  
56  	private static final 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) { // NOPMD
102 		this.activity = activity;
103 		heap.push(-1);
104 	}
105 
106 	public void setBounds(int size) {
107 		assert (size >= 0);
108 		indices.growTo(size, 0);
109 	}
110 
111 	public boolean inHeap(int n) {
112 		assert (ok(n));
113 		return indices.get(n) != 0;
114 	}
115 
116 	public void increase(int n) {
117 		assert (ok(n));
118 		assert (inHeap(n));
119 		percolateUp(indices.get(n));
120 	}
121 
122 	public boolean empty() {
123 		return heap.size() == 1;
124 	}
125 
126 	public void insert(int n) {
127 		assert (ok(n));
128 		indices.set(n, heap.size());
129 		heap.push(n);
130 		percolateUp(indices.get(n));
131 	}
132 
133 	public int getmin() {
134 		int r = heap.get(1);
135 		heap.set(1, heap.last());
136 		indices.set(heap.get(1), 1);
137 		indices.set(r, 0);
138 		heap.pop();
139 		if (heap.size() > 1)
140 			percolateDown(1);
141 		return r;
142 	}
143 
144 	public boolean heapProperty() {
145 		return heapProperty(1);
146 	}
147 
148 	public boolean heapProperty(int i) {
149 		return i >= heap.size()
150 				|| ((parent(i) == 0 || !comp(heap.get(i), heap.get(parent(i))))
151 						&& heapProperty(left(i)) && heapProperty(right(i)));
152 	}
153 
154 }