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.constraints.cnf;
29  
30  import java.io.Serializable;
31  
32  import org.sat4j.core.Vec;
33  import org.sat4j.minisat.core.Constr;
34  import org.sat4j.minisat.core.ILits;
35  import org.sat4j.minisat.core.Propagatable;
36  import org.sat4j.minisat.core.Undoable;
37  import org.sat4j.specs.IVec;
38  
39  /**
40   * @author laihem
41   * @author leberre
42   * 
43   */
44  public class Lits implements Serializable, ILits {
45  
46  	private static final long serialVersionUID = 1L;
47  
48  	private boolean pool[] = new boolean[1];
49  
50  	private int realnVars = 0;
51  
52  	@SuppressWarnings("unchecked")
53  	protected IVec<Propagatable>[] watches = new IVec[0];
54  
55  	private int[] level = new int[0];
56  
57  	private Constr[] reason = new Constr[0];
58  
59  	private int maxvarid = 0;
60  
61  	@SuppressWarnings("unchecked")
62  	private IVec<Undoable>[] undos = new IVec[0];
63  
64  	private boolean[] falsified = new boolean[0];
65  
66  	public Lits() {
67  		init(128);
68  	}
69  
70  	@SuppressWarnings( { "unchecked" })
71  	public void init(int nvar) {
72  		if (nvar < pool.length)
73  			return;
74  
75  		assert nvar >= 0;
76  		// let some space for unused 0 indexer.
77  		int nvars = nvar + 1;
78  		boolean[] npool = new boolean[nvars];
79  		System.arraycopy(pool, 0, npool, 0, pool.length);
80  		pool = npool;
81  
82  		int[] nlevel = new int[nvars];
83  		System.arraycopy(level, 0, nlevel, 0, level.length);
84  		level = nlevel;
85  
86  		IVec<Propagatable>[] nwatches = new IVec[2 * nvars];
87  		System.arraycopy(watches, 0, nwatches, 0, watches.length);
88  		watches = nwatches;
89  
90  		IVec<Undoable>[] nundos = new IVec[nvars];
91  		System.arraycopy(undos, 0, nundos, 0, undos.length);
92  		undos = nundos;
93  
94  		Constr[] nreason = new Constr[nvars];
95  		System.arraycopy(reason, 0, nreason, 0, reason.length);
96  		reason = nreason;
97  
98  		boolean[] newFalsified = new boolean[2 * nvars];
99  		System.arraycopy(falsified, 0, newFalsified, 0, falsified.length);
100 		falsified = newFalsified;
101 	}
102 
103 	public int getFromPool(int x) {
104 		int var = Math.abs(x);
105 		if (var >= pool.length) {
106 			init(Math.max(var, pool.length << 1));
107 		}
108 		assert var < pool.length;
109 		if (var > maxvarid) {
110 			maxvarid = var;
111 		}
112 		int lit = ((x < 0) ? (var << 1) ^ 1 : (var << 1));
113 		assert lit > 1;
114 		if (!pool[var]) {
115 			realnVars++;
116 			pool[var] = true;
117 			watches[var << 1] = new Vec<Propagatable>();
118 			watches[(var << 1) | 1] = new Vec<Propagatable>();
119 			undos[var] = new Vec<Undoable>();
120 			level[var] = -1;
121 			falsified[var << 1] = false; // because truthValue[var] is
122 			// UNDEFINED
123 			falsified[var << 1 | 1] = false; // because truthValue[var] is
124 			// UNDEFINED
125 		}
126 		return lit;
127 	}
128 
129 	public boolean belongsToPool(int x) {
130 		assert x > 0;
131 		if (x >= pool.length)
132 			return false;
133 		return pool[x];
134 	}
135 
136 	public void resetPool() {
137 		for (int i = 0; i < pool.length; i++) {
138 			if (pool[i]) {
139 				reset(i << 1);
140 			}
141 		}
142 	}
143 
144 	public void ensurePool(int howmany) {
145 		if (howmany >= pool.length)
146 			init(howmany);
147 		maxvarid = howmany;
148 	}
149 
150 	public void unassign(int lit) {
151 		assert falsified[lit] || falsified[lit ^ 1];
152 		falsified[lit] = false;
153 		falsified[lit ^ 1] = false;
154 	}
155 
156 	public void satisfies(int lit) {
157 		assert !falsified[lit] && !falsified[lit ^ 1];
158 		falsified[lit] = false;
159 		falsified[lit ^ 1] = true;
160 	}
161 
162 	public boolean isSatisfied(int lit) {
163 		return falsified[lit ^ 1];
164 	}
165 
166 	public final boolean isFalsified(int lit) {
167 		return falsified[lit];
168 	}
169 
170 	public boolean isUnassigned(int lit) {
171 		return !falsified[lit] && !falsified[lit ^ 1];
172 	}
173 
174 	public String valueToString(int lit) {
175 		if (isUnassigned(lit))
176 			return "?"; //$NON-NLS-1$
177 		if (isSatisfied(lit))
178 			return "T"; //$NON-NLS-1$
179 		return "F"; //$NON-NLS-1$
180 	}
181 
182 	public int nVars() {
183 		// return pool.length - 1;
184 		return maxvarid;
185 	}
186 
187 	public int not(int lit) {
188 		return lit ^ 1;
189 	}
190 
191 	public static String toString(int lit) {
192 		return ((lit & 1) == 0 ? "" : "-") + (lit >> 1); //$NON-NLS-1$//$NON-NLS-2$
193 	}
194 
195 	public void reset(int lit) {
196 		watches[lit].clear();
197 		watches[lit ^ 1].clear();
198 		level[lit >> 1] = -1;
199 		reason[lit >> 1] = null;
200 		undos[lit >> 1].clear();
201 		falsified[lit] = false;
202 		falsified[lit ^ 1] = false;
203 	}
204 
205 	public int getLevel(int lit) {
206 		return level[lit >> 1];
207 	}
208 
209 	public void setLevel(int lit, int l) {
210 		level[lit >> 1] = l;
211 	}
212 
213 	public Constr getReason(int lit) {
214 		return reason[lit >> 1];
215 	}
216 
217 	public void setReason(int lit, Constr r) {
218 		reason[lit >> 1] = r;
219 	}
220 
221 	public IVec<Undoable> undos(int lit) {
222 		return undos[lit >> 1];
223 	}
224 
225 	public void watch(int lit, Propagatable c) {
226 		watches[lit].push(c);
227 	}
228 
229 	public IVec<Propagatable> watches(int lit) {
230 		return watches[lit];
231 	}
232 
233 	public boolean isImplied(int lit) {
234 		int var = lit >> 1;
235 		assert reason[var] == null || falsified[lit] || falsified[lit ^ 1];
236 		// a literal is implied if it is a unit clause, ie
237 		// propagated without reason at decision level 0.
238 		return pool[var] && (reason[var] != null || level[var] == 0);
239 	}
240 
241 	public int realnVars() {
242 		return realnVars;
243 	}
244 
245 	/**
246 	 * To get the capacity of the current vocabulary.
247 	 * 
248 	 * @return the total number of variables that can be managed by the
249 	 *         vocabulary.
250 	 */
251 	protected int capacity() {
252 		return pool.length - 1;
253 	}
254 
255 	/**
256 	 * @since 2.1
257 	 */
258 	public int nextFreeVarId(boolean reserve) {
259 		if (reserve) {
260 			ensurePool(maxvarid + 1);
261 			// ensure pool changes maxvarid
262 			return maxvarid;
263 		}
264 		return maxvarid + 1;
265 	}
266 }